Árbol de Böhm

En el estudio de la semántica denotacional del cálculo lambda , los árboles de Böhm , ^[a] los árboles de Lévy-Longo , ^[1]^[2]^[b] y los árboles de Berarducci ^[3] son objetos matemáticos (potencialmente infinitos) similares a árboles que capturan el "significado" de un término hasta un conjunto de términos "sin significado".

Motivación

Una forma sencilla de leer el significado de un cálculo es considerarlo como un procedimiento mecánico que consiste en un número finito de pasos que, cuando se completa, produce un resultado. En particular, considerando el cálculo lambda como un sistema de reescritura , cada paso de reducción beta es un paso de reescritura, y una vez que no hay más reducciones beta, el término está en forma normal . Podríamos así, siguiendo ingenuamente la sugerencia de Church , ^[4] decir que el significado de un término es su forma normal, y que los términos sin una forma normal no tienen sentido. Por ejemplo, los significados de I = λx.xy son ambos . Esto funciona para cualquier subconjunto fuertemente normalizador del cálculo lambda, como un cálculo lambda tipificado .I II

Sin embargo, esta asignación ingenua de significado es inadecuada para el cálculo lambda completo. El término Ω =(λx.x x)(λx.x x)no tiene una forma normal y, de manera similar, el término no tiene una forma normal. Pero la aplicación , donde denota el término lambda estándar , se reduce solo a sí mismo, mientras que la aplicación se reduce con reducción de orden normal a , por lo tanto tiene un significado. Vemos, por tanto, que no todos los términos no normalizantes son equivalentes. Nos gustaría decir que es menos significativo que porque la aplicación a un término puede producir un resultado, pero la aplicación no.X=λx.xΩΩ (K I)K λx.λy.xX (K I)IΩXXΩ

Los árboles de Böhm también pueden aplicarse en el contexto del cálculo lambda infinitario, que incluye términos infinitamente grandes. En este contexto, el término N N, donde , se reduce tanto a como a , por lo que también hay problemas con la confluencia de la normalización. ^[5]N = λx.I(xx)I (I (...))Ω

Conjuntos de términos sin sentido

La construcción general está parametrizada por un conjunto de términos sin sentido , que se requieren para satisfacer los siguientes axiomas: ^[6]^[7] ${\estilo de visualización U}$

Actividad de raíz: Todo término con actividad de raíz está en . Un término es activo de raíz si para todo existe un redex tal que . ${\estilo de visualización U}$ ${\estilo de visualización M}$ $M{\stackrel {*}{\to }}N$ $(\lambda xP)Q$ $N{\stackrel {*}{\to }}(\lambda xP)Q$
Cierre bajo β-reducción: Para todo , si entonces . $M\en U$ $M{\stackrel {*}{\to }}N$ $N\en U$
Cierre bajo sustitución: Para todas las sustituciones y , . $M\en U$ ${\estilo de visualización \sigma}$ $M\sigma \en U$
Superposición: Para todos , . $\lambda xM\en U$ $(\lambda xM)N\in U$
Indiscernibilidad: Para todo , si se puede obtener de reemplazando un conjunto de subtérminos disjuntos por pares en con otros términos de , entonces si y solo si . ${\estilo de visualización M,N}$ ${\estilo de visualización N}$ ${\estilo de visualización M}$ ${\estilo de visualización U}$ ${\estilo de visualización U}$ $M\en U$ $N\en U$
Clausura bajo β-expansión. Para todo , si , entonces . Algunas definiciones lo dejan de lado, pero es útil. ^[8] $N\en U$ $M{\stackrel {*}{\to }}N$ $M\en U$

Hay infinitos conjuntos de términos sin significado, pero los más comunes en la literatura son: ^[9]

El conjunto de términos sin cabeza forma normal
El conjunto de términos sin cabeza débil forma normal
El conjunto de términos activos en la raíz, es decir, los términos sin forma normal superior o forma normal en la raíz. Como se supone que existe actividad en la raíz, este es el conjunto más pequeño de términos sin significado.

Téngase en cuenta que Ωes raíz-activa y, por lo tanto, para cada conjunto de términos sin sentido . $\mathbf {\Omega } \en U$ ${\estilo de visualización U}$

Términos λ⊥

