チャーチ数は自然数を関数としてエンコードしたものです。
(\ f x → (f x)) -- church number 1
(\ f x → (f (f (f x)))) -- church number 3
(\ f x → (f (f (f (f x))))) -- church number 4
2 つのチャーチ数を単に適用するだけで、うまく累乗することができます。つまり、4 を 2 に適用すると、チャーチ数16または が得られます2^4。明らかに、これはまったく実用的ではありません。チャーチ数は線形量のメモリを必要とし、非常に低速です。GHCI が10^10すぐに正しい答えを出すようなものを計算するには、何時間もかかり、いずれにしてもコンピュータのメモリに収まりきりません。
最近、最適 λ 評価器の実験を行っています。テスト中に、誤って最適 λ 計算機に次のように入力してしまいました。
10 ^ 10 % 13
それは累乗ではなく乗算のはずでした。絶望して永遠に実行されているプログラムを中止しようと指を動かす前に、プログラムは私の要求に応えました。
3
{ iterations: 11523, applications: 5748, used_memory: 27729 }
real 0m0.104s
user 0m0.086s
sys 0m0.019s
「バグアラート」が点滅したので、Google にアクセスして10^10%13 == 3実際に確認しました。しかし、λ 計算機はその結果を見つけることが想定されておらず、10^10 をほとんど保存できません。私は科学のためにそれを強調し始めました。それは即座に私に答えました20^20%13 == 3、、50^50%13 == 4。60^60%3 == 0私は使わなければなりませんでした外部ツールこれらの結果を検証するには、
Haskell 自体では計算できなかった (整数オーバーフローのため) ため、次の式を実行する必要が
あります (もちろん、Int ではなく Integer を使用する場合は計算できます)。これを限界まで押し上げると、次の式に対する答えが返ってきました200^200%31。
5
{ iterations: 10351327, applications: 5175644, used_memory: 23754870 }
real 0m4.025s
user 0m3.686s
sys 0m0.341s
宇宙の各原子に対して宇宙のコピーが 1 つずつあり、合計で各原子に対してコンピュータが 1 台ずつあるとしたら、教会の数を保存することはできません200^200。このため、私の Mac が本当にそれほど高性能なのか疑問に思いました。おそらく、最適な評価器は、Haskell の遅延評価と同じ方法で、不要な分岐をスキップして答えに直接到達できるのでしょう。これをテストするために、λ プログラムを Haskell にコンパイルしました。
data Term = F !(Term -> Term) | N !Double
instance Show Term where {
show (N x) = "(N "++(if fromIntegral (floor x) == x then show (floor x) else show x)++")";
show (F _) = "(λ...)"}
infixl 0 #
(F f) # x = f x
churchNum = F(\(N n)->F(\f->F(\x->if n<=0 then x else (f#(churchNum#(N(n-1))#f#x)))))
expMod = (F(\v0->(F(\v1->(F(\v2->((((((churchNum # v2) # (F(\v3->(F(\v4->(v3 # (F(\v5->((v4 # (F(\v6->(F(\v7->(v6 # ((v5 # v6) # v7))))))) # v5))))))))) # (F(\v3->(v3 # (F(\v4->(F(\v5->v5)))))))) # (F(\v3->((((churchNum # v1) # (churchNum # v0)) # ((((churchNum # v2) # (F(\v4->(F(\v5->(F(\v6->(v4 # (F(\v7->((v5 # v7) # v6))))))))))) # (F(\v4->v4))) # (F(\v4->(F(\v5->(v5 # v4))))))) # ((((churchNum # v2) # (F(\v4->(F(\v5->v4))))) # (F(\v4->v4))) # (F(\v4->v4))))))) # (F(\v3->(((F(\(N x)->F(\(N y)->N(x+y)))) # v3) # (N 1))))) # (N 0))))))))
main = print $ (expMod # N 5 # N 5 # N 4)
1これは( )を正しく出力します5 ^ 5 % 4が、それ以上の値を入力する10^10とスタックし、仮説が排除されます。
の私が使用した最適な評価者これは 160 行の長さの最適化されていない JavaScript プログラムで、指数係数の計算は一切含まれていません。また、私が使用したラムダ計算の係数関数も同様に単純です。
(λab.(b(λcd.(c(λe.(d(λfg.(f(efg)))e))))(λc.(c(λde.e)))(λc.(a(b(λdef.(d(λg.(egf))))(λd.d)(λde.(ed)))(b(λde.d)(λd.d)(λd.d))))))
特定のモジュラー演算アルゴリズムや式は使用しませんでした。では、最適な評価者はどのようにして正しい答えに到達できるのでしょうか?
ベストアンサー1
この現象は、共有されるベータ削減ステップの量から生じます。これは、Haskell スタイルの遅延評価 (または、この点ではそれほど遠くない通常の値渡し) と、Vuillemin-Lévy-Lamping-Kathail-Asperti-Guerrini (その他) の「最適な」評価では大幅に異なる可能性があります。これは一般的な機能であり、この特定の例で使用できる算術式とはまったく無関係です。
共有とは、ラムダ項の表現を持ち、1つの「ノード」が、表現する実際のラムダ項の複数の類似部分を記述できることを意味します。たとえば、次の項を表現できます。
\x. x ((\y.y)a) ((\y.y)a)
を表すサブグラフが 1 つだけ出現し、そのサブグラフをターゲットとする 2 つのエッジがある (有向非巡回) グラフを使用します(\y.y)a。Haskell の用語では、1 回だけ評価する 1 つのサンクと、このサンクへの 2 つのポインターがあります。
Haskell スタイルのメモ化は、完全なサブタームの共有を実装します。このレベルの共有は、有向非巡回グラフで表すことができます。最適な共有にはこの制限はありません。グラフ表現に循環を意味する可能性のある「部分的な」サブタームも共有できます。
これら2つのレベルの共有の違いを理解するには、次の用語を考えてみましょう。
\x. (\z.z) ((\z.z) x)
Haskell の場合のように共有が完全な部分項に制限されている場合、 は 1 つしか出現しない可能性があります\z.zが、ここでの 2 つのベータ リデックスは別個になります。1 つは で(\z.z) x、もう 1 つは であり(\z.z) ((\z.z) x)、これらは等しい項ではないため共有できません。部分的な部分項の共有が許可されている場合は、部分項(\z.z) [](関数 だけでなく、「に適用された\z.z関数」)を共有できるようになります。\z.z何か）、これは1ステップで評価され、何か、この引数が何であれ。したがって、1 つのノードだけが\z.z2 つの異なる引数への 2 つの適用を表し、これらの 2 つの適用を 1 つのステップで簡約できるグラフを作成できます。このノードにはサイクルがあることに注目してください。これは、「最初の発生」の引数がまさに「2 番目の発生」であるためです。最後に、最適な共有により、ベータ削減の 1 つのステップ (およびいくつかのブックキーピング) で、 (表すグラフ)\x. (\z.z) ((\z.z) x))から (表すグラフ) の結果に移行でき\x.xます。これは基本的に、最適な評価で発生することです (また、グラフ表現はスペース爆発を防ぐものでもあります)。
もう少し詳しい説明については、論文をご覧ください。弱い最適性と共有の意味(あなたが興味を持っているのは、序論とセクション 4.1、そしておそらく最後の参考文献のポインターの一部です)。
あなたの例に戻ると、チャーチ整数で動作する算術関数のコーディングは、最適評価器が主流の言語よりも優れたパフォーマンスを発揮できる「よく知られた」例の宝庫の1つです（この文でよく知られているというのは、実際には少数の専門家がこれらの例を知っているという意味です）。そのような例をもっと知りたい場合は、論文をご覧ください。安全なオペレーター: 括弧は永久に閉じるAsperti と Chroboczek による (ちなみに、ここでは EAL 型付けできない興味深いラムダ項が見つかります。そのため、この Asperti/Chroboczek の論文から始めて、オラクルを調べることをお勧めします)。
あなた自身が言ったように、この種のエンコードはまったく実用的ではありませんが、それでも何が起こっているかを理解するための優れた方法です。そして、さらなる調査のための課題で締めくくりたいと思います。これらの悪いと思われるエンコードの最適評価が、合理的なデータ表現の従来の評価と実際に同等である例を見つけることができるでしょうか? (私の知る限り、これは本当に未解決の問題です)。