Representar variables enlazadas con una función desde usos hasta carpetas

11

El problema de representar las variables ligadas en la sintaxis, y en particular el de la sustitución para evitar la captura, es bien conocido y tiene una serie de soluciones: variables nombradas con equivalencia alfa, índices de Bruijn, anonimato local, conjuntos nominales, etc.

Pero parece haber otro enfoque bastante obvio, que sin embargo no he visto usado en ningún lado. Es decir, en la sintaxis básica tenemos solo un término "variable", escrito say , y luego le damos por separado una función que asigna cada variable a una carpeta en cuyo ámbito se encuentra. Entonces, a -term likeλλ

λx.(λy.xy)

se escribiría , y la función asignaría la primera a la primera y la segunda a la segunda . Por lo tanto, es como los índices de Bruijn, solo que en lugar de tener que "contar s" a medida que retrocede del término para encontrar la carpeta correspondiente, solo evalúa una función. (Si representa esto como una estructura de datos en una implementación, pensaría en equipar cada objeto de término variable con un puntero / referencia simple al objeto de término de carpeta correspondiente).λ λ λλ.(λ.)λλλ

Obviamente, esto no es sensato para escribir la sintaxis en una página para que los humanos la lean, pero tampoco lo son los índices de Bruijn. Me parece que tiene un sentido matemático perfecto y, en particular, hace que la sustitución para evitar la captura sea muy fácil: simplemente deje caer el término que está sustituyendo y tome la unión de las funciones de enlace. Es cierto que no tiene una noción de "variable libre", pero (de nuevo) tampoco los índices de Bruijn realmente; en cualquier caso, un término que contiene variables libres se representa como un término con una lista de carpetas de "contexto" al frente.

¿Me estoy perdiendo algo y hay alguna razón por la cual esta representación no funciona? ¿Hay problemas que lo hacen mucho peor que los demás que no vale la pena considerar? (El único problema que se me ocurre en este momento es que el conjunto de términos (junto con sus funciones vinculantes) no está definido inductivamente, pero eso no parece insuperable). ¿O hay realmente lugares donde se ha utilizado?

Mike Shulman
fuente
2
No sé sobre inconvenientes. ¿Quizás la formalización (por ejemplo, en un asistente de prueba) es más pesada? No estoy seguro ... Lo que sé es que no hay nada técnicamente incorrecto: esta forma de ver los términos lambda es la sugerida por su representación como redes de prueba, por lo que las personas conscientes de la red de pruebas (como yo) lo usan implícitamente todo el tiempo. Pero las personas conscientes de la prueba de red son muy raras :-) Entonces, tal vez es realmente una cuestión de tradición. PD: agregué un par de etiquetas poco relacionadas para que la pregunta sea más visible (con suerte).
Damiano Mazza
¿No es este enfoque equivalente a una sintaxis abstracta de orden superior (es decir, representar carpetas como funciones en el idioma del host)? En cierto sentido, el uso de una función como aglutinante establece punteros a aglutinantes implícitamente, en la representación de cierres.
Rodolphe Lepigre
2
@RodolpheLepigre No lo creo. En particular, entiendo que HOAS solo es correcto cuando la metateoría es bastante débil, mientras que este enfoque es correcto en una metateoría arbitraria.
Mike Shulman
3
Correcto, por lo que cada carpeta utiliza un nombre de variable único (dentro del árbol) (el puntero a él es uno automáticamente). Esta es la convención de Barendregt. Pero cuando sustituye, debe reconstruir (en C) lo que está sustituyendo para continuar teniendo nombres únicos. De lo contrario (en general), está utilizando los mismos punteros para múltiples subárboles y puede obtener una captura variable. La reconstrucción es el cambio de nombre alfa. ¿Presumiblemente ocurre algo similar dependiendo de los detalles de su codificación de árboles como conjuntos?
Dan Doel
3
@DanDoel Ah, interesante. Pensé que era tan obvio que no era necesario mencionar que colocarías una copia separada del término que se sustituye cada vez que aparece la variable por la que se sustituye; de lo contrario, ya no tendría un árbol de sintaxis . No se me ocurrió pensar en esta copia como un cambio de nombre alfa, pero ahora que lo señala, puedo verlo.
Mike Shulman

Respuestas:

11

Las respuestas de Andrej y Łukasz hacen buenos puntos, pero quería agregar comentarios adicionales.

Para hacer eco de lo que dijo Damiano, esta forma de representar la unión usando punteros es la sugerida por las redes de prueba, pero el primer lugar donde lo vi para los términos lambda fue en un viejo ensayo de Knuth:

  • Donald Knuth (1970). Ejemplos de semántica formal. En el Simposio sobre semántica de lenguajes algorítmicos , E. Engeler (ed.), Lecture Notes in Mathematics 188, Springer.

