評価による正規化

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

NBEは、最初に単純型付きラムダ計算のために記述されました。[1]その後、ドメイン理論的アプローチを用いた型なしラムダ計算[2]などのより弱い型システムや、 Martin-Löf型理論のいくつかの変種などのより豊富な型システムにも拡張されました。[3] [4] [5] [6]

概要

単純型付きラムダ計算を考えてみましょう。ここで、型 τ は基本型 (α)、関数型 (→)、または積 (×) であり、次のバッカス-ナウア形式文法で与えられます (→ いつものように右に結合します)。

(種類) τ ::= α | τ 1 → τ 2 | τ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）は→ （それぞれ × ）のintro / elim形式であり、 xは変数です。これらの項は、メタ言語において 一階データ型として実装されることを意図しています。

データ型 tm  = 文字列のvar  |文字列のlam * tm | tm * tmのapp | tm * tmのpair | tmのfst | tmのsnd

メタ言語の（閉じた）用語の表示的意味論は、構文の構成をメタ言語の機能の観点から解釈します。つまり、 lamは抽象として、app はアプリケーションとして解釈されます。構築される意味オブジェクトは次のとおりです。

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

セマンティクスには変数や消去形式は存在せず、単に構文として表現されることに注意してください。これらのセマンティックオブジェクトは、以下のデータ型で表現されます。 

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

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

↑ α t ＝ S はい 北   t ↑ τ 1 → τ 2 v ＝ L あ M （ λ S 。   ↑ τ 2 （ 1つの p p   （ v 、 ↓ τ 1 S ） ） ） ↑ τ 1 × τ 2 v ＝ P あ 私 R （ ↑ τ 1 （ f s t   v ） 、 ↑ τ 2 （ s n d   v ） ） ↓ α （ S はい 北   t ） ＝ t ↓ τ 1 → τ 2 （ L あ M   S ） ＝ l 1つの メートル   （ × 、 ↓ τ 2 （ S   （ ↑ τ 1 （ v 1つの r   × ） ） ） ）  どこ  ×  新鮮です ↓ τ 1 × τ 2 （ P あ 私 R   （ S 、 T ） ） ＝ p 1つの 私 r   （ ↓ τ 1 S 、 ↓ τ 2 T ） {\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 *)
および 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 ∥ Γと表記され（Γ は束縛のコンテキスト）、項構造のみに基づく帰納法によって実行される。

‖ v a r   x ‖ Γ = Γ ( x ) ‖ l a m   ( x , s ) ‖ Γ = L A M   ( λ S .   ‖ s ‖ Γ , x ↦ S ) ‖ a p p   ( s , t ) ‖ Γ = S   ( ‖ t ‖ Γ )  where  ‖ s ‖ Γ = L A M   S ‖ p a i r   ( s , t ) ‖ Γ = P A I R   ( ‖ s ‖ Γ , ‖ t ‖ Γ ) ‖ f s t   s ‖ Γ = S  where  ‖ s ‖ Γ = P A I R   ( S , T ) ‖ s n d   t ‖ Γ = T  where  ‖ t ‖ Γ = P A I R   ( S , T ) {\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 )の追加      

(* lookup : ctx -> string -> sem *) 
fun  lookup  ( add  ( remdr ,  ( y ,  value )))  x  =  
      if  x  =  y  then  value  else  lookup  remdr  x

(* 意味 : ctx -> tm -> sem *) 
fun 意味 G  t  = 
      case  t  of 
        var  x  =>  lookup  G  x 
      |  lam  ( x 、 s )  =>  LAM  ( fn  S  => 意味 ( add  ( G 、 ( x 、 S )))  s ) 
      |  app  ( s 、 t )  =>  ( case 意味 G  s  of 
                         LAM  S  =>  S  (意味 G  t )) 
      |  pair  ( s 、 t )  =>  PAIR  (意味 G  s 、 意味 G  t ) 
      |  fst  s  =>  ( case 意味 G  s  of 
                    PAIR  ( S 、 T )  =>  S ) 
      |  snd  t  =>  ( case 意味 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  (矢印 (基本 "a" 、 基本 "a" ))  SKK ; 
val  it  =  lam  ( "v0" 、var  "v0" )  :  tm

結果は実際にはη-long形式であり、別のアイデンティティ型で正規化すると簡単にわかります。 

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

変種

残差構文で名前の代わりにde Bruijnレベルを使用するとreify、 が不要になるという点で純粋関数になりますfresh_var。[8]

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

評価による正規化は、区切り制御演算子とを使用して、単純に型付けされたラムダ計算（+）にも拡張できます。 [ 7] [ 10] shiftreset

参照

参考文献

  1. ^ Berger, Ulrich; Schwichtenberg, Helmut (1991). 「型付きλ計算の評価関数の逆」LICS .
  2. ^ Filinski, Andrzej; Rohde, Henning Korsholm (2005). 「評価による型なし正規化の表示的説明」.ソフトウェア科学と計算構造の基礎 (FOSSACS) . 第10巻. doi : 10.7146/brics.v12i4.21870 .
  3. ^ Coquand, Thierry; Dybjer, Peter (1997). 「直観主義モデルの構築と正規化証明」.コンピュータサイエンスにおける数学的構造. 7 (1): 75– 94. doi :10.1017/S0960129596002150.
  4. ^ Abel, Andreas; Aehlig, Klaus; Dybjer, Peter (2007). 「1つの宇宙を持つMartin-Löf型理論の評価による正規化」(PDF) . MFPS .
  5. ^ Abel, Andreas; Coquand, Thierry; Dybjer, Peter (2007). 「型付き等価性判定を伴うMartin-Löf型理論の評価による正規化」(PDF) . LICS .
  6. ^ Gratzer, Daniel; Sterling, Jon; Birkedal, Lars (2019). 「様相依存型理論の実装」(PDF) . ICFP .
  7. ^ ab Danvy, Olivier (1996). 「型指示部分評価」（gzip圧縮PostScript） . POPL（FTP）. pp.  242– 257. [デッド FTP リンク] (ドキュメントを表示するには、ヘルプ:FTP を参照してください)
  8. ^ Filinski, Andrzej. 「型指向部分評価の意味論的説明」『宣言型プログラミングの原則と実践』 . doi : 10.7146/brics.v6i17.20074 .
  9. ^ Danvy, Olivier; Rhiger, Morten; Rose, Kristoffer (2001). 「型付き抽象構文による評価による正規化」. Journal of Functional Programming . 11 (6): 673– 680. doi :10.1017/S0956796801004166.
  10. ^ Danvy, Olivier; Filinski, Andrzej (1990). 「制御の抽象化」. LISPと関数型プログラミング. pp.  151– 160. doi : 10.1145/91556.91622 . ISBN 0-89791-368-X. S2CID  6426191。
Retrieved from "https://en.wikipedia.org/w/index.php?title=Normalisation_by_evaluation&oldid=1300130726"