from Church encoding

2つの引数を取って、

最初の値を返すか、2番目の値を返すか

「関数」でBool値を表現している

型注釈はSystem Fによるもの

定義

型注釈

2つの引数を取ってどちらか一方を返すだけなので、型自体は任意で良い

if文ぽいもの

\overline{B}MN

\overline{B}には、チャーチブール値のどちらかが入る

もしくは簡約の結果、チャーチブール値になるものでもいい

以下の様に見ることができる

\mathrm{if}\;\overline{B}\;\mathrm{then}\;M\mathrm{else}\;N

論理演算を定義する

2つのチャーチブール値を引数を取る

b,cが共に\overline{T}のときのみ\overline{T}を返す

ex. \lambda bc.bc\overline{F} \overline{T}\overline{F}\to_\beta\overline{T}\overline{F}\overline{F}\to_\beta\overline{F}