En la página 234, dibujó el siguiente diagrama (que llamó una "estructura de información") que representa el término :(λy.λz.yz)x

Diagrama de Knuth para $ (\ lambda y. \ Lambda z.yz) x $

Este tipo de representación gráfica de los términos lambda también se estudió de forma independiente (y más profundamente) en dos tesis a principios de la década de 1970, tanto por Christopher Wadsworth (1971, Semántica y pragmática del cálculo lambda ) como por Richard Statman (1974, Complejidad estructural). de pruebas ). Hoy en día, estos diagramas a menudo se denominan "gráficos λ" (ver, por ejemplo, este documento ).

Observe que el término en el diagrama de Knuth es lineal , en el sentido de que cada variable libre o ligada ocurre exactamente una vez; como han mencionado otros, hay problemas y elecciones no triviales que se deben hacer al tratar de extender este tipo de representación a -términos lineales.

Por otro lado, para términos lineales, ¡creo que es genial! La linealidad excluye la necesidad de copiar, por lo que obtienes -equivalencia y sustitución "gratis". Estas son las mismas ventajas que HOAS, y en realidad estoy de acuerdo con Rodolphe Lepigre en que hay una conexión (si no exactamente una equivalencia) entre las dos formas de representación: hay un sentido en el que estas estructuras gráficas pueden interpretarse naturalmente como diagramas de cuerdas , que representa endomorfismos de un objeto reflexivo en una bicategoría cerrada compacta (di una breve explicación de eso aquí ).α

Noam Zeilberger
fuente
10

No estoy seguro de cómo se representaría su función de variable a carpeta y para qué propósito le gustaría usarla. Si está utilizando indicadores de retroceso, entonces, como Andrej señaló, la complejidad computacional de la sustitución no es mejor que el cambio de nombre alfa clásico.

De su comentario sobre la respuesta de Andrej, infiero que, hasta cierto punto, está interesado en compartir. Puedo proporcionar alguna entrada aquí.

En un cálculo lambda tipificado típico, el debilitamiento y la contracción, al contrario de otras reglas, no tienen sintaxis.

Γt:TΓ,x:At:TW
Γ,x1:A,x2:At:TΓ,x:At:TC

Agreguemos una sintaxis:

Γt:TΓ,x:AWx(t):TW
Γ,x1:A,x2:At:TΓ,x:ACxx1,x2(t):TC

a b , cCab,c() está 'usando' la variable y vinculando las variables . Me enteré de esa idea de una de las " Implementaciones netas de interacción de reducción cerrada " de Ian Mackie .ab,c

Con esa sintaxis, cada variable se usa exactamente dos veces, una donde está vinculada y otra donde se usa. Esto nos permite distanciarnos de una sintaxis particular y ver el término como un gráfico donde las variables y los términos son aristas.

Desde la complejidad algorítmica, ahora podemos usar punteros no de una variable a un aglutinante, sino de un aglutinante a una variable y tener sustituciones en un tiempo constante.

Además, esta reformulación nos permite rastrear el borrado, la copia y el intercambio con más fidelidad. Uno puede escribir reglas que copien (o borren) de forma incremental un término mientras comparten subterms. Hay muchas formas de hacer eso. En algunos entornos restringidos, las victorias son bastante sorprendentes .

Esto se está acercando a los temas de redes de interacción, combinadores de interacción, sustitución explícita, lógica lineal, evaluación óptima de Lamping, gráficos compartidos, lógicas ligeras y otros.

Todos estos temas son muy emocionantes para mí y con mucho gusto daría referencias más específicas, pero no estoy seguro de si algo de esto es útil para usted y cuáles son sus intereses.

Łukasz Lew
fuente
6

Su estructura de datos funciona, pero no será más eficiente que otros enfoques porque necesita copiar todos los argumentos en cada reducción beta, y debe hacer tantas copias como apariciones de la variable enlazada. De esta manera sigues destruyendo el intercambio de memoria entre subterms. Combinado con el hecho de que está proponiendo una solución no pura que implica manipulaciones de puntero y, por lo tanto, es muy propensa a errores, probablemente no valga la pena.

¡Pero estaría encantado de ver un experimento! Puede tomarlo lambdae implementarlo con su estructura de datos (OCaml tiene punteros, se llaman referencias ). Más o menos, solo tienes que reemplazar syntax.mly norm.mlcon tus versiones. Eso es menos de 150 líneas de código.

