次の式が与えられたとします (l をラムダと呼びます):
lx.f1 f2 x
ここで、f1 と f2 は関数であり、x はある数値を想定しています。
この表現をどう解釈しますか？lx.(f1 f2) x は lx.f1 (f2 x) と同じですか?
例として、lx.(not eq0) x と lx.not (eq0 x) の結果の違いは何でしょうか? (eq0 は parm が 0 の場合に true を返す関数であり、not はよく知られている not 関数です)
より形式的には T=lx.ly.x ,F=lx.ly.y ,not = lx.xFT および eq0 = lx.x(ly.F)T
f1 f2 xと同じ(f1 f2) xです。関数の適用は左結合です。
ln.(f1 f2) x は ln.f1 (f2 x) と同じですか?
いいえ、まったくありません。(f1 f2) xを引数として呼び出しf1てf2から、結果の関数をx引数として呼び出します。f1 (f2 x)引数として を呼び出しf2、x次にf1の結果をf2 x引数として呼び出します。
ln.(not eq0) x と ln.not (eq0 x)?
型指定されたラムダ計算について話しnot、ブール値を引数として期待する場合、前者は単純に型エラーを引き起こします (eq0は関数であり、ブール値ではないため)。型指定されていないラムダ計算について話していて、trueandfalseが関数として表されている場合、それは がどのようnotに定義され、どのようtrueに andfalseが表されているかに依存します。
trueとfalseが教会のブール値である場合、つまりtrueが最初の引数を返すfalse2 引数の関数であり、2 番目の引数を返す 2 引数の関数である場合、 は関数notと同等flipです。つまり、2 引数の関数を取り、2 つの引数を返します。 -argument 引数が逆になっている関数。So(not eq0) xは、他の 2 つの引数yおよびに適用されるとz、 に評価される関数を返し((eq0 y) x) zます。したがって、yが 0 の場合は を返しx、そうでない場合は を返しますz。