評価による正規化

プログラミング言語のセマンティクスにおいて、評価による正規化（NBE）は、 λ計算における項の正規形を、その​​表示的意味論に依拠して得る方法である。まず項はλ項構造の表示的モデルに解釈され、次にその表示を具体化することによって、標準的な（β正規かつη長の）代表が抽出される。このような本質的に意味論的で還元を用いないアプローチは、λ項の内部でβ還元が許容される項書き換えシステムにおける還元として正規化を記述する、より伝統的な構文論的で還元に基づく記述とは異なる。

NBEは、最初に単純な型付きラムダ計算について記述されました。^{[ 1 ]}その後、ドメイン理論的アプローチを使用して、型なしラムダ計算^{[ 2 ]}などの弱い型システムと、 Martin-Löf型理論のいくつかのバリアントなどのよりリッチな型システムの両方に拡張されました。^{[ 3 ] [ 4 ] [ 5 ] [ 6 ]}

型が基本型（α）、関数型（→）、または積（×）である単純型ラムダ計算を考えます。これは、次のバッカス・ナウア記法で与えられます（→は通常通り右結合）。

(種類) τ  ::= α | τ ₁ → τ ₂ | τ1 × _τ2​

これらはメタ言語のデータ型として実装できます。たとえば、 Standard MLでは、次のように使用できます。

データ型ty =文字列の基本| ty * tyの矢印| ty * tyの積

用語は2つのレベルで定義されます。^{[ 7 ]}下位の構文レベル（動的レベルと呼ばれることもあります）は、正規化しようとする表現です。

（構文用語）s、t、…  ::= var x | lam ( x、t ) | app ( s、t ) | pair ( s、t ) | fst t | snd t

ここで、lam / app (それぞれpair / fst、snd ) は→ (それぞれ ×) の導入/削除形式であり、 xは変数です。これらの用語は、メタ言語において一階述語論理データ型として実装されることを意図しています。

データ型tm = var of string | lam of string * tm | app of tm * tm | pair of tm * tm | fst of tm | snd of tm

メタ言語における（閉じた）用語の指示的意味論は、構文の構成要素をメタ言語の特徴に基づいて解釈します。したがって、 lamは抽象化として、app は適用として解釈されます。構築される意味オブジェクトは次のとおりです。

（意味論的用語）S、T、…  ::= LAM（λ x . S x）| PAIR（S、T）| SYN t

意味論には変数や消去形式は含まれておらず、単に構文として表現されることに注意してください。これらの意味オブジェクトは、次のデータ型で表現されます。

データ型sem = LAM of ( sem -> sem ) | PAIR of sem * sem | SYN of tm

構文層と意味層の間を行き来する、型インデックス付き関数が2つあります。最初の関数（通常は↑ _τと表記）は構文という用語を意味に反映させ、2番目の関数（↓ ^τと表記）は意味を構文項として具体化します。これらの定義は相互に再帰的であり、以下のようになります。

${\displaystyle {\begin{aligned}\uparrow _{\alpha }t&=\mathbf {SYN} \ t\\\uparrow _{\tau _{1}\to \tau _{2}}v&=\mathbf {LAM} (\lambda S.\ \uparrow _{\tau _{2}}(\mathbf {app} \ (v,\downarrow ^{\tau _{1}}S)))\\\uparrow _{\tau _{1}\times \tau _{2}}v&=\mathbf {PAIR} (\uparrow _{\tau _{1}}(\mathbf {fst} \ v),\uparrow _{\tau _{2}}(\mathbf {snd} \ v))\\[1ex]\downarrow ^{\alpha }(\mathbf {SYN} \ t)&=t\\\downarrow ^{\tau _{1}\to \tau _{2}}(\mathbf {LAM} \ S)&=\mathbf {lam} \ (x,\downarrow ^{\tau _{2}}(S\ (\uparrow _{\tau _{1}}(\mathbf {var} \ x)))){\text{ where }}x{\text{ is fresh}}\\\downarrow ^{\tau _{1}\times \tau _{2}}(\mathbf {PAIR} \ (S,T))&=\mathbf {pair} \ (\downarrow ^{\tau _{1}}S,\downarrow ^{\tau _{2}}T)\end{aligned}}}$

これらの定義はメタ言語で容易に実装できます。

