Normalizacja przez ocenę

W semantyce języka programowania normalizacja przez ocenę (NBE) to styl uzyskiwania normalnej postaci terminów w rachunku λ poprzez odwoływanie się do ich semantyki denotacyjnej . Termin jest najpierw interpretowany jako denotacyjny model struktury λ-terminowej, a następnie reprezentatywna reprezentacja kanoniczna (β-normalna i η-długa) jest wyodrębniana przez reifikację oznaczenie. Takie zasadniczo semantyczne, wolne od redukcji podejście różni się od bardziej tradycyjnego składniowego, opartego na redukcji opisu normalizacji jako redukcji w systemie przepisywania terminów , w którym β-redukcje są dozwolone głęboko w λ-termach.

NBE został po raz pierwszy opisany dla prostego rachunku lambda . Od tego czasu został rozszerzony zarówno na słabsze systemy typów , takie jak nieokreślony rachunek lambda przy użyciu podejścia opartego na teorii domeny , jak i na bogatsze systemy typów, takie jak kilka wariantów teorii typów Martina-Löfa .

Zarys

Rozważmy po prostu wpisany rachunek lambda , gdzie typy τ mogą być typami podstawowymi (α), typami funkcji (→) lub iloczynami (×), określonymi przez następującą gramatykę postaci Backusa-Naura (→ kojarzenie w prawo, jak zwykle):

(Typy) τ ::= α | τ ₁ → τ ₂ | τ ₁ × τ ₂

Można je zaimplementować jako typ danych w metajęzyku; na przykład dla Standard ML możemy użyć:

      
                  
                 typ danych  ty  =  Podstawowy  ciąg  znaków  |  Strzałka  ty  *  ty  |  _  Produkt  ty  *  ty  _

Terminy definiowane są na dwóch poziomach. Niższy syntaktyczny (czasami nazywany poziomem dynamicznym ) to reprezentacja, którą zamierza się znormalizować.

Tutaj lam / app (odp. pair / fst , snd ) to formy intro / elim dla → (odp. ×), a x to zmienne . Terminy te mają być zaimplementowane jako pierwszego rzędu w metajęzyku:

      
                        
                           typ  danych  tm  =  zmienna  łańcucha  |  lam  łańcucha  *  tm  |  _  aplikacja  tm  *  tm  |  _  para  tm  *  tm  |  _  pierwszy  z  tm  |  snd  z  tm

Semantyka denotacyjna terminów (zamkniętych) w metajęzyku interpretuje konstrukcje składni w kategoriach cech metajęzyka; zatem lam jest interpretowane jako abstrakcja, app jako aplikacja itp. Konstruowane obiekty semantyczne są następujące:

(Warunki semantyczne) S , T ,… ::= LAM (λ x . S x ) | PARA ( S , T ) | SYN t

Zauważ, że w semantyce nie ma zmiennych ani form eliminacji; są one reprezentowane po prostu jako składnia. Te obiekty semantyczne są reprezentowane przez następujący typ danych:

        
                   
                  typ danych  sem  =  LAM  z  (  sem  ->  sem  )  |  PARA  sem  *  sem  |  _  SYN  z  tm

Istnieje para funkcji indeksowanych typu, które poruszają się tam iz powrotem między warstwą składniową i semantyczną. Pierwsza funkcja, zwykle zapisywana ↑ _τ , odzwierciedla składnię terminu w semantyce, podczas gdy druga reifikuje semantykę jako termin syntaktyczny (zapisany jako ↓ ^τ ). Ich definicje są wzajemnie rekurencyjne w następujący sposób:

${\ Displaystyle {\ rozpocząć {wyrównane} \ uparrow _ {\ alfa} t & = \ mathbf {SYN} \ t \ \\ uparrow _ {\ tau _ {1} \ do \ 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 {PARA} (\uparrow _{\tau _{1}}(\mathbf {fst} \ v),\uparrow _{\ tau _{2}}(\mathbf {snd} \ v))\\[1ex]\strzałka w dół ^{\alpha }(\mathbf {SYN} \ t)&=t\\\strzałka w dół ^{\tau _{ 1}\to \tau _{2}}(\mathbf {LAM} \ S)&=\mathbf {lam} \ (x,\strzałka w dół ^{\tau _{2}}(S\ (\uparrow _{ \tau _{1}}(\mathbf {var} \ x)}}){\text{ gdzie }}x{\text{ jest świeże}}\\\downarrow ^{\tau _{1}\times \ tau _{2}}(\mathbf {PARA} \ (S,T))&=\mathbf {para} \ (\strzałka w dół ^{\tau _{1}}S,\strzałka w dół ^{\tau _{2 }}T)\end{wyrównane}}}$

Definicje te można łatwo zaimplementować w metajęzyku:

 
     
     
           
          

 
       
         (* zmienna_świeża : jednostka -> łańcuch *)  val  zmienna_zmienna  =  ref  ~1  zabawa  zmienna_świeża  ()  =  (  zmienna_zmienna  :=  1  +  !zmienna_zmienna  ;  "v"  ^  Int  .  toString  (  !zmienna_zmienna  ))  (* reflect : ty -> tm -> sem *)  zabawa  odbijać  (  Strzałka  (  a  ,  b  ))  t  =  LAM  (  fn          
         
               
        
         S  =>  odzwierciedlać  b  (  app  (  t  ,  (  reify  a  S  ))))  |  odbicie  (  Prod  (  a  ,  b  ))  t  =  PARA  (  odbicie  a  (  pierwsze  t  ),  odbicie  b  (  snd  t  ))  |  odzwierciedlać  (  Podstawowe  _)  t  =  SYN  t 

 
        
             
                 
       
        (* reify : ty -> sem -> tm *)  i  reify  (  Strzałka  (  a  ,  b  ))  (  LAM  S  )  =  niech  val  x  =  fresh_var  ()  in  lam  (  x  ,  reify  b  (  S  (  odzwierciedla  a  (  var  x  ))))  koniec  |  reify  (  Prod  (  a  ,  b     
             
           ))  (  PARA  (  S  ,  T  ))  =  para  (  reify  a  S  ,  reify  b  T  )  |  reify  (  Podstawowy  _)  (  SYN  t  )  =  t

Z indukcji struktury typów wynika, że jeśli obiekt semantyczny S denotuje dobrze wpisany termin s typu τ, to reifikacja obiektu (tj. ↓ ^τ S) daje β-normalną η-długą postać s . Pozostaje więc tylko skonstruować wyjściową interpretację semantyczną S z terminu syntaktycznego s . Operacja ta, zapisana ∥ s ∥ _Γ , gdzie Γ jest kontekstem powiązań, przebiega przez indukcję wyłącznie po strukturze terminowej:

${\ Displaystyle {\ rozpocząć {wyrównane} \|\ mathbf {var} \ x \ | _ {\ Gamma} & = \ Gamma (x) \\\|\ mathbf {lam} \ (x, s) \|_ {\Gamma}&=\mathbf {LAM} \ (\lambda S.\ \|s\|_{\Gamma,x\mapsto S})\\\|\mathbf {aplikacja} \ (s,t)\ |_{\Gamma }&=S\ (\|t\|_{\Gamma }){\text{ gdzie }}\|s\|_{\Gamma }=\mathbf {LAM} \ S\\\ |\mathbf {para} \ (s, t)\|_{\Gamma}&=\mathbf {PARA} \ (\|s\|_{\Gamma},\|t\|_{\Gamma}) \\\|\mathbf {fst} \ s\|_{\Gamma }&=S{\text{ gdzie }}\|s\|_{\Gamma }=\mathbf {PARA} \ (S,T) \\\|\mathbf {snd} \ t\|_{\Gamma }&=T{\text{ gdzie }}\|t\|_{\Gamma }=\mathbf {PARA} \ (S,T) \end{wyrównane}}}$

W realizacji:

     
                     

 
         
                

 
   typ danych  ctx  =  pusty  |  add  of  ctx  *  (  string  *  sem  )  (* wyszukiwanie : ctx -> string -> sem *)  zabawne  wyszukiwanie  (  add  (  remdr  ,  (  y  ,  value  )))  x  =  jeśli  x  =  y  następnie  wartość  else  szukaj  remdr  x  (* znaczenie: ctx -> tm -> sem *)  zabawne  znaczenie    
         
              
                     
              G  t  =  przypadek  t  z  var  x  =>  wyszukiwanie  G  x  |  lam  (  x  ,  s  )  =>  LAM  (  fn  S  =>  znaczenie  (  dodaj  (  G  ,  (  x  ,  S  )))  s  )  |  aplikacja  (  s  ,  t  )  =>  (  wielkość liter  ma znaczenie    
                                
                  
               
                          G  s  z  LAM  S  =>  S  (  co oznacza  G  t  ))  |  para  (  s  ,  t  )  =>  PARA  (  co oznacza  G  s  ,  co oznacza  G  t  )  |  fst  s  =>  (  wielkość liter  oznacza  G  s  z  PARY  (  S  ,  T  )  =>  S  ) 
               
                          |  snd  t  =>  (  wielkość liter  oznacza  G  t  z  PARY  (  S  ,  T  )  =>  T  )

Należy zauważyć, że istnieje wiele niewyczerpujących przypadków; jednak w przypadku zastosowania do zamkniętego , dobrze wpisanego terminu żaden z tych brakujących przypadków nigdy nie zostanie napotkany. Operacja NBE na zasadach zamkniętych to zatem:

 
           (* nbe : ty -> tm -> tm *)  fun  nbe  a  t  =  reify  a  (  co oznacza  puste  t  )

Jako przykład jego użycia rozważ termin składniowy SKK zdefiniowany poniżej:

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

Jest to dobrze znane kodowanie funkcji tożsamości w logice kombinatorycznej . Normalizowanie go w typie tożsamości daje:

        
         -  nbe  (  strzałka  (  podstawowe  „a”  ,  podstawowe  „a”  ))  SKK  ;  val  it  =  lam  (  "v0"  ,  var  "v0"  )  :  tm

Wynik jest w rzeczywistości w formie η-długiej, co można łatwo zobaczyć, normalizując go przy innym typie tożsamości:

              
          -  nbe  (  Strzałka  (  Strzałka  (  Podstawa  „a”  ,  Podstawa  „b”)  ),  Strzałka  (  Podstawa  „a”  ,  Podstawa  „b”  )))  SKK  ;  val  it  =  lam  (  "v1"  ,  lam  (  "v2"  ,  app  (  var  "v1"  ,  var  "v2"  )))    :  tm

Warianty

Używanie poziomów de Bruijna zamiast nazw w składni rezydualnej sprawia, że reify jest czysto funkcjonalne, ponieważ nie ma potrzeby fresh_var .

Typ danych terminów rezydualnych może być również typem danych terminów rezydualnych w postaci normalnej . Typ reify (a zatem nbe ) wyjaśnia następnie, że wynik jest znormalizowany. A jeśli typ danych normalnych form jest wpisany, typ reify (a zatem nbe ) wyjaśnia, że normalizacja zachowuje typ.

Normalizacja przez ocenę jest również skalowana do prostego rachunku lambda z sumami ( + ), przy użyciu rozdzielonych operatorów sterujących shift i reset .

Zobacz też

MINLOG , asystent sprawdzania , który używa NBE jako silnika przepisywania.