Czy algebrę boolowską można wyrazić prostym typem lambda caclulus?

Algebra boolowska może być wyrażona w ten sposób bez typu rachunku lambda (na przykład).

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;

Również algebra boolowska może być zakodowana w Systemie F w następujący sposób :

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;

Czy istnieje sposób na wyrażenie algebry boolowskiej w prostym typie rachunku lambda? Zakładam, że odpowiedź brzmi NIE. ( Na przykład Poprzednik i listy nie są reprezentowalne w prostym typie rachunku lambda .) Jeśli odpowiedź brzmi NIE, to czy istnieje proste intuicyjne wyjaśnienie, dlaczego nie można zakodować boolanów w prostym typie rachunku lambda?

AKTUALIZACJA: Zakładamy, że istnieją typy podstawowe.

AKTUALIZACJA: Znaleziono tutaj odpowiedź negatywną z wyjaśnieniem (komentarz „Oto szkic dowodu, który pokazuje, że prosty rachunek różniczkowy lambda z produktami i nieskończenie wieloma typami podstawowymi nie ma boolanów”). Właśnie tego szukałem.

lo.logic type-theory lambda-calculus

— Ilja Klyuchnikov
źródło

Spróbuj wpisać definicje w Haskell i zobacz, co się stanie, gdy dodasz typy do różnych wyrażeń. Przekonasz się, że kod w dużej mierze opiera się na polimorfizmie.

— Dave Clarke

Przepraszam, że jestem pedantyczny, ale pytania o ekspresję tego lub tego rachunku różnobarwnego stają się znaczące tylko dzięki jasnemu zrozumieniu tego, co rozumiesz przez „wyrażony”, „zakodowany” i „reprezentowany”, ponieważ istnieje wiele rozsądnych sposobów zrozumienia tych terminów. Co więcej, skoro określasz istnienie typów bazowych, musisz sprecyzować, co to są i jakie konstruktory / destruktory pochodzą.

— Martin Berger

Przepraszam, że nie byłem pedantyczny. Odpowiedź znaleziono tutaj: math.andrej.com/2009/03/21/...

— Ilya Klyuchnikov

Wydaje mi się, że powinienem trochę podziękować za prowadzenie tak fajnego bloga :-)

— Andrej Bauer

O

$O$

B = O \to O \to O

$B=O\to O\to O$

t r u e = λ x : O . λ y : O . x

$\mathrm{true}=\lambda x:O.\lambda y:O.x$

f a l s e = λ x : O . λ y : O . y

$\mathrm{false}=\lambda x:O.\lambda y:O.y$

n o t = λ a : B . λ x : O . λ y : O . a y x

$\mathrm{not}=\lambda a:B.\lambda x:O.\lambda y:O.ayx$

a n d = λ a : B . λ b : B . λ x : O . λ y : O . a (b x y) y

$\mathrm{and}=\lambda a:B.\lambda b:B.\lambda x:O.\lambda y:O.a(bxy)y$

o r = λ a : B . λ b : B . λ x : O . λ y : O . a x (b x y)

$\mathrm{or}=\lambda a:B.\lambda b:B.\lambda x:O.\lambda y:O.ax(bxy)$

OP napisał powyżej, że na pytanie odpowiada post na blogu @ AndrejBauer .

— Bjørn Kjos-Hanssen
źródło