Lazi

Remplacer 0b, 1b, if façon lambda calcul

Contexte

En lambda calcul on définit 0b par $F x,y → y, 1b par $F x,y → x.

Question

Peut-on faire la même chose en lazi ?
Non car les fonctions ont besoin de if 1b et 0b pour être définies.

Mais pour définir les fonctions il n'y a besoin que de identF et constF, peut - on alors avoir des règles définissant identF et constF et se passer de if,0b et 1b ?

règles à ajouter :
identF x = x
constF x y = x

Puis on définit :
$Def 1b = $F x,y → x
$Def 0b = $F x,y → y
$Def if = $F c,x,y → c x y

Mais alors on a des problèmes de tiers exclu car on peut avoir if x y z = 1b sans pour autant que x soit 1b ou 0b.

Réponse

Non.