El conjunto de términos λ con ⊥ (abreviado como términos λ⊥) se define de manera coinductiva mediante la gramática . Esto corresponde al cálculo lambda infinitario estándar más los términos que contienen . La reducción beta en este conjunto se define de la manera estándar. Dado un conjunto de términos sin sentido , también definimos una reducción al final: si y , entonces . Los términos λ⊥ se consideran entonces como un sistema de reescritura con estas dos reglas; gracias a la definición de términos sin sentido, este sistema de reescritura es confluente y normalizante. ^[7] $M=\bot \mid x\mid (\lambda xM)\mid (MM)$ ${\estilo de visualización \bot}$ ${\estilo de visualización U}$ $M[\bot \mapsto \mathbf {\Omega } ]\en U$ $M\neq \bot$ $M\to \bot$

El "árbol" tipo Böhm para un término puede entonces obtenerse como la forma normal del término en este sistema, posiblemente en un sentido infinitario "en el límite" si el término se expande infinitamente.

Árboles de Böhm

Los árboles de Böhm se obtienen considerando los términos λ⊥ donde el conjunto de términos sin sentido consiste en aquellos sin forma normal de cabeza . Más explícitamente, el árbol de Böhm BT( M ) de un término lambda M se puede calcular de la siguiente manera: ^[10]

BT( M ) es , si M no tiene forma normal de cabeza ${\estilo de visualización \bot}$
$\mathrm {BT} (M)=\lambda x_{1}.\lambda x_{2}.\ldots \lambda x_{n}.y\mathrm {BT} (M_{1})\ldots \mathrm {BT} (M_{m})$ , si se reduce en un número finito de pasos a la forma normal de la cabeza ${\estilo de visualización M}$ $\lambda x_{1}.\lambda x_{2}.\ldots \lambda x_{n}.yM_{1}\ldots M_{m}$

Por ejemplo, .BT(Ω)=⊥, BT(I)=I, and BT(λx.xΩ)=λx.x⊥

Determinar si un término tiene una forma normal de cabeza es un problema indecidible . Barendregt introdujo una noción de un árbol de Böhm "efectivo" que es computable, con la única diferencia de que los términos sin forma normal de cabeza no se marcan con . ^[11] ${\estilo de visualización \bot}$

Nótese que calcular el árbol de Böhm es similar a encontrar una forma normal para M. Si M tiene una forma normal, el árbol de Böhm es finito y tiene una correspondencia simple con la forma normal. Si M no tiene una forma normal, la normalización puede "hacer crecer" algunos subárboles infinitamente, o puede quedar "atascado en un bucle" al intentar producir un resultado para una parte del árbol, lo que produce árboles infinitarios y términos sin sentido respectivamente. Dado que el árbol de Böhm puede ser infinito, el procedimiento debe entenderse como aplicado de forma correcursiva o como tomando el límite de una serie infinita de aproximaciones.

Árboles de Lévy-Longo

Los árboles de Lévy-Longo se obtienen considerando los términos λ⊥ donde el conjunto de términos sin sentido consiste en aquellos sin forma normal de cabeza débil . Más explícitamente, el árbol de Lévy-Longo LLT( M ) de un término lambda M se puede calcular de la siguiente manera: ^[10]

LLT( M ) es , si M no tiene forma normal de cabeza débil. ${\estilo de visualización \bot}$
Si se reduce a la forma normal de la cabeza débil , entonces . ${\estilo de visualización M}$ $yM_{1}\ldots M_{m}$ $\mathrm {LLT} (M)=y\mathrm {LLT} (M_{1})\ldots \mathrm {LLT} (M_{m})$
Si se reduce a la forma normal de la cabeza débil , entonces / ${\estilo de visualización M}$ $\lambda xN$ $\mathrm {LLT} (M)=\lambda x.\mathrm {LLT} (N)$

Árboles de Berarducci

Los árboles de Berarducci se obtienen considerando los términos λ⊥, donde el conjunto de términos sin sentido consiste en los términos activos en la raíz. Más explícitamente, el árbol de Berarducci BerT( M ) de un término lambda M se puede calcular de la siguiente manera: ^[10]

