L'algèbre booléenne peut-elle s'exprimer en lambda caclulus simplement typé?

15

L'algèbre booléenne peut être exprimée dans le calcul lambda non typé de cette manière (par exemple).

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;

L'algèbre booléenne peut également être encodée dans le système F de cette manière :

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;

Existe-t-il un moyen d'exprimer l'algèbre booléenne dans un calcul lambda simplement tapé? Je suppose que cette réponse est NON. ( Par exemple, le prédécesseur et les listes ne sont pas représentables dans le lambda-calcul simplement tapé .) Si la réponse est NON, existe-t-il une explication intuitive simple, pourquoi il est impossible de coder des booléens dans un lambda-calcul simplement tapé?

MISE À JOUR: Nous supposons qu'il existe des types de base.

MISE À JOUR: La réponse négative avec explication a été trouvée ici (Commentaire "Voici un croquis de preuve pour montrer que le calcul lambda simplement tapé avec des produits et une infinité de types de base n'a pas de booléens.") C'est ce que je cherchais.

lo.logic type-theory lambda-calculus Ilya Klyuchnikov
la source
2
Essayez de taper les définitions dans Haskell et voyez ce qui se passe lorsque vous donnez des types à diverses expressions. Vous verrez que le code repose fortement sur le polymorphisme.
Dave Clarke
2
Désolé d'être pédant, mais les questions sur l'expressivité de tel ou tel calcul ne deviennent significatives qu'avec une compréhension claire de ce que vous entendez par "exprimé", "codé" et "représenté", car il existe plusieurs façons raisonnables de comprendre ces termes. De plus, puisque vous stipulez l'existence de types de base, vous devez être précis sur ce que sont ces types et sur les constructeurs / destructeurs avec lesquels ils sont fournis.
Martin Berger
3
Désolé que je n'étais pas pédant. La réponse a été trouvée ici: math.andrej.com/2009/03/21/…
Ilya Klyuchnikov
3
Je pense que je devrais obtenir un crédit pour avoir dirigé un blog aussi astucieux :-)
Andrej Bauer
7
La définition d'un type booléen utilisée sur le blog est plus forte qu'ici. En fait, la réponse de Jeremy montre qu'un calcul lambda simplement tapé avec au moins un type de base (appelez-le ) peut exprimer l'algèbre booléenne au sens de l'OP: définissez , , , , , . OB=O→O→Otrue=λX:O.λy:O.XFunelse=λX:O.λy:O.ynot=λune:B.λX:O.λy:O.uneyXunenré=λune:B.λb:B.λX:O.λy:O.une(bXy)yor=λune:B.λb:B.λX:O.λy:O.uneX(bXy)
Emil Jeřábek soutient Monica le

Réponses: