El álgebra booleana se puede expresar en cálculo lambda sin tipo de (por ejemplo) de esta manera.
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;
También el álgebra booleana se puede codificar en el Sistema F de esta manera :
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;
¿Hay alguna manera de expresar el álgebra booleana en un cálculo lambda simplemente escrito? Supongo que la respuesta es NO. ( Por ejemplo, el predecesor y las listas no son representables en cálculo lambda simplemente tipado ). Si la respuesta es NO, ¿existe una explicación intuitiva simple, por qué es imposible codificar booleanos en cálculo lambda simplemente tipado?
ACTUALIZACIÓN: Suponemos que hay tipos base.
ACTUALIZACIÓN: La respuesta negativa con explicación se encontró aquí (Comentario "Aquí hay un bosquejo de prueba para mostrar que el cálculo lambda de tipo simple con productos e infinitos tipos de bases no tiene booleanos"). Esto es lo que estaba buscando.
fuente
Respuestas:
El OP escribió anteriormente que la pregunta es respondida por una publicación en el blog de @ AndrejBauer .
fuente