Может ли булева алгебра быть выражена в просто типизированной лямбда-какклус?

15

Таким образом, булева алгебра может быть выражена в нетипизированном лямбда-исчислении .

true  = \t. \f. t;
false = \t. \f. t;
not   = \x. x false true;
and   = \x. \y. x y false;
or    = \x. \y. x true y;

Также булева алгебра может быть закодирована в Системе F следующим образом :

CBool = All X.X -> X -> X;
true  = \X. \t:X. \f:X. t;
false = \X. \t:X. \f:X. f;
not   = \x:CBool. x [CBool] false true;
and   = \x:CBool. \y:CBool. x [CBool] y false;
or    = \x:CBool. \y:CBool. x [CBool] true y;

Есть ли способ выразить булеву алгебру в простом типе лямбда-исчисления? Я предполагаю, что ответ НЕТ. ( Например, Предшественник и списки не могут быть представлены в простом типе лямбда-исчисления .) Если ответ действительно НЕТ, есть ли простое интуитивное объяснение, почему невозможно кодировать логические значения в просто типизированном лямбда-исчислении?

ОБНОВЛЕНИЕ: Мы предполагаем, что есть базовые типы.

ОБНОВЛЕНИЕ: здесь был найден отрицательный ответ с объяснением (комментарий «Вот эскиз для доказательства того, что лямбда-исчисление простого типа с продуктами и бесконечным числом базовых типов не имеет логических значений».) Это то, что я искал.

Илья Ключников
источник
2
Попробуйте ввести определения в Haskell и посмотрите, что произойдет, когда вы дадите типы различным выражениям. Вы увидите, что код сильно зависит от полиморфизма.
Дейв Кларк
2
Извините за педантичность, но вопросы о выразительности того или иного исчисления становятся осмысленными только при ясном понимании того, что вы подразумеваете под «выраженным», «закодированным» и «представленным», поскольку существует множество разумных способов понимания этих терминов. Более того, поскольку вы оговариваете существование базовых типов, вам нужно будет конкретно указать, что это такое и с какими конструкторами / деструкторами они идут.
Мартин Бергер
3
Извините, что я не был педантичным. Ответ был найден здесь: math.andrej.com/2009/03/21/…
Илья Ключников
3
Я чувствую, что должен получить некоторый кредит за ведение такого изящного блога :-)
Андрей Бауэр
7
Определение логического типа, используемого в блоге, сильнее, чем здесь. Фактически, ответ Джереми показывает, что лямбда-исчисление с простыми типами, по крайней мере, с одним базовым типом (назовем его ) может выражать булеву алгебру в смысле OP: определить B = O O O , t r u e = λ x : O . λ у : O . х , е L сек е = λ х : O . λ y :ОВзнак равноОООTрUезнак равноλИкс:О,λY:О,Икс , п о т = λ : В . λ х : O . λ у : O . у й , п д = λ : В . λ б : Б . λ х : O . λ у : O . ( б х у ) у , о геaLsезнак равноλИкс:О,λY:О,YNоTзнак равноλa:В,λИкс:О,λY:О,aYИксaNdзнак равноλa:В,λб:В,λИкс:О,λY:О,a(бИксY)Y . орзнак равноλa:В,λб:В,λИкс:О,λY:О,aИкс(бИксY)
Эмиль Йержабек поддерживает Монику

Ответы: