誰かがリダクションセマンティクスとPLTRedexの使用法をより簡単な言語で説明してください。
ありがとう。
質問する
2412 次
2 に答える
16
リダクションセマンティクスは、置換が不可能になるまで、式を同等の（できればより小さな）式に置き換えることを含む計算手法です。言語がチューリング完全である場合、置き換えを停止することのない式があります。
削減は通常、右矢印で示され、例で最もよく説明されます。
(3 + 7) + 5 --> 10 + 5 --> 15
これは、算術式の標準的な削減セマンティクスを示しています。式15をこれ以上減らすことはできません。
お役に立てれば。
于 2009-07-28T00:19:30.870 に答える
7
リダクションセマンティクスは、コンテキストセマンティクスと似ています（同じではない場合は？）。任意の式は、コンテキストとredexに分解できます。
Robert Harperのプログラミング言語の実用的な基礎（ドラフトPDFはここで入手可能）セクション9.3コンテキストセマンティクスはそれらを説明するのに適切な仕事をします。
例：
print 5+4
**context: print [], redex: 5+4
**evaluate redex: 9
**plug back into context
print 9
**context: [], redex: print 9
**evaluate redex: nil ==> 9
**plug back into context
nil
redexをコンテキストの「穴」に「貼り付け」て、次のように取得できます。print 5+4。評価はredexで行われます。式をコンテキスト+redexに分割し、redexを評価して新しい式を取得し、それをコンテキストにプラグインして、すすぎ、繰り返します。
ラムダ計算を評価する抽象マシンの知識を必要とする、もう少し複雑な例を次に示します。
(lambda x.x+1) 5
**context: [] 5, redex: (lambda x.x+1)
**evaluate redex: <(lambda x.x+1), {environment}> <- create a closure
**plug back into context
<(lambda x.x+1), {}> 5
**context: [], redex: <(lambda x.x+1), {}> 5
**evaluate redex: x+1 where x:=5
**plug back into context
x+1 where x:=5
**context: []+1, redex: x
**evaluate redex: 5 (since x:=5 in our environment)
*plug back into context
5+1...
6
編集：トリッキーな部分は、式をコンテキストとリデックスに分割する場所を認識することです。言語の操作的意味論（次に評価する必要のある式の「部分」）の知識が必要です。
于 2010-02-09T18:41:07.387 に答える