Normalización por evaluación

En la semántica de los lenguajes de programación , la normalización por evaluación (NBE) es un método para obtener la forma normal de los términos en el cálculo λ recurriendo a su semántica denotacional . Un término se interpreta primero en un modelo denotacional de la estructura del término λ, y luego se extrae un representante canónico (β-normal y η-largo) mediante la reificación de la denotación. Este enfoque esencialmente semántico, sin reducción, difiere de la descripción sintáctica más tradicional, basada en la reducción, de la normalización como reducciones en un sistema de reescritura de términos donde se permiten β-reducciones en el interior de los términos λ.

NBE se describió por primera vez para el cálculo lambda simplemente tipado . ^{[ 1 ]} Desde entonces se ha extendido tanto a sistemas de tipos más débiles como el cálculo lambda sin tipado ^{[ 2 ]} utilizando un enfoque de teoría de dominios , como a sistemas de tipos más ricos como varias variantes de la teoría de tipos de Martin-Löf . ^{[ 3 ] [ 4 ] [ 5 ] [ 6 ]}

Consideremos el cálculo lambda simplemente tipado , donde los tipos τ pueden ser tipos básicos (α), tipos de función (→) o productos (×), dados por la siguiente gramática de formas de Backus-Naur (→ asociando a la derecha, como es habitual):

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

Estos se pueden implementar como un tipo de dato en el metalenguaje; por ejemplo, para Standard ML , podríamos usar:

tipo de datos ty = Básico de cadena | Flecha de ty * ty | Producto de ty * ty

Los términos se definen en dos niveles. ^{[ 7 ]} El nivel sintáctico inferior (a veces llamado nivel dinámico ) es la representación que se pretende normalizar.

(Términos de sintaxis) s , t ,…  ::= var x | lam ( x , t ) | app ( s , t ) | pair ( s , t ) | fst t | snd t

Aquí, lam / app (respectivamente, pair / fst , snd ) son las formas intro / elim para → (respectivamente, ×), y x son variables . Estos términos están destinados a ser implementados como un tipo de dato de primer orden en el metalenguaje:

tipo de dato tm = var de cadena | lam de cadena * tm | app de tm * tm | pair de tm * tm | fst de tm | snd de tm

La semántica denotacional de los términos (cerrados) en el metalenguaje interpreta las construcciones de la sintaxis en términos de características del metalenguaje; así, lam se interpreta como abstracción, app como aplicación, etc. Los objetos semánticos construidos son los siguientes:

(Términos semánticos) S , T ,…  ::= LAM (λ x . S x ) | PAIR ( S , T ) | SYN t

Nótese que en la semántica no hay variables ni formas de eliminación; se representan simplemente como sintaxis. Estos objetos semánticos se representan mediante el siguiente tipo de dato:

tipo de datos sem = LAM de ( sem -> sem ) | PAIR de sem * sem | SYN de tm

Hay un par de funciones indexadas por tipo que se mueven entre la capa sintáctica y la semántica. La primera función, generalmente escrita como ↑ _τ , refleja la sintaxis del término en la semántica, mientras que la segunda reifica la semántica como un término sintáctico (escrito como ↓ ^τ ). Sus definiciones son mutuamente recursivas de la siguiente manera:

${\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}}}$

Estas definiciones se implementan fácilmente en el metalenguaje:

(* fresh_var : unidad -> cadena *) 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(* reificar: ty -> sem -> tm *) y reificar ( Flecha ( a , b )) ( LAM S ) = dejar val x = fresh_var () en lam ( x , reificar b ( S ( reflejar a ( var x )))) fin | reificar ( Prod ( a , b )) ( PAIR ( S , T )) = pair ( reificar a S , reificar b T ) | reificar ( Básico _) ( SYN t ) = t

Por inducción sobre la estructura de tipos, se deduce que si el objeto semántico S denota un término bien tipado s de tipo τ, entonces la reificación del objeto (es decir, ↓ ^τ S) produce la forma η-larga β-normal de s . Por lo tanto, solo queda construir la interpretación semántica inicial S a partir de un término sintáctico s . Esta operación, escrita ∥ s ∥ _Γ , donde Γ es un contexto de ligaduras, procede por inducción únicamente sobre la estructura del término:

${\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}}}$

En la implementación:

tipo de dato ctx = vacío | agregar de ctx * ( cadena * sem )(* búsqueda : ctx -> cadena -> sem *) fun búsqueda ( agregar ( remdr , ( y , valor ))) x = si x = y entonces valor sino búsqueda remdr x(* significado: ctx -> tm -> sem *) fun significado G t = caso t de var x => búsqueda G x | lam ( x , s ) => LAM ( fn S => significado ( agregar ( G , ( x , S ))) s ) | app ( s , t ) => ( caso significado G s de LAM S => S ( significado G t )) | pair ( s , t ) => PAIR ( significado G s , significado G t ) | fst s => ( caso significado G s de PAIR ( S , T ) => S ) | snd t => ( caso significado G t de PAIR ( S , T ) => T )

Cabe señalar que existen muchos casos no exhaustivos; sin embargo, si se aplica a un término cerrado bien tipificado, ninguno de estos casos faltantes se presenta. La operación NBE en términos cerrados es entonces:

(* nbe : ty -> tm -> tm *) fun nbe a t = reificar a ( significado vacío t )

Como ejemplo de su uso, considérese el término sintáctico SKKque se define a continuación:

val K = lam ( "x" , lam ( "y" , var "x" )) val S = lam ( "x" , lam ( "y" , lam ( "z" , aplicación ( aplicación ( var "x" , var "z" ), aplicación ( var "y" , var "z" ))))) val SKK = aplicación ( aplicación ( S , K ), K )

Esta es la codificación bien conocida de la función identidad en lógica combinatoria . Normalizarla en un tipo identidad produce:

- nbe ( Flecha ( Básico "a" , Básico "a" )) SKK ; val it = lam ( "v0" , var "v0" ) : tm

El resultado está en realidad en forma η-larga, como se puede ver fácilmente normalizándolo a un tipo de identidad diferente:

- nbe ( Flecha ( Flecha ( Básico "a" , Básico "b" ), Flecha ( Básico "a" , Básico "b" ))) SKK ; val it = lam ( "v1" , lam ( "v2" , app ( var "v1" , var "v2" ))) : tm

El uso de niveles de De Bruijn en lugar de nombres en la sintaxis residual crea reifyuna función pura en la que no hay necesidad de fresh_var. ^{[ 8 ]}

El tipo de datos de los términos residuales también puede ser el tipo de datos de los términos residuales en forma normal . El tipo de reify(y por lo tanto de nbe) deja claro que el resultado está normalizado. Y si el tipo de datos de las formas normales está tipado, el tipo de reify(y por lo tanto de nbe) deja claro que la normalización conserva el tipo. ^{[ 9 ]}

La normalización por evaluación también se escala al cálculo lambda tipado simple con sumas ( +), ^{[ 7 ]} utilizando los operadores de control delimitadosshift y reset. ^{[ 10 ]}

• MINLOG , un asistente de pruebas que utiliza NBE como motor de reescritura.