BerT( M ) es , si M es raíz activa. ${\estilo de visualización \bot}$
Si se reduce a un término , entonces . ${\estilo de visualización M}$ $\lambda xN$ $\mathrm {BerT} (M)=\lambda x.\mathrm {BerT} (N)$
Si se reduce a un término donde no se reduce a ninguna abstracción , entonces . ${\estilo de visualización M}$ ${\estilo de visualización NP}$ ${\estilo de visualización N}$ $\lambda xQ$ $\mathrm {BerT} (M)=\mathrm {BerT} (N)\mathrm {BerT} (P)$

Notas

^ por Sangiorgi y Walker (2003, p. 493), introducido en Barendregt (1977) y llamado así por un teorema de Corrado Böhm
^ acuñado en Ong (1988), por Sangiorgi y Walker (2003, p. 511)

Referencias

^ Levy, Jean-Jacques (1975). "Una interpretación algebraica del cálculo λβK y un cálculo λ etiquetado". λ-Calculus and Computer Science Theory . Apuntes de clase en informática. Vol. 37. págs. 147–165. doi :10.1007/BFb0029523. ISBN 3-540-07416-3.
^ Longo, Giuseppe (agosto de 1983). "Modelos teóricos de conjuntos de λ-cálculo: teorías, expansiones, isomorfismos". Anales de lógica pura y aplicada . 24 (2): 153–188. doi : 10.1016/0168-0072(83)90030-1 .
^ Berarducci, Alessandro (1996). "Cálculo λ infinito y modelos no sensibles" (PDF) . Lógica y álgebra . Nueva York: Marcel Dekker. pp. 339–377. ISBN. 0824796063. Consultado el 23 de septiembre de 2007 .
^ Church, Alonzo (1941). Los cálculos de conversión lambda . Princeton University Press. pág. 15. ISBN 0691083940.
^ Severi y de Vries 2011, pag. 1.
^ Kennaway, Richard; van Oostrom, Vincent; de Vries, Fer-Jan (1996). "Términos sin sentido en la reescritura". Programación algebraica y lógica . Apuntes de clase en informática. Vol. 1139. págs. 254–268. CiteSeerX 10.1.1.37.3616 . doi :10.1007/3-540-61735-3_17. ISBN. 978-3-540-61735-8.
^ ab Severi y de Vries 2011, pág. 5.
^ Severi y de Vries 2011, págs. 4-5.
^ Severi y de Vries 2011, pag. 2.
^ abc Severi & de Vries 2011, pág. 6.
^ Barendregt, Henk P. (2012). El cálculo lambda: su sintaxis y semántica . Londres: College Publications. pp. 219–221. ISBN 9781848900660.

Huet, Gérard; Laulhère, H. (1997). "Transductores de estados finitos como árboles de Böhm regulares" (PDF) . En Abadi, M.; Ito, T. (eds.). Aspectos teóricos del software informático . LNCS. Vol. 1281. Springer. págs. 604–610. CiteSeerX 10.1.1.110.7910 . doi :10.1007/BFb0014570. ISBN. 978-3-540-69530-1.
Gérard Huet (1998). "Árboles Böhm normales" (PDF) . Matemáticas. Estructura. En comp. Ciencia . 8 (6): 671–680. CiteSeerX 10.1.1.123.475 . doi :10.1017/S0960129598002643. S2CID 15752309.
Ong, C.-H. Luke (31 de mayo de 1988). El cálculo lambda perezoso: una investigación sobre los fundamentos de la programación funcional (PDF) (PhD). Universidad de Londres. OCLC 31204528 . Consultado el 23 de septiembre de 2022 .
Sangiorgi, Davide; Walker, David (16 de octubre de 2003). El cálculo Pi: una teoría de los procesos móviles . Cambridge University Press. ISBN 978-0-521-54327-9.
Barendregt, Henk P. (1977). "El cálculo lambda sin tipos". Manual de lógica matemática . Estudios de lógica y fundamentos de las matemáticas. Vol. 90. págs. 1091–1132. doi :10.1016/S0049-237X(08)71129-7. hdl : 2066/17225 . ISBN . 9780444863881. Número de identificación del sujeto 25828519.
Severi, Paula; de Vries, Fer-Jan (2011). "Descomposición de la red de conjuntos sin sentido en el cálculo lambda infinito" (PDF) . Lógica, lenguaje, información y computación . Apuntes de clase en informática. Vol. 6642. págs. 210–227. doi :10.1007/978-3-642-20920-8_22. ISBN 978-3-642-20919-2. Recuperado el 23 de septiembre de 2022 .