チャーチブール値

2つの引数を取って、

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

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

型注釈はSystem Fによるもの

定義

tru = λtf.t

tru = ΛX. λt:X. λf:X. t

tru: CBool

fls = λtf.f

fls = ΛX. λt:X. λf:X. f

fls: CBool

型注釈

CBool = ∀X.X->X->X

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

if文ぽいもの

$ \overline{B}MN

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

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

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

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

論理演算を定義する

and = λb λc.bc fls

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

and b c

$ 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}

or = λbλc.b tru c

not = λb.b fls tru

not = λb:CBool. ΛX. λt:X. λf:X. b[X] f t

not: CBool -> CBool