ラムダ計算で型がどのように機能するかをよりよく把握しようとしています。確かに、型理論に関する多くのことは私の頭の中にあります。Lisp は動的に型付けされた言語ですが、それは型付けされていないラムダ計算にほぼ相当しますか? それとも、私が気付いていない「動的に型付けされたラムダ計算」のようなものがありますか?
4823 次
3 に答える
39
Lisp は動的に型付けされた言語ですが、それは型付けされていないラムダ計算にほぼ相当しますか?
はい、でも大まかに。「純粋な」型なしラムダ計算では、すべてが関数としてコーディングされます。(人気のある「チャーチ エンコーディング」とあまり人気のない「スコット エンコーディング」をググってください。) Lisp にはアトムや数値などの非関数データがあるため、これは「定数で拡張された型指定されていないラムダ計算」と見なされます。
もう 1 つの重要な違いは、評価の順序です。ラムダ計算項を削減するためのルールは、非常に非決定論的です。(Church-Rosser の定理という定理があり、物事が終了する限り、評価の順序は問題にならないという大雑把な言い方をしています。) 実際には、ラムダ項は通常、左端から外側にある「正規順序」縮約を使用して縮約されます。どんな削減戦略も終了します。これは、ベータ還元を行う前に常に引数を正規形に評価する Lisp とは大きく異なります。この評価順序は「値による呼び出し」と呼ばれます。
要約すると、Lisp は定数で拡張された、型指定されていない値渡しラムダ計算に対応しています。
于 2010-05-01T18:38:44.103 に答える
3
John McCarthyは、1960年4月の論文「記号式の再帰関数と機械によるそれらの計算、パートI」でLISPを紹介しました。次の段落は6ページからのものです。
e。関数とフォーム。数学では、数理論理学以外では、「関数」という単語を不正確に使用し、y 2 +xなどの形式に適用するのが一般的です。後で関数の式を使用して計算するため、関数と形式の区別と、この区別を表すための表記法が必要です。この区別とそれを説明するための表記法は、私たちが自明に逸脱しているものであり、Church[3]によって与えられています。
...
3. A. CHURCH、The Calculi of Lambda-Conversion（Princeton University Press、ニュージャージー州プリンストン、1941年）。
ラムダ計算に関するウィキペディアの記事には、教会の出版物の歴史があります。マッカーシーが参照した1941年の論文は、ウィキペディアの記事の紹介とは対照的に、型付きラムダ計算に関するもののようです。
Lispのlambdaキーワードは、類推によってのみラムダ計算を参照していると理解できます。Lispラムダ式は無名関数の一種です。
于 2010-05-01T15:16:59.270 に答える
-6
Lisp は「ラムダ計算」ではありません。「ラムダ計算」が何であるかはわかりません。
型システムによってラムダ計算を識別したい場合は、もちろん Lisp が独自のものです。Scheme より前の Lisp の 'lambda' キーワードは確かに大げさであり、Scheme の後ではそうであると言う余地もあります。「func」を使用するだけで、より謙虚になります。Lisp は主にリスト プロセッサであり、「ラムダ計算」ではありません
私はまた、これについて、A: 「関数型プログラミング」という用語が無意味である理由と、B: 「型システム」ではなく「ラムダ計算」について話すこともそうである理由を実証しようとするかなり広範な記事を書いたことがあります。
http://blog.nihilarchitect.net/archives/289/on-functional-programming/
また、Lisp では、すべての関数は事実上単一の引数であり、引数としてリストしか持てないことに注意してください。
于 2010-05-18T04:05:58.280 に答える