Andrej Bauer
fuente
¡Gracias! Admito que realmente no estaba pensando mucho en las implementaciones, sino principalmente en poder hacer pruebas matemáticas sin preocuparme por la contabilidad de Bruijn o el cambio de nombre alfa. Pero, ¿hay alguna posibilidad de que una implementación pueda retener algo de memoria compartida al no hacer copias "hasta que sea necesario", es decir, hasta que las copias diverjan entre sí?
Mike Shulman
β(λx.e1)e2e1e2
2
Con respecto a las pruebas matemáticas, ahora he pasado por una gran cantidad de formalización de la sintaxis de teoría de tipos, mi experiencia es que se obtienen ventajas cuando generalizamos la configuración y la hacemos más abstracta, no cuando la hacemos más concreta. Por ejemplo, podemos parametrizar la sintaxis con "cualquier buena forma de tratar el enlace". Cuando lo hacemos, es más difícil cometer errores. También he formalizado la teoría de tipos con índices de Bruijn. No es demasiado terrible, especialmente si tienes tipos dependientes que te impiden hacer cosas sin sentido.
Andrej Bauer
2
Para agregar, he trabajado en una implementación que utiliza básicamente esta técnica (pero con enteros y mapas únicos, no punteros), y realmente no la recomendaría. Definitivamente tuvimos muchos errores en los que extrañamos la clonación de las cosas correctamente (en gran parte debido a tratar de evitarla cuando sea posible). Pero creo que hay un documento de algunas personas de GHC donde lo defienden (creo que utilizaron una función hash para generar los nombres únicos). Puede depender de lo que estás haciendo exactamente. En mi caso, fue inferencia de tipo / comprobación, y parece bastante poco adecuado allí.
Dan Doel
@MikeShulman Para algoritmos de complejidad razonable (Elemental) (en gran medida copia y borrado), la llamada 'parte abstracta' de la reducción óptima de Lamping no es hacer copias hasta que sea necesario. La parte abstracta también es la parte no controvertida en comparación con el algoritmo completo que requiere algunas anotaciones que pueden dominar el cálculo.
Łukasz Lew
5

Otras respuestas son principalmente sobre temas de implementación. Ya que mencionas tu principal motivación para hacer pruebas matemáticas sin demasiada contabilidad, aquí está el problema principal que veo con eso.

Cuando dice "una función que asigna cada variable a una carpeta en cuyo ámbito se encuentra": ¡el tipo de salida de esta función es seguramente un poco más sutil que eso! Específicamente, la función debe tomar valores en algo como "los ligantes del término en consideración", es decir, un conjunto que varía según el término (y obviamente no es un subconjunto de un conjunto ambiental más grande de ninguna manera útil). Por lo tanto, en la sustitución, no puede simplemente "tomar la unión de las funciones de enlace": también tiene que reindexar sus valores, de acuerdo con algún mapa de carpetas en los términos originales a carpetas en el resultado de la sustitución.

Estas reindexaciones seguramente deberían ser "rutinarias", en el sentido de que razonablemente podrían ser barridas debajo de la alfombra, o bien empaquetadas en términos de algún tipo de funcionalidad o naturalidad. Pero lo mismo es cierto de la contabilidad involucrada en el trabajo con variables con nombre. Entonces, en general, me parece probable que haya al menos tanta contabilidad involucrada con este enfoque como con enfoques más estándar.

Sin embargo, aparte de esto, es un enfoque conceptual muy atractivo, y me encantaría verlo cuidadosamente elaborado. Me imagino que podría arrojar una luz diferente sobre algunos aspectos de la sintaxis que los enfoques estándar.

PLL
fuente
Hacer un seguimiento del alcance de cada variable requiere realmente la contabilidad, ¡pero no salte a la conclusión de que siempre se debe restringir a una sintaxis bien definida! Las operaciones como la sustitución y la reducción beta pueden definirse incluso en términos de alcance limitado, y sospecho que si uno quisiera formalizar este enfoque (que de nuevo, es realmente el enfoque de las redes de prueba / "gráficos λ") en un asistente de prueba, primero se implementarían las operaciones más generales, y luego se demostraría que preservan la propiedad de tener un buen alcance.
Noam Zeilberger
(Estuve de acuerdo en que vale la pena probarlo ... aunque no me sorprendería que alguien ya lo haya hecho en el contexto de la formalización de pruebas de redes / gráficos λ.)
Noam Zeilberger,
5

λLazy.t

En general, creo que es una representación genial, pero implica cierta contabilidad con punteros, para evitar romper enlaces vinculantes. Supongo que sería posible cambiar el código para usar campos mutables, pero la codificación en Coq sería menos directa. Todavía estoy convencido de que esto es muy similar a HOAS, aunque la estructura del puntero se hace explícita. Sin embargo, la presencia de Lazy.timplica que es posible que algún código sea evaluado en el momento equivocado. Este no es el caso en mi código, ya que solo puede ocurrir una sustitución de una variable con una variable a la forcevez (y no una evaluación, por ejemplo).