(* fresh_var : unit -> string *) val variable_ctr = ref ~1 fun fresh_var () = ( variable_ctr := 1 + !variable_ctr ; "v" ^ Int . toString ( !variable_ctr ))(* reflect : ty -> tm -> sem *) fun reflect ( Arrow ( a , b )) t = LAM ( fn S => reflect b ( app ( t , ( reify a S )))) | reflect ( Prod ( a , b )) t = PAIR ( reflect a ( fst t ), reflect b ( snd t )) | reflect ( Basic _) t = SYN t(* reify : ty -> sem -> tm *) and reify ( Arrow ( a , b )) ( LAM S ) = let val x = fresh_var () in lam ( x , reify b ( S ( reflect a ( var x )))) end | reify ( Prod ( a , b )) ( PAIR ( S , T )) = pair ( reify a S , reify b T ) | reify ( Basic _) ( SYN t ) = t

型の構造に関する帰納法によって、意味対象Sが型 τ の適切な型付けされた項sを表す場合、対象を具体化する (すなわち、↓ ^{τ S) とすると、} sの β-正規 η-長形式が生成されることが導かれる。したがって、残っているのは、構文項sから初期意味解釈S を構築することだけである。この操作は、 ∥ s ∥ _Γと表記され、Γ は束縛のコンテキストであり、項構造のみに関する帰納法によって進行する。

${\displaystyle {\begin{aligned}\|\mathbf {var} \ x\|_{\Gamma }&=\Gamma (x)\\\|\mathbf {lam} \ (x,s)\|_{\Gamma }&=\mathbf {LAM} \ (\lambda S.\ \|s\|_{\Gamma ,x\mapsto S})\\\|\mathbf {app} \ (s,t)\|_{\Gamma }&=S\ (\|t\|_{\Gamma }){\text{ where }}\|s\|_{\Gamma }=\mathbf {LAM} \ S\\\|\mathbf {pair} \ (s,t)\|_{\Gamma }&=\mathbf {PAIR} \ (\|s\|_{\Gamma },\|t\|_{\Gamma })\\\|\mathbf {fst} \ s\|_{\Gamma }&=S{\text{ where }}\|s\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\\\|\mathbf {snd} \ t\|_{\Gamma }&=T{\text{ where }}\|t\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\end{aligned}}}$

実装においては：

データ型ctx =空| ctx * (文字列* sem )の追加(* ルックアップ : ctx -> string -> sem *) fun lookup ( add ( remdr , ( y , value ))) x = if x = y then value else lookup remdr x(* 意味 : ctx -> tm -> sem *) fun meaning G t = case t of var x => lookup G x | lam ( x , s ) => LAM ( fn S => meaning ( add ( G , ( x , S ))) s ) | app ( s , t ) => ( case meaning G s of LAM S => S ( meaning G t )) | pair ( s , t ) => PAIR ( meaning G s , meaning G t ) | fst s => ( case meaning G s of PAIR ( S , T ) => S ) | snd t => ( case meaning G t of PAIR ( S , T ) => T )

網羅的ではないケースが多数存在することに注意してください。ただし、閉じた型付き項に適用した場合、これらの欠落ケースは発生しません。閉じた項に対する NBE 演算は次のようになります。

(* nbe : ty -> tm -> tm *) fun nbe a t = reify a (空のtを意味する)

その使用例として、SKK以下に定義する構文用語を考えてみましょう。

val K = lam ( "x" , lam ( "y" , var "x" )) val S = lam ( "x" , lam ( "y" , lam ( "z" , app ( app ( var "x" , var "z" ), app ( var "y" , var "z" ))))) val SKK = app ( app ( S , K ), K )

これは組み合わせ論理における恒等関数のよく知られた符号化である。これを恒等型で正規化すると次のようになる。

- nbe ( Arrow ( Basic "a" , Basic "a" )) SKK ; val it = lam ( "v0" , var "v0" ) : tm

結果は実際にはη-long形式であり、異なる恒等型で正規化することで容易に確認できます。

- nbe ( Arrow ( Arrow ( Basic "a" , Basic "b" ), Arrow ( Basic "a" , Basic "b" ))) SKK ; val it = lam ( "v1" , lam ( "v2" , app ( var "v1" , var "v2" ))) : tm

残余構文で名前の代わりにデ・ブルインレベルを使用するとreify、純粋関数になります。つまり、 は必要ありませんfresh_var。^{[ 8 ]}

残余項のデータ型は、正規形の残余項のデータ型にすることもできます。 の型reify（したがって の型nbe）から、結果が正規化されていることが明確になります。また、正規形のデータ型が型付きである場合、 の型reify（したがって の型nbe）から、正規化が型保存型であることが明確になります。^{[ 9 ]}

評価による正規化は、区切り制御演算子とを使用して、単純な型付きラムダ計算と和 ( +) ^{[ 7 ]}にも拡張されます。^{[ 10 ]}shiftreset

• MINLOGは、書き換えエンジンとしてNBEを使用する証明支援システムです。