Á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) con forma de árbol que capturan el "significado" de un término hasta cierto conjunto de términos "sin significado".

Una forma sencilla de leer el significado de un cálculo es considerarlo como un procedimiento mecánico que consta de un número finito de pasos que, al completarse, 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 . Por lo tanto, podríamos, 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 forma normal carecen de significado. Por ejemplo, los significados de${\displaystyle \mathbf {I} =\lambda xx}$y${\displaystyle \mathbf {II} }$son ambos${\displaystyle \mathbf {I} }$Esto funciona para cualquier subconjunto fuertemente normalizador del cálculo lambda, como un cálculo lambda tipado .

Esta asignación ingenua de significado es, sin embargo, inadecuada para el cálculo lambda completo. El término${\displaystyle \mathbf {\Omega } =(\lambda x.xx)(\lambda x.xx)}$no tiene una forma normal, y de manera similar el término${\displaystyle \mathbf {X} =\lambda xx\mathbf {\Omega } }$no tiene una forma normal. Pero la aplicación${\displaystyle \mathbf {\Omega } (\mathbf {KI} )}$, dónde${\displaystyle \mathbf {K} }$denota el término lambda estándar${\displaystyle \lambda x.\lambda yx}$, se reduce solo a sí mismo, mientras que la aplicación${\displaystyle \mathbf {X} (\mathbf {KI} )}$se reduce con reducción de orden normal a${\displaystyle \mathbf {I} }$, por lo tanto tiene un significado. Vemos así que no todos los términos no normalizadores son equivalentes. Nos gustaría decir que${\displaystyle \mathbf {\Omega } }$es menos significativo que${\displaystyle \mathbf {X} }$porque aplicando${\displaystyle \mathbf {X} }$a un término puede producir un resultado pero aplicar${\displaystyle \mathbf {\Omega } }$no puedo.

Los árboles de Böhm también pueden aplicarse en el contexto del cálculo lambda infinito, que incluye términos infinitamente grandes. En este contexto, el término${\displaystyle \mathbf {NN} }$, dónde${\displaystyle \mathbf {N} =\lambda x.\mathbf {I} (xx)}$, se reduce a ambos a${\displaystyle \mathbf {I} (\mathbf {I} (\dots ))}$y${\displaystyle \mathbf {\Omega } }$, por lo tanto, también hay problemas con la confluencia de la normalización. ^{[ 5 ]}

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

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

Hay infinitos conjuntos de términos sin sentido, 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 con actividad en la raíz, es decir, los términos sin forma normal superior ni forma normal en la raíz. Dado que se presupone la actividad en la raíz, este es el conjunto más pequeño de términos sin significado.

Tenga en cuenta que${\displaystyle \mathbf {\Omega } }$es activo en la raíz y por lo tanto${\displaystyle \mathbf {\Omega } \en U}$para cada conjunto de términos sin sentido${\displaystyle U}$.

El conjunto de términos λ con ⊥ (abreviado términos λ⊥) se define coinductivamente mediante la gramática.${\displaystyle M=\bot \mid x\mid (\lambda xM)\mid (MM)}$Esto corresponde al cálculo lambda infinito estándar más términos que contienen${\displaystyle \bot }$La reducción beta en este conjunto se define de la manera estándar. Dado un conjunto de términos sin sentido${\displaystyle U}$, también definimos una reducción al fondo: si${\displaystyle M[\bot \mapsto \mathbf {\Omega } ]\en U}$y${\displaystyle M\neq \bot }$, entonces${\displaystyle M\to \bot }$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 normalizador. ^{[ 7 ]}

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