(* Representation of a term of the λ-calculus. *)
type term =
  | FVar of string      (* Free variable  *)
  | BVar of bvar        (* Bound variable *)
  | Appl of term * term (* Application    *)
  | Abst of abst        (* Abstraction    *)

(* A bound variable is a pointer to the corresponding binder. *)
and bvar = abst

(* A binder is represented as its body in which the bound variable points to
   the binder itself. Note that we need to use a thunk to be able to work
   underneath a binder (for substitution, evaluation, ...). A name can be
   given for easy printing, but no renaming is done. Only “visual capture”
   can happen since pointers are established the right way, even if names
   can clash. *)
and abst = { body : term Lazy.t ; name : string }

(* Terms can be built with recursive values for abstractions. *)

(* Krivine's notation is used for application (function in parentheses). *)

let id    : term = (* λx.x        *)
  Abst(let rec id = {body = lazy (BVar(id)); name = "x"} in id)

let idid  : term = (* (λx.x) λx.x *)
  Appl(id, id)

let delta : term = (* λx.(x) x *)
  Abst(let rec d = {body = lazy (Appl(BVar(d), BVar(d))); name = "x" } in d)

let weird : term = (* (λx.x) λy.(λx.(x) x) (C) y *)
  Appl(id, Abst(let rec x = {body = lazy (Appl(delta, Appl(FVar("C"),
    BVar(x)))); name = "y"} in x))

let omega : term = (* (λx.(x) x) λx.(x) x *)
  Appl(delta, delta)

(* Printing function is immediate. *)
let rec print : out_channel -> term -> unit = fun oc t ->
  match t with
  | FVar(x)   -> output_string oc x
  | BVar(x)   -> output_string oc x.name
  | Appl(t,u) -> Printf.fprintf oc "(%a) %a" print t print u
  | Abst(f)   -> Printf.fprintf oc "λ%s.%a" f.name print (Lazy.force f.body)

(* Substitution of variable [x] by [v] in the term [t]. Occurences of [x] in
   [t] are identified using physical equality ([BVar] case). The subtle case
   is [Abst], because we need to reestablish the physical link between the
   binder and the variable it binds. *)
let rec subst_var : bvar -> term -> term -> term = fun x t v ->
  match t with
  | FVar(_)   -> t
  | BVar(y)   -> if y == x then v else t
  | Appl(t,u) -> Appl(subst_var x t v, subst_var x u v)
  | Abst(f)   ->
      (* First compute the new body. *)
      let fv = subst_var x (Lazy.force f.body) v in
      (* Reestablish the physical link, using [subst_var] itself again. This
         requires a second traversal of the term. We could probably do both
         at once, but who cares the complexity is linear in [t] anyway. *)
      Abst(let rec g = {f with body = lazy (subst_var f fv (BVar(g)))} in g)

(* Actual substitution function. *)
let subst : abst -> term -> term = fun f v ->
  subst_var f (Lazy.force f.body) v

(* Normalization function (all the way, even under binders). *)
let rec eval : term -> term = fun t ->
  match t with
  | Appl(t,u) ->
      begin
        let v = eval u in
        match eval t with
        | Abst(f) -> eval (subst f v)
        | t       -> Appl(t,v)
      end
  | Abst(f)   ->
      (* Actual computation in the body. *)
      let fv = eval (Lazy.force f.body) in
      (* Here, the physical link is reestablished, but it is important to note
         that the computation of evaluation is done above. So the part below
         only takes a linear time in the size of the normal form of the body
         of the abstraction. *)
      Abst(let rec g = {f with body = lazy (subst_var f fv (BVar(g)))} in g)
  | _         ->
      t

let _ = Printf.printf "id         = %a\n%!" print id
let _ = Printf.printf "eval id    = %a\n%!" print (eval id)

let _ = Printf.printf "idid       = %a\n%!" print idid
let _ = Printf.printf "eval idid  = %a\n%!" print (eval idid)

let _ = Printf.printf "delta      = %a\n%!" print delta
let _ = Printf.printf "eval delta = %a\n%!" print (eval delta)

let _ = Printf.printf "omega      = %a\n%!" print omega
(* The following obviously loops. *)
(*let _ = Printf.printf "eval omega = %a\n%!" print (eval omega)*)

let _ = Printf.printf "weird      = %a\n%!" print weird
let _ = Printf.printf "eval weird = %a\n%!" print (eval weird)

(* Output produced:
id         = λx.x
eval id    = λx.x
idid       = (λx.x) λx.x
eval idid  = λx.x
delta      = λx.(x) x
eval delta = λx.(x) x
omega      = (λx.(x) x) λx.(x) x
weird      = (λx.x) λy.(λx.(x) x) (C) y
eval weird = λy.((C) y) (C) y
*)
Rodolphe Lepigre
fuente