¿Cómo es el cálculo Lambda un tipo específico de sistema de escritura a término?

Ahora podemos ver que la Iglesia estaba asociada con el Cálculo Lambda Simplemente Escrito . De hecho, parece que explicó el cálculo de Lambda simplemente tipado para reducir los malentendidos sobre el cálculo de Lambda.

Ahora, cuando John McCarthy creó Lisp, lo basó en el cálculo Lambda . Esto es por su propia admisión cuando publicó "Funciones recursivas de expresiones simbólicas y su cálculo por máquina, Parte I" . Puedes leerlo aquí .

Ahora sabemos que en el núcleo de Mathematica hay un sistema similar a Lisp , pero en lugar de basarse únicamente en el cálculo Lambda, se basa en un sistema de reescritura de términos .

Aquí el autor declara:

Mathematica es fundamentalmente un sistema de reescritura de términos ... un concepto más general que el cálculo Lambda detrás de Lisp.

Parece que el cálculo Lambda es una pequeña parte de una categoría mucho más general. (Muy revelador como un pensamiento, este era más un concepto fundamental). Estoy tratando de leer más sobre esto para tener una perspectiva al respecto.

Mi pregunta es: ¿Cómo es el cálculo Lambda un tipo específico de sistema de escritura de términos?

La respuesta es que depende de lo que quiere decir con Sistema de reescritura de términos .

Cuando se introdujo, el concepto de Sistemas de reescritura de términos , o TRSes, describió lo que ahora se llama TRS de primer orden , que es simplemente un conjunto de reglas de cálculo de la forma

$$l\rightarrow r$$

donde y son términos de primer orden de la forma$l$$r$

$$t :=\ x\ \mid\ f(t_1,\ldots,t_n)$$

donde es una variable es un símbolo de función tomado de un conjunto arbitrario, pero fijo , llamado firma , que también corrige varios argumentos para cada .$x$$f$$\Sigma$$f\in\Sigma$

Hay un par de restricciones comunes impuestas a las reglas, por ejemplo, pero no necesitamos entrar en ellas aquí.$\mathrm{Var}(r)\subseteq\mathrm{Var}(l)$

Con esta definición, el cálculo lambda habitual, con la regla : no se puede expresar, ya que el constructor " " une la aparición de en (Sin embargo, la aplicación está bien). Una posible solución, y una que es más antigua que la teoría de reescribir los sistemas en sí, es convertir cada término en otro tipo de término, que no implique vinculación.$\beta$

$$(\lambda x. t)\ u \rightarrow t[u/x]$$ $\lambda$$x$$t$$\lambda$

Una forma es el famoso cálculo del combinador , que es una regla de reescritura con la firma y las reglas y $SK$$\Sigma=\{S,\ K, \mathrm{app}\}$

$$\mathrm{app}(\mathrm{app}(K,x),y)\rightarrow x$$ $$\mathrm{app}(\mathrm{app}(\mathrm{app}(S, x), y), z)\rightarrow \mathrm{app}(\mathrm{app}(x, z),\mathrm{app}(y, z))$$

Hay otra codificación más intuitiva que implica términos lambda con índices de Bruijn y sustituciones explícitas, pero no voy a entrar aquí.

---

A pesar de las codificaciones de primer orden, quedó claro que los problemas técnicos con el comportamiento de reducción del cálculo se abordaron mejor extendiendo la noción de TRS para incluir constructores con aglutinantes. Esto a menudo se conoce con el término Sistemas de reescritura de orden superior . Ahora se toman los términos del formulario$\lambda$

$$t\ :=\ x(t_1,\ldots, t_n)\ \mid\ f(x^1_1\ldots x^1_{i_1}.t_1,\ldots,x^n_1\ldots x^n_{i_n}.t_n)$$

Donde nuevamente , pero ahora cada está enlazado en . Las firmas necesitan especificar cuántas variables están unidas por cada argumento. Ahora podemos escribir para el término que representa . Con un poco de trabajo, puede definir nociones apropiadas de sustitución.x i j t i a b s ( x . t ) λ x . $f\in\Sigma$$x^i_j$$t_i$$\mathrm{abs}(x.t)$$\lambda x.t$

Aquí hay menos consenso sobre lo que constituye una regla de reescritura . Un problema es que queremos que la reescritura sea decidible, por lo que debe ser decidible si un lado izquierdo coincide con un término. Pero esto generalmente se toma como módulo que se cree que es decidible, pero solo con algoritmos extremadamente complejos y lentos (¡y solo es indecidible!).$\beta\eta$$\beta$

Por lo tanto, los lados izquierdos están restringidos a estar en algún subconjunto agradable, a menudo los "patrones de Miller". Se generalizan varios resultados para el caso de primer orden, aunque hay algunas sorpresas desagradables.

También es común tomar sistemas de primer orden y simplemente agregar y aplicación a la estructura de términos, junto con reducciones ad hoc y . Esto produce sistemas bastante razonables, a costa de (alguna) generalidad.β $\lambda$ $\beta$$\eta$

Por supuesto, el cálculo habitual se puede escribir directamente en estos sistemas. Por ejemplo, la regla :$\lambda$$\beta$

$$\mathrm{app}(\mathrm{abs}(x.y(x)),z)\rightarrow y(z)$$

Nipkow y Prehofer dan una descripción bastante decente de las definiciones y resultados básicos aquí .

Esta presentación de Beckman y Meijer repasa el cálculo lambda, la reescritura de términos y menciona Mathematica. Creo que responde la pregunta de forma intuitiva: https://channel9.msdn.com/Series/Beckman-Meijer-Overdrive/Beckman-Meijer-Overdrive-The-Lambda-Calculus-and-Food-Nutrition