教会のエンコーディング

数学において、チャーチ符号化は、ラムダ計算でデータと演算子を表現する手段です。チャーチ数字は、ラムダ表記法を使用して自然数を表します。この方法は、ラムダ計算でこの方法で初めてデータを符号化したアロンゾ・チャーチにちなんで名付けられました。

他の表記法では通常プリミティブと見なされる用語 (整数、ブール値、ペア、リスト、タグ付き共用体など) は、チャーチ符号化では高階関数にマッピングされます。チャーチ-チューリングのテーゼは、計算可能な演算子 (およびそのオペランド) はどれもチャーチ符号化で表現できると主張しています。^{[疑わしい–議論する]}型なしラムダ計算では、関数だけがプリミティブ データ型です。

チャーチ符号化方式を単純に実装すると、 から へのアクセス操作が遅くなります。ここで はデータ構造のサイズであり、チャーチ符号化方式は実用的ではありません。^[1]研究では、この問題は対象を絞った最適化によって対処できることが示されていますが、ほとんどの関数型プログラミング言語では、中間表現を拡張して代数データ型を含めます。^[2]それでも、チャーチ符号化方式は部分評価や定理証明の自然な表現であるため、理論的な議論ではよく使用されます。^{[1]操作は、}より高位の型を使用して型付けでき、^[3]プリミティブ再帰に簡単にアクセスできます。^[1]関数が唯一のプリミティブデータ型であるという仮定により、多くの証明が合理化されます。 ${\displaystyle O(1)}$${\displaystyle O(n)}$${\displaystyle n}$

チャーチ符号化は完全ですが、表現上のみです。人々に表示するために、表現を一般的なデータ型に変換するには、追加の関数が必要です。チャーチの定理による同値の決定不能性のため、一般に 2 つの関数が外延的に等しいかどうかを判断することはできません。変換では、関数を何らかの方法で適用してそれが表す値を取得するか、その値をリテラル ラムダ項として検索します。ラムダ計算は通常、内包的等式を使用するものとして解釈されます。内包的等式と外延的等式の定義が異なるため、結果の解釈に 潜在的な問題があります。

チャーチ数値は、チャーチ符号化による自然数の表現です。自然数nを表す高階関数は、任意の関数をそのn倍の構成にマッピングする関数です。簡単に言えば、数値の「値」は、関数がその引数をカプセル化する回数に相当します。 ${\displaystyle f}$

${\displaystyle f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ 回}}}.\,}$

すべてのチャーチ数値は2つのパラメータを取る関数です。チャーチ数値0、1、2、 ... は、ラムダ計算で次のように定義されます。

0 で関数をまったく適用しないことから始めて、 1 で 関数を 1 回適用し、2 で 関数を 2 回適用し、3 で 関数を 3 回適用する、というように進めます。

${\displaystyle {\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}$

チャーチ数字3 は、任意の関数を値に 3 回適用するアクションを表します。指定された関数は、最初に指定されたパラメータに適用され、次に関数自体の結果に連続して適用されます。最終結果は数値 3 ではありません (指定されたパラメータがたまたま 0 で、関数が後続関数である場合を除く)。関数自体 (最終結果ではありません) がチャーチ数字3です。チャーチ数字3 は、単に何かを 3 回実行することを意味します。これは、「3 回」が何を意味するかを示す 明示的なデモンストレーションです。

数値の算術演算は、チャーチ数値の関数で表すことができます。これらの関数は、ラムダ計算で定義するか、ほとんどの関数型プログラミング言語で実装できます (ラムダ式から関数への変換を参照)。

加算関数は恒等式を使用します。 ${\displaystyle \operatorname {plus} (m,n)=m+n}$${\displaystyle f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))}$

${\displaystyle \operatorname {plus} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}$

後継関数はとβ 等価です。 ${\displaystyle \operatorname {succ} (n)=n+1}$${\displaystyle (\operatorname {plus} \ 1)}$

${\displaystyle \operatorname {succ} \equiv \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}$

乗算関数は恒等式を使用します。 ${\displaystyle \operatorname {mult} (m,n)=m*n}$${\displaystyle f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)}$

${\displaystyle \operatorname {mult} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}$

