1

ラムダ計算とチューリングマシンの等価性の証明、および証明の一般的な方法について、一般的な用語で誰かが私に説明できるのではないかと思っています。できるだけ平易な言葉で。

4

2 に答える 2

1

非常に基本的な用語で言えば、次の 2 つのことを証明するだけです。

  1. 任意のラムダ項について、同じことを計算するチューリング マシンがあります。
  2. どのチューリング マシンにも、同じことを計算するラムダ項があります。

もちろん、入力/出力の操作上の違いも考慮に入れる必要があるため、ここではいくつかの手を振る必要がありますが、ここでは触れません。

実際には、上記の 2 つの定理は建設的に証明されます。つまり、一方を他方に変換する機械的な方法を実際に与えることによって証明されます。したがって、基本的には、2 つのコンパイラーと、それらの正確性の証明を提供しています。

直観をよくするために、ラムダ計算とレジスタ マシンの間の同等性に関する類似の定理を考えてみてください。その設定では、実際のコンピューターの有限性を手放して、型指定されていないラムダ計算のインタープリターが一方向の証明になります。そして、ここで私が意味するのは、実行できる実際の具体的なプログラムです。たとえば、関数型プログラミング言語のコンパイラから型チェッカーを削除することによって (これには、ラムダ計算の型付きバージョンが組み込まれている必要があります。

次回GHCを実行するときは、この定理を考えてみてください!

于 2014-12-04T01:57:30.393 に答える