En "Tipos y lenguajes de programación", en la sección 6.1.2 se habla de un contexto de nomenclatura utilizado para numerar variables libres en expresiones lambda. Usando el esquema de ejemplo que han proporcionado, tanto λx.xb como λx.xx tendrán su representación de Bruijn como λ.00 cuando sean términos claramente diferentes. ¿Como funciona esto?¿Cómo usar un contexto de nomenclatura para encontrar índices de Bruijn de variables libres?
Como mencionaste, el libro utiliza un contexto de nomenclatura que asigna n variables gratuitas a los números del 0 al n-1. Sin embargo, si observa detenidamente los ejemplos del libro, notará que no utiliza esos números directamente para representar las variables. Por ejemplo, se representa como λw. y wλ. 4 0 a pesar de que la asignación para y es 3, 4. No
Lo que sucede aquí es que, añade la profundidad de anidamiento de la variable al número. Es decir. si una variable libre v está anidada en d lambdas, obtiene el índice Γ(v)+d, no solo Γ(v).
Así que en tu ejemplo mediante el contexto Γ {b -> 0}λx.xb se representaría como λ. 0 1, no λ. 0 0. Por lo tanto, no hay ambigüedad.
Creé un [intérprete basado en la web] (http://pure-fn.appspot.com/about) para un método basado en un índice más simple en un esfuerzo por aprender el funcionamiento del Cálculo Lambda. Agradecería sus comentarios al respecto. – dansalmo
¿Qué te hace pensar que la representación de la primera sería 'λ.00'. No creo que el primero pueda representarse en absoluto ya que 'b' no está vinculado a ninguna parte. – sepp2k
En la sección que mencioné, hablan sobre cómo se pueden representar las variables libres usando un _naming context_. – sanjoyd
Ah, ya veo. Escribiré una respuesta en breve. – sepp2k