指数関数はチャーチ数の定義によって与えられます。定義で を代入すると、次の式が得られます。 ${\displaystyle \operatorname {exp} (m,n)=m^{n}}$${\displaystyle n\ h\ x=h^{n}\ x}$${\displaystyle h\to m,x\to f}$${\displaystyle n\ m\ f=m^{n}\ f}$

${\displaystyle \operatorname {exp} \ m\ n=m^{n}=n\ m}$

これはラムダ式を与える。

${\displaystyle \operatorname {exp} \equiv \lambda m.\lambda n.n\ m}$

機能は理解するのがより困難です。 ${\displaystyle \operatorname {pred} (n)}$

${\displaystyle \operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}$

チャーチ数値は関数をn回適用します。先行関数は、そのパラメータをn - 1回適用する関数を返す必要があります。これは、関数の最初の適用を省略する方法で初期化されるfとx の周りにコンテナを構築することによって実現されます。詳細な説明については、先行関数を参照してください。

減算関数は、先行関数に基づいて記述できます。

${\displaystyle \operatorname {minus} \equiv \lambda m.\lambda n.(n\operatorname {pred} )\ m}$

注記:

チャーチエンコーディングで使用される先行関数は、

${\displaystyle \operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}}$。

先行関数を構築するには、関数を 1 回少なく適用する方法が必要です。数値n は関数f を xにn回適用します。先行関数は、数値n を使用して関数をn -1回適用する必要があります。

先行関数を実装する前に、値をコンテナ関数にラップするスキームを次に示します。fとx の代わりに使用するincとinitという新しい関数を定義します。コンテナ関数はvalueと呼ばれます。表の左側には、incとinitに適用された数値nが表示されています。

${\displaystyle {\begin{array}{r|r|r}{\text{Number}}&{\text{Using init}}&{\text{Using const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)&\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x\\2&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}}$

一般的な繰り返し規則は、

${\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}$

コンテナから値を取得する関数（extractと呼ばれる）もある場合、

${\displaystyle \operatorname {extract} \ (\operatorname {value} \ v)=v}$

次に、extractを使用して、samenum関数を次のように定義します。

${\displaystyle \operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n}$

samenum関数は、本質的には役に立ちません。ただし、inc はfの呼び出しをそのコンテナ引数に委任するため、最初の適用時にinc が引数を無視する特別なコンテナを受け取り、 fの最初の適用をスキップするように設定できます。この新しい初期コンテナをconst と呼びます。上記の表の右側は、n inc constの展開を示しています。次に、同じ関数の式でinit をconstに置き換えると、先行関数が得られます。

${\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)}$

以下に説明するように、関数inc、init、const、value、extract は次のように定義できます。

${\displaystyle {\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}}$

これにより、 predのラムダ式は次のようになります。

${\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}$

Pred はペアを使用して定義することもできます。

${\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}}$

これはより単純な定義ですが、pred の表現はより複雑になります。 の展開は次のようになります。 ${\displaystyle \operatorname {pred} \operatorname {three} }$

${\displaystyle {\begin{aligned}\operatorname {pred} \operatorname {three} =&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} ))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {one} )))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {one} \ \operatorname {two} ))\\=&\ \operatorname {first} \ (\operatorname {pair} \ \operatorname {two} \ \operatorname {three} )\\=&\ \operatorname {two} \end{aligned}}}$

自然数の除算は次のように実装できる。^[4]

${\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0}$

計算には多くのベータ削減が必要です。削減を手動で行わない限り、これはそれほど重要ではありませんが、この計算を 2 回実行しない方が望ましいです。数値をテストするための最も単純な述語はIsZeroなので、条件を検討してください。 ${\displaystyle n-m}$

${\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}$

しかし、この条件は と等価であり、 ではありません。この表現を使用すると、上記の除算の数学的定義は、チャーチ数上の関数に変換され、 ${\displaystyle n\leq m}$${\displaystyle n<m}$

${\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}$

希望どおり、この定義には の呼び出しが 1 回あります。ただし、結果として、この式は の値を返します。 ${\displaystyle \operatorname {minus} \ n\ m}$${\displaystyle (n-1)/m}$

