numeri di Church

Booleani di church

Valori

$$\begin{gathered} \text{true}\equiv \text{Fn}xy⟹x \\ \text{false}\equiv \text{Fn}xy⟹y \end{gathered}$$

Che è uno short hand per:

$$\begin{gathered} \text{true}\equiv \text{Fn}x⟹\text{Fn}y⟹x \\ \text{false}\equiv \text{Fn}x⟹\text{Fn}y⟹y \end{gathered}$$

Operazioni

$$\text{not}\equiv \text{Fn}Z⟹\text{Fn}xy⟹Zyx$$

nj_sml

Se la applichiamo a un booleano di Church, la funzione ci da un booleano vero?

todo Si dimostra che la funzione ifthenelse $\text{Fn}z⟹z$ è un booleano di Church. L’ifthenelse è una proprietà dei booleani, i booleani sono degli ifthenelse.