En la semántica del lenguaje de programación , la normalización por evaluación (NBE) es un estilo de obtener la forma normal de los términos en el cálculo λ apelando 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) reificando la denotación. Este enfoque esencialmente semántico difiere de la descripción sintáctica más tradicional de la normalización como reducciones en un sistema de reescritura de términos donde las reducciones β se permiten profundamente dentro 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 tipo [2] utilizando un enfoque teórico de dominio , como a sistemas de tipos más ricos como varias variantes de la teoría de tipos de Martin-Löf . [3] [4]
Esquema
Considere el cálculo lambda simplemente tipado , donde los tipos τ pueden ser tipos básicos (α), tipos de función (→) o productos (×), dado por la siguiente gramática de la forma Backus-Naur (→ asociando a la derecha, como de costumbre):
- (Tipos) τ :: = α | τ 1 → τ 2 | τ 1 × τ 2
Estos se pueden implementar como un tipo de datos en el metalenguaje; por ejemplo, para ML estándar , podríamos usar:
tipo de datos ty = Básico de cadena | Flecha de ty * ty | Prod of ty * ty
Los términos se definen en dos niveles. [5] 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 ) | aplicación ( s , t ) | par ( s , t ) | fst t | snd t
Aquí lam / app (resp. Pair / fst , snd ) son las formas intro / elim para → (resp. ×), yx son variables . Estos términos están pensados para ser implementados de primer orden en el metalenguaje:
tipo de datos tm = var de cadena | lam de cadena * tm | aplicación de tm * tm | par de tm * tm | primero de tm | snd de tm
La semántica denotacional de 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 ) | PAREJA ( S , T ) | SYN t
Tenga en cuenta que no hay variables ni formas de eliminación en la semántica; se representan simplemente como sintaxis. Estos objetos semánticos están representados por el siguiente tipo de datos:
tipo de datos sem = LAM de ( sem -> sem ) | PAR de sem * sem | SYN de tm
Hay un par de funciones indexadas por tipo que se mueven hacia adelante y hacia atrás entre la capa sintáctica y semántica. La primera función, generalmente escrita ↑ τ , refleja el término sintaxis en la semántica, mientras que la segunda reifica la semántica como un término sintáctico (escrito como ↓ τ ). Sus definiciones son recursivas entre sí de la siguiente manera:
Estas definiciones se implementan fácilmente en el metalenguaje:
(* reflejar: ty -> tm -> sem *) divertido reflejar ( Flecha ( a , b )) t = LAM ( fn S => reflejar b ( app t ( reificar a S ))) | reflejar ( Prod ( a , b )) t = PAR ( reflejar a ( fst t )) ( reflejar b ( snd t )) | reflejar ( Básico _) t = SYN t (* reificar: ty -> sem -> tm *) y reificar ( Flecha ( a , b )) ( LAM S ) = dejar x = fresh_var () en Lam ( x , reificar b ( S ( reflejar a ( var x ) ))) final | reify ( Prod ( a , b )) ( PAIR S T ) = Pair ( reify a S , reify b T ) | reify ( 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 s bien tipificado de tipo τ, entonces reificar el objeto (es decir, ↓ τ S) produce la forma β-normal η-larga de s . Todo lo que queda es, por tanto, 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 enlaces, procede por inducción únicamente en la estructura del término:
En la implementación:
(* significado: ctx -> tm -> sem *) divertido 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 que significa G s de LAM S => S (que significa G t )) | par ( s , t ) => PAR (que significa G s , que significa G t ) | fst s => ( caso que significa G s de PAR ( S , T ) => S ) | snd t => ( caso que significa G t de PAR ( S , T ) => T )
Tenga en cuenta que hay muchos casos no exhaustivos; sin embargo, si se aplica a un término cerrado bien mecanografiado, nunca se encuentra ninguno de estos casos faltantes. La operación NBE en términos cerrados es entonces:
(* nbe: ty -> tm -> tm *) fun nbe a t = reify a (que significa t vacío )
Como ejemplo de su uso, considere el término sintáctico SKK
definido a continuación:
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 )
Ésta es la conocida codificación de la función de identidad en lógica combinatoria . Normalizarlo en un tipo de identidad produce:
- nbe ( Flecha ( Básico "a" , Básico "a" )) SKK ; val it = lam ( "v0" , var "v0" ) : tm
El resultado es en realidad en forma η-long, como se puede ver fácilmente normalizándolo en 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
Ver también
- MINLOG , un asistente de pruebas que utiliza NBE como motor de reescritura.
Referencias
- ^ Berger, Ulrich; Schwichtenberg, Helmut (1991). "Una inversa de la evaluación funcional para el cálculo λ tipado". LICS .
- ^ Filinski, Andrzej; Rohde, Henning Korsholm (2004). "Una cuenta denotacional de la normalización no tipificada por evaluación" . FOSSACS .
- ^ Abel, Andreas; Aehlig, Klaus; Dybjer, Peter (2007). "Normalización por evaluación para la teoría de tipos de Martin-Löf con un universo" (PDF) . MFPS .
- ^ Abel, Andreas; Coquand, Thierry; Dybjer, Peter (2007). "Normalización por evaluación para la teoría de tipos de Martin-Löf con juicios de igualdad tipificados" (PDF) . LICS .
- ^ Danvy, Olivier (1996). "Evaluación parcial dirigida a tipografía " ( PostScript comprimido con gzip ) . POPL : 242-257.