deniok

В импликационном фрагменте классической пропозициональной логики у нас нет никаких связок кроме импликационной стрелочки. Поэтому мы не можем записать закон двойного отрицания или закон исключённого третьего - у нас для этого нет соответствующей связки. Однако имеется закон Пирса ((α → β) → α) → α, который в классической логике полностью эквивалентен упомянутым законам.

В просто типизированной лямбде тип ((α → β) → α) → α необитаем, поскольку соответствие Карри-Говарда задаёт изоморфизм с интуиционистской логикой, которая отличается от классической как раз отсутствием всех этих законов. Однако имеется слабый закон Пирса ((((α → β) → α) → α) → β) → β, про который известно, что он верен интуиционистски, а значит может быть получен конструктивно.

Откуда возникает задача: написать в просто типизированном лямбда-исчислении замкнутый терм типа ((((α → β) → α) → α) → β) → β.

Комменты не скринятся; Coq-читерам предлагается забыть про тактику auto и вспомнить про intros, apply и exact :)

Придумал задачку по лямбда исчислению.

Общеизвестен лямбда-терм, не имеющий нормальной формы

(\x.xx)(\x.xx)

Этот терм обладает следующим свойством: он воспроизводит сам себя при каждой бета-редукции, ведя себя по отношению к ней как экспонента по отношению к дифференцированию.

А теперь задача: написать не имеющий нормальной формы терм, который бы вел себя как e^(-x). То есть при первой бета-редукции он должен превращаться во что-то другое, а при следующей возвращаться к исходному виду. Моя версия такого терма (flipflop) под катом белым цветом
( Ответ тут, белым цветом... )
Может кто придумает попроще?

UPD: Эх, а у меня-то решение неправильное :) (Потому что у меня аж шесть шагов) Правильное - у lomeo в комментах.

Прекрасная логическая задачка с подробным обсуждением у avva. Формулировка там чуть-чуть неясная (допустимы формальные придирки), ниже, в комментах, vik_rud  дал более точный перевод (который я слегка причесал):

Есть остров, на котором проживает одно племя. Племя состоит из 1000 человек, имеющих разный цвет глаз. Их религия запрещает им знать их собственный цвет глаз или обсуждать эту тему с другими. Таким образом, каждый житель может видеть (и видит) цвет глаз всех других жителей, но не имеет никакого способа выяснить цвет собственных глаз (отражающие поверхности отсутствуют). Если житель выясняет каким-то образом цвет собственных глаз, то, в соответствии с религией, он обязан совершить ритуальное самоубийство в полдень следующего дня на глазах у всех остальных жителей. Все жители очень логичны и набожны, и каждый знает, что все жители очень логичны и набожны (и каждый знает, что каждый знает, что все жители очень логичны и набожны и т.д.)

Из 1000 островитян 100 имеют голубые глаза, а остальные 900 имеют карие глаза, хотя островитяне первоначально не обладают этими статистическими данными (каждый из них может видеть только 999 из 1000 жителей).

Однажды голубоглазый иностранец посещает остров и завоевывает полное доверие племени.

Как-то вечером, он обращается ко всему племени, и благодарит их за гостеприимство.

Однако, не зная местных обычаев, иностранец делает ошибку, упоминая цвет глаз в своем обращении: "Как необычно видеть другого голубоглазого человека, такого как я, в этой части света".

Какое воздействие эта бестактность окажет на племя?

UPD. По совету друзей приобрел автомобиль "Москвич" подкорректировал перевод. Фактически у avva не очень ясно указано лишь, что статистика 100/900 неизвестна островитянам. Ну и подсказка "каждый знает, что каждый знает, ..." про общее знание опущена ;) Англоязычный оригинал.