この問題は、 divideを呼び出す前にnに1を加算することで修正できます。divideの定義は次のようになります。

${\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)}$

division1 は再帰的な定義です。再帰を実装するには、Y コンビネータを使用できます。div byという新しい関数を作成します。

• 左側に${\displaystyle \operatorname {divide1} \rightarrow \operatorname {div} \ c}$
• 右側には${\displaystyle \operatorname {divide1} \rightarrow c}$

取得するため、

${\displaystyle \operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}$

それから、

${\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)}$

どこ、

${\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}$

${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}$

${\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}$

与える、

${\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)}$

またはテキストとして、λの代わりに\を使用する。

除算 = (\n.((\f.(\xx x) (\xf (xx))) (\c.\n.\m.\f.\x.(\d.(\nn (\x .(\a.\bb)) (\a.\ba)) d ((\f.\xx) fx) (f (cdmfx))) ((\m.\nn (\n.\f.\ xn (\g.\hh (gf)) (\ux) (\uu)) m) nm))) ((\n.\f.\x. f (nfx)) n))

例えば、9/3は次のように表されます。

割り算 (\f.\xf (f (f (f (f (f (f (f (f (f (f (f (f (f (fx))))))))) (\f.\xf (f (fx)))

ラムダ計算計算機を使用すると、上記の式は通常の順序で 3 に簡約されます。

\f.\xf (f (f (x)))

チャーチ数字を符号付き数に拡張する簡単な方法の1つは、正の値と負の値を表すチャーチ数字を含むチャーチペアを使用することです。^[5] 整数値は2つのチャーチ数字の差です。

自然数は次のように符号付き数に変換される。

${\displaystyle \operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0}$

否定は値を交換することによって実行されます。

${\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}$

整数値は、ペアの1つがゼロの場合に、より自然に表現されます。OneZero関数はこの条件を実現します。

${\displaystyle \operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}$

再帰はYコンビネータを使用して実装できます。

${\displaystyle \operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}$

${\displaystyle \operatorname {OneZero} =Y\operatorname {OneZ} }$

加算は数学的には次のように定義されます。

${\displaystyle x+y=[x_{p},x_{n}]+[y_{p},y_{n}]=x_{p}-x_{n}+y_{p}-y_{n}=(x_{p}+y_{p})-(x_{n}+y_{n})=[x_{p}+y_{p},x_{n}+y_{n}]}$

最後の式はラムダ計算では次のように翻訳される。

${\displaystyle \operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))}$

同様に減算も定義される。

${\displaystyle x-y=[x_{p},x_{n}]-[y_{p},y_{n}]=x_{p}-x_{n}-y_{p}+y_{n}=(x_{p}+y_{n})-(x_{n}+y_{p})=[x_{p}+y_{n},x_{n}+y_{p}]}$

与える、

${\displaystyle \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}$

乗算は次のように定義される。

${\displaystyle x*y=[x_{p},x_{n}]*[y_{p},y_{n}]=(x_{p}-x_{n})*(y_{p}-y_{n})=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]}$

最後の式はラムダ計算では次のように翻訳される。

${\displaystyle \operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}$

除算についても同様の定義がここに示されていますが、この定義では、各ペアの 1 つの値はゼロでなければなりません (上記のOneZeroを参照)。divZ関数を使用すると、ゼロ要素を持つ値を無視できます。

${\displaystyle \operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)}$

次に、 divZが次の式で使用されます。これは乗算の場合と同じですが、multがdivZに置き換えられます。

${\displaystyle \operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}$

有理数と計算可能な実数もラムダ計算でエンコードできます。有理数は符号付きの数のペアとしてエンコードできます。計算可能な実数は、実数値との差が、必要なだけ小さくできる数値だけ異なることを保証する制限プロセスによってエンコードできます。^{[6] [7]} 示されている参考文献では、理論的にはラムダ計算に変換できるソフトウェアについて説明しています。実数が定義されると、複素数は自然に実数のペアとしてエンコードされます。

上で説明したデータ型と関数は、あらゆるデータ型や計算をラムダ計算でエンコードできることを示しています。これがチャーチ＝チューリングのテーゼです。

現実世界の言語のほとんどは、マシン固有の整数をサポートしています。church 関数とunchurch関数は、非負整数とそれに対応する Church 数値を変換します。これらの関数は、ここではHaskellで提供されています。ここで、 は\ラムダ計算の λ に対応します。他の言語での実装も同様です。

タイプChurch a = ( a -> a ) -> a -> a          

church :: Integer -> Church Integer church 0 = \ f -> \ x -> x church n = \ f -> \ x -> f ( church ( n - 1 ) f x )     
       
           

unchurch ::教会整数->整数unchurch cn = cn ( + 1 ) 0     
      

Church ブール値は、ブール値trueとfalseの Church エンコードです。一部のプログラミング言語では、これをブール演算の実装モデルとして使用します。例としては、SmalltalkやPico などがあります。

ブール論理は選択肢として考えられます。trueとfalseの Church エンコードは、2 つのパラメータの関数です。

• true は最初のパラメータを選択します。
• false は2 番目のパラメータを選択します。

次の 2 つの定義は Church ブール値として知られています。

${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}$

この定義により、述語 (つまり、論理値を返す関数) が直接 if 節として動作できるようになります。ブール値を返す関数は、2 つのパラメータに適用され、最初のパラメータまたは 2 番目のパラメータのいずれかを返します。

${\displaystyle \operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {else-clause} }$

述語 x がtrueと評価された場合はthen 節に評価され、述語 x がfalseと評価された場合はelse節に評価されます。

trueとfalse は最初のパラメータまたは 2 番目のパラメータを選択するため、これらを組み合わせて論理演算子を提供できます。notの実装は複数可能であることに注意してください。

${\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}$

例:

${\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}}$

述語はブール値を返す関数です。最も基本的な述語は で、引数がチャーチ数値 の場合はを返し、引数がその他のチャーチ数値の場合は を返します。 ${\displaystyle \operatorname {IsZero} }$${\displaystyle \operatorname {true} }$${\displaystyle 0}$${\displaystyle \operatorname {false} }$

${\displaystyle \operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} }$

次の述語は、最初の引数が 2 番目の引数以下かどうかをテストします。

${\displaystyle \operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)}$、

アイデンティティのため、

${\displaystyle x=y\equiv (x\leq y\land y\leq x)}$

等価性のテストは次のように実装できます。

${\displaystyle \operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)}$

チャーチペアは、ペア（2組）型のチャーチエンコーディングです。ペアは、関数引数を取る関数として表されます。引数が与えられると、ペアの2つのコンポーネントに引数が適用されます。ラムダ計算の定義は、

${\displaystyle {\begin{aligned}\operatorname {pair} &\equiv \lambda x.\lambda y.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda x.\lambda y.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda x.\lambda y.y)\end{aligned}}}$

例えば、

${\displaystyle {\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b)\\=&(\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x)\\=&(\lambda x.\lambda y.x)\ a\ b=a\end{aligned}}}$

(不変の)リストはリストノードから構築されます。リストに対する基本的な操作は次のとおりです。

以下にリストの 4 つの異なる表現を示します。

• 各リスト ノードを 2 つのペアから構築します (空のリストを許可するため)。
• 各リスト ノードを 1 つのペアから構築します。
• 右折り畳み関数を使用してリストを表します。
• 一致式のケースを引数として取るスコットのエンコーディングを使用してリストを表現する

空でないリストは Church ペアによって実装できます。

• まず頭が入っています。
• 2番目には尾が含まれています。

ただし、これは「null」ポインタがないため、空のリストを表すものではありません。null を表すには、ペアを別のペアでラップして、次の 3 つの値を指定します。

• まず、ヌルポインター（空のリスト）。
• Second.Firstにはヘッドが含まれます。
• 2番目。2番目には末尾が含まれます。

この考え方を用いると、基本的なリスト操作は次のように定義できる。^[8]

nilノードでは、headとtail が空でないリストにのみ適用される 場合、 second はアクセスされません。

あるいは、^{[9]を定義する。}

${\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {first} \\\operatorname {tail} &\equiv \operatorname {second} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {false} )\operatorname {true} \end{aligned}}}$

最後の定義は一般的な定義の特別なケースである

${\displaystyle \operatorname {process-list} \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {head-and-tail-clause} )\operatorname {nil-clause} }$

チャーチペアを使用したエンコードの代替として、リストは右折り畳み関数で識別することによってエンコードできます。たとえば、3 つの要素 x、y、z のリストは、コンビネータ c と値 n に適用すると cx (cy (czn)) を返す高階関数によってエンコードできます。

${\displaystyle {\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda t.\operatorname {false} )\ \operatorname {true} \\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda t.h)\ \operatorname {false} \\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda t.\lambda g.g\ h\ (t\ c))\ (\lambda t.n)\ (\lambda h.\lambda t.t)\end{aligned}}}$

このリスト表現はSystem Fの型で指定できます。

代替表現としてスコット符号化があり、継続の考え方を利用してよりシンプルなコードを実現できる。^[10]（モーゲンセン・スコット符号化も参照）。

このアプローチでは、パターン マッチング式を使用してリストを観察できるという事実を利用します。たとえば、Scala表記法を使用すると、が空のリストとコンストラクタを持つlist型の値を表す場合、リストを検査して、リストが空の場合とリストが空でない場合 を計算できます。ListNilCons(h, t)nilCodeconsCode(h, t)

リスト一致{ case Nil => nilCode case Cons ( h , t ) => consCode ( h , t ) }  
            
      

は、 およびlistにどのように作用するかによって決まります。したがって、リストを、 および を引数として受け取る関数として定義すると、上記のパターン マッチの代わりに、次のように簡単に記述できます。 nilCodeconsCodenilCodeconsCode

${\displaystyle \operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode} }$

nに対応するパラメータを で表しnilCode、cに対応するパラメータを で表しますconsCode。空のリストは nil 引数を返すリストです。

${\displaystyle \operatorname {nil} \equiv \lambda n.\lambda c.\ n}$

h先頭と末尾を持つ空でないリストはt次のように与えられる。

${\displaystyle \operatorname {cons} \ h\ t\ \ \equiv \ \ \lambda n.\lambda c.\ c\ h\ t}$

より一般的には、選択肢を持つ代数データ型は、パラメータを持つ関数になります。番目のコンストラクタに引数がある場合、エンコーディングの対応するパラメータも引数を取ります。 ${\displaystyle m}$${\displaystyle m}$${\displaystyle i}$${\displaystyle n_{i}}$${\displaystyle n_{i}}$

スコット エンコーディングは型なしラムダ計算で実行できますが、型で使用するには再帰と型多態性を備えた型システムが必要です。この表現で要素型 E を持ち、型 C の値を計算するために使用されるリストには、次の再帰型定義があります。ここで、'=>' は関数型を示します。

type List = C => // nil 引数( E => List => C ) => // cons 引数C // パターンマッチングの結果   
                       
            
                         

任意の型を計算するために使用できるリストは、 を量化する型を持ちます。のジェネリック^{[明確化が必要]}Cなリストも、型引数として を取ります。EE

• ラムダ計算
• 型付き計算におけるチャーチ数字のシステム F
• モーゲンセン・スコット符号化
• フォン・ノイマンの順序数の定義— 自然数を集合として符号化する別の方法

• Stump, A. (2009). 「直接反射メタプログラミング」(PDF) . High-Order Symb Comput . 22 (2): 115–144. CiteSeerX  10.1.1.489.5018 . doi :10.1007/s10990-007-9022-0. S2CID  16124152.
• Cartwright, Robert. 「Church の数字とブール値の説明」(PDF)。Comp 311 — レビュー 2。ライス大学。
• Kemp, Colin (2007)。「§2.4.1 Church Naturals、§2.4.2 Church Booleans、第 5 章 TFP の導出テクニック」。実用的な「完全関数型プログラミング」の理論的基礎(PhD). クイーンズランド大学情報技術・電気工学部. pp. 14–17, 93–145. CiteSeerX  10.1.1.149.3505 . Church やその他の類似のエンコーディングについて、その導出方法や操作方法など、基本原理からすべて説明します。
• 教会数字のインタラクティブな例
• ラムダ計算ライブチュートリアル: ブール代数