[解決済み] なぜλ-calculusの最適評価器は数式を使わずに大きなモジュラーエクスペンジョンを計算できるのか？

疑問点

チャーチナンバーとは、自然数を関数として符号化したものです。

(\ 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つの教会番号を当てはめるだけで指数化することができます。つまり、2に4を適用すると、教会番号が得られます。 16 となり、また 2^4 . 明らかに、これはまったく実用的ではありません。教会数は直線的な量のメモリを必要とし、本当に、本当に遅いのです。次のような計算をすると 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 確かに でも、λ-calculatorはその結果を見つけるはずもなく、10^10を保存するのがやっとです。 科学のために、それを強調するようになりました。即座に答えが返ってきた 20^20%13 == 3 , 50^50%13 == 4 , 60^60%3 == 0 . 私は 外部ツール を使って検証する必要がありました。 Haskell自身は（整数のオーバーフローにより）計算することができませんでした。 (もちろん Ints ではなく Integer を使用した場合です!) 。その限界に挑戦したところ、これが答えとなり 200^200%31 :

5
{ iterations: 10351327, applications: 5175644, used_memory: 23754870 }

real    0m4.025s
user    0m3.686s
sys 0m0.341s

もし、宇宙上の原子1つにつき1つのコピーがあり、合計で1つの原子に1つのコンピュータがあったとしたら、教会番号を保存することはできません。 200^200 . このことから、私は自分のマックが本当にそんなに強力なのかどうか、疑問を持ちました。もしかしたら、最適評価器は、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))))))

特定のモジュール演算のアルゴリズムや公式を使ったわけではありません。 では、最適評価器はどのようにして正しい答えを導き出すことができるのでしょうか？

どのように解決するのか？

この現象は、Haskell スタイルの遅延評価 (または、この点ではそれほど遠くない通常の call-by-value) と Vuillemin-Lévy-Lamping-Kathail-Asperti-Guerrini-(et al...) "optimal" 評価で劇的に異なることがある共有ベータ削減ステップの量から来るものです。これは一般的な機能であり、この特定の例で使用できる算術式とは完全に独立しています。

共有とは、ラムダ項の表現を持つことで、1つのquot;ノード"が、表現した実際のラムダ項のいくつかの類似した部分を記述することができます。例えば、次のような項を表現することができます。

\x. x ((\y.y)a) ((\y.y)a)

を表す部分グラフが1つだけ存在する（有向無サイクル）グラフを使用しています。 (\y.y)a を表す部分グラフが1つだけ存在し、その部分グラフをターゲットとする2つのエッジがあります。Haskellの用語では、一度だけ評価する1つのサンクと、このサンクへの2つのポインタがあります。

Haskellスタイルのメモ化は、完全な部分項の共有を実装しています。このレベルの共有は有向無サイクルグラフで表現することができます。最適な共有にはこの制限がありません。それはまた、グラフ表現におけるサイクルを暗示する可能性がある "partial"サブタームを共有することができます。

これらの 2 つのレベルの共有の違いを見るために、項を考えてみましょう。

\x. (\z.z) ((\z.z) x)

Haskellのように共有が完全な部分項に制限されている場合、1つだけの \z.z のように、共有が完全な部分項に限定されている場合、 は一つですが、ここでの二つのベータ・レデックスは区別されます。 (\z.z) x であり、もうひとつは (\z.z) ((\z.z) x) であり、これらは等しい項ではないので、共有することはできません。 もし部分項の共有が許されるなら、部分項 (\z.z) [] (を共有することができるようになる（それは単に関数 \z.z のみならず、quot;関数 \z.z に適用される 何か を適用した場合)、一段階で評価されるのは、単に 何か と評価される。したがって、1つのノードだけが \z.z を2つの異なる引数に適用し、これらの2つの適用がちょうど1つのステップで削減されるようなグラフを持つことができます。このノードにはサイクルが存在することに注意してください。なぜなら、"first occurrence" の引数は、まさに "second occurrence" であるからです。 最後に、最適な共有で、(グラフを表す) \x. (\z.z) ((\z.z) x)) を表すグラフ）から、（結果を表すグラフ）である \x.x をベータ削減の一段階（と、いくつかの簿記）で表現します。これは基本的に、最適な評価器において起こることです (そして、グラフ表現が空間の爆発を防ぐものでもあります)。

少し拡張された説明のために、論文 弱い最適性、および共有の意味 (をご覧ください（興味のあるのは序章と4.1節、そして最後にある文献紹介の一部でしょう）。

あなたの例に戻ると、教会の整数上で動作する算術関数のコーディングは、最適な評価者が主流の言語よりも優れたパフォーマンスを発揮できる例のよく知られた鉱山（この文章では、よく知られているというのは、実際にはこれらの例を知っている一握りの専門家を意味します）の1つです。 このような例については、次の論文を参照してください。 安全な演算子。括弧は永遠に閉じられる AspertiとChroboczekの論文を見てください（ちなみに、ここではEALで型付けできない面白いラムダ項を見つけることができますので、このAsperti/Chroboczekの論文から始めて、オラクルに目を向けるように勧めています）。

あなた自身が言ったように、この種のエンコーディングはまったく実用的ではありませんが、それでも何が起こっているかを理解するための良い方法を示しています。そして、さらなる調査への挑戦で締めくくりたいと思います。これらの悪いと思われるエンコーディングでの最適な評価が、合理的なデータ表現での従来の評価と実際に同等である例を見つけることができるでしょうか。(私が知る限り、これは本当に未解決の問題です)。