論理値を以下の関数で定義します。
trueとfalseの値を関数で定義するなんて、何てミステリアス。
\textbf{T} = \lambda x y.x
\textbf{F} = \lambda x y.y
$\textbf{T}$は最初の変数に置き換え、$\textbf{F}$は二番目の変数に置き換える操作のようです。
論理積$\land$は$$\land=\lambda a b.ab\textbf{F}$$と定義します。
$$\land\ \textbf{T}\textbf{T}\longrightarrow_\beta\textbf{T}$$
$$\land\textbf{F}\textbf{T}\longrightarrow_\beta\textbf{F}$$
$$\land\textbf{T}\textbf{F}\longrightarrow_\beta\textbf{F}$$
$$\land\textbf{F}\textbf{F}\longrightarrow_\beta\textbf{F}$$
Haskellで確認すると、
t' x y = x -- true
f' x y = y -- false
and a b = a b f'
-- Evaluation
main = do
print $ and t' t' 1 0
print $ and f' t' 1 0
print $ and t' f' 1 0
print $ and f' f' 1 0
>ghci> main
1
0
0
0
式の評価で最後はt'やf'として出力したかったのですが、Haskellでは値がないと評価できないようです。t'ならば最初の価を、f'ならば二番目の値を取るので1 0のようにして右側に付けました。1は真、0は僞です。t'やf'などの形で出力できる方法をご存じでしたら教えてください。
Exerecise 5
論理和$\lor$の式はどうなるか？最初は$\lambda a b.a b \textbf{T}$かと思いましたが、予想に反して$\lor\equiv\lambda a b.b \textbf{T}a$でした。全く、直観に反した答えでした。ちなみに、前の式は排他的論理和でした。$\textbf{xor}\equiv\lambda a b.a b\textbf{T}$
否定（NOT）論理演算子は、$\neg\equiv\lambda x.x\textbf{F}\textbf{T}$となります。
$\neg\textbf{T}\equiv(\lambda x.x\textbf{F}\textbf{T})\textbf{T}\rightarrow\textbf{T}\textbf{F}\textbf{T}\rightarrow\textbf{F}$
$\neg\textbf{F}\equiv(\lambda x.x\textbf{F}\textbf{T})\textbf{F}\rightarrow\textbf{F}\textbf{F}\textbf{T}\rightarrow\textbf{T}$
更に、条件式は$\textbf{if_then_else}\equiv\lambda x.x$となります。
$$\textbf{if_then_else}\ \textbf{T}MN\longrightarrow_\beta M$$
$$\textbf{if_then_else}\ \textbf{F}MN\longrightarrow_\beta N$$
Haskellでは以下のように書けますね。
or' a b = b t' a -- orは予約語なのか通りませんでした。
xor a b = a b t'
not x = x f' t'