Cálculo lambda simplemente escrito

Sistema formal en lógica matemática.

El cálculo lambda de tipo simple ( ), una forma de teoría de tipos , es una interpretación tipificada del cálculo lambda con un solo constructor de tipos ( ) que construye tipos de funciones . Es el ejemplo canónico y más simple de cálculo lambda tipificado. El cálculo lambda simplemente tipificado fue introducido originalmente por Alonzo Church en 1940 como un intento de evitar el uso paradójico del cálculo lambda no tipificado . ^[1] ${\displaystyle \lambda ^{\to }}$ ${\displaystyle \to }$

El término tipo simple también se utiliza para referirse a extensiones del cálculo lambda de tipo simple con construcciones como productos , coproductos o números naturales ( Sistema T ) o incluso recursividad completa (como PCF ). Por el contrario, los sistemas que introducen tipos polimórficos (como el Sistema F ) o tipos dependientes (como el Marco Lógico ) no se consideran simplemente tipificados . Los tipos simples, excepto la recursión completa, todavía se consideran simples porque las codificaciones de Church de tales estructuras se pueden realizar utilizando únicamente variables de tipo adecuadas, mientras que el polimorfismo y la dependencia no. ${\displaystyle \to }$

Sintaxis

En la década de 1930, Alonzo Church buscó utilizar el método logístico : ^[a] su cálculo lambda , como lenguaje formal basado en expresiones simbólicas, consistía en una serie infinitamente infinita de axiomas y variables, ^[b] pero también un conjunto finito de símbolos primitivos. , ^[c] que denota abstracción y alcance, así como cuatro constantes: negación, disyunción, cuantificación universal y selección respectivamente; ^{[d] [e]} y además, un conjunto finito de reglas I a VI. Este conjunto finito de reglas incluía la regla V modus ponens así como la IV y VI para sustitución y generalización respectivamente. ^[d] Las reglas I a III se conocen como conversión alfa, beta y eta en el cálculo lambda. Church buscó utilizar el inglés sólo como lenguaje sintáctico (es decir, un lenguaje metamatemático) para describir expresiones simbólicas sin interpretaciones. ^[F]

En 1940, Church optó por una notación de subíndice para denotar el tipo en una expresión simbólica. ^[b] En su presentación, Church utilizó sólo dos tipos básicos: para "el tipo de proposiciones" y para "el tipo de individuos". El tipo no tiene términos constantes, mientras que tiene un término constante. Frecuentemente se considera el cálculo con un solo tipo de base, generalmente . Los subíndices de letras griegas , etc. denotan variables de tipo; el subíndice entre paréntesis indica el tipo de función . Church 1940 p.58 usó 'flecha o ' para indicar que significa o es una abreviatura de . ^[g] En la década de 1970 se utilizaba la notación de flechas independiente; por ejemplo, en este artículo, símbolos sin subíndice y pueden variar según los tipos. Se consideró entonces que el número infinito de axiomas era una consecuencia de aplicar las reglas I a VI a los tipos (ver Axiomas de Peano ). Informalmente, el tipo de función se refiere al tipo de funciones que, dada una entrada de tipo , producen una salida de tipo . Por convención, asociados a la derecha: se lee como . ${\displaystyle o}$ ${\displaystyle \iota }$ ${\displaystyle o}$ ${\displaystyle \iota }$ ${\displaystyle o}$ ${\displaystyle \alpha ,\beta }$ ${\displaystyle (\alpha \beta )}$ ${\displaystyle \beta \to \alpha }$ ${\displaystyle \to }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \to }$ ${\displaystyle \sigma \to \tau \to \rho }$ ${\displaystyle \sigma \to (\tau \to \rho )}$

Para definir los tipos, primero se debe definir un conjunto de tipos base . A veces se les llama tipos atómicos o constantes de tipo . Con esto arreglado, la sintaxis de tipos es: ${\displaystyle B}$

${\displaystyle \tau ::=\tau \to \tau \mid T\quad \mathrm {where} \quad T\in B}$.

Por ejemplo, genera un conjunto infinito de tipos que comienzan con , , , , , , , ..., , ... ${\displaystyle B=\{a,b\}}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a\to a}$ ${\displaystyle a\to b}$ ${\displaystyle b\to b}$ ${\displaystyle b\to a}$ ${\displaystyle a\to (a\to a)}$ ${\displaystyle (b\to a)\to (a\to b)}$

También se fija un conjunto de constantes de términos para los tipos base. Por ejemplo, se podría suponer que uno de los tipos base es nat y sus constantes de término podrían ser los números naturales.

La sintaxis del cálculo lambda de tipo simple es esencialmente la del cálculo lambda mismo. El término denota que la variable es de tipo . El término sintaxis, en la forma Backus-Naur , es referencia de variable , abstracciones , aplicación o constante : ${\displaystyle x{\mathbin {:}}\tau }$ ${\displaystyle x}$ ${\displaystyle \tau }$

${\displaystyle e::=x\mid \lambda x{\mathbin {:}}\tau .e\mid e\,e\mid c}$

donde es un término constante. Una referencia de variable está vinculada si está dentro de un enlace de abstracción . Un término está cerrado si no hay variables libres. ${\displaystyle c}$ ${\displaystyle x}$ ${\displaystyle x}$

En comparación, la sintaxis del cálculo lambda sin tipo no tiene tales constantes de tipificación o términos:

${\displaystyle e::=x\mid \lambda x.e\mid e\,e}$

Mientras que en el cálculo lambda escrito cada abstracción (es decir, función) debe especificar el tipo de su argumento.

Reglas de mecanografía

Para definir el conjunto de términos lambda bien tipificados de un tipo determinado, se define una relación de tipificación entre términos y tipos. En primer lugar, se introducen los contextos de escritura , o entornos de escritura , que son conjuntos de suposiciones de escritura. Una suposición de tipificación tiene la forma , es decir, la variable tiene tipo . ${\displaystyle \Gamma ,\Delta ,\dots }$ ${\displaystyle x{\mathbin {:}}\sigma }$ ${\displaystyle x}$ ${\displaystyle \sigma }$

La relación de tipificación indica que es un término de tipo en contexto . En este caso se dice que está bien tipado (que tiene tipo ). Los casos de relación de tipificación se denominan juicios de tipificación . La validez de un juicio de tipificación se muestra proporcionando una derivación de tipificación , construida usando reglas de tipificación (donde las premisas sobre la línea nos permiten derivar la conclusión debajo de la línea). El cálculo lambda escrito simplemente utiliza estas reglas: ^[h] ${\displaystyle \Gamma \vdash e{\mathbin {:}}\sigma }$ ${\displaystyle e}$ ${\displaystyle \sigma }$ ${\displaystyle \Gamma }$ ${\displaystyle e}$ ${\displaystyle \sigma }$

En palabras,

1. Si tiene tipo en el contexto, entonces tiene tipo . ${\displaystyle x}$ ${\displaystyle \sigma }$ ${\displaystyle x}$ ${\displaystyle \sigma }$
2. Las constantes de término tienen los tipos de base apropiados.
3. Si, en un contexto determinado con tipo , tiene tipo , entonces, en el mismo contexto sin , tiene tipo . ${\displaystyle x}$ ${\displaystyle \sigma }$ ${\displaystyle e}$ ${\displaystyle \tau }$ ${\displaystyle x}$ ${\displaystyle \lambda x{\mathbin {:}}\sigma .~e}$ ${\displaystyle \sigma \to \tau }$
4. Si, en un contexto determinado, tiene tipo y tiene tipo , entonces tiene tipo . ${\displaystyle e_{1}}$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle e_{2}}$ ${\displaystyle \sigma }$ ${\displaystyle e_{1}~e_{2}}$ ${\displaystyle \tau }$

Ejemplos de términos cerrados, es decir, términos que se pueden escribir en el contexto vacío, son:

• Para cada tipo , un término ( función de identidad /combinador I), ${\displaystyle \tau }$ ${\displaystyle \lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau }$
• Para los tipos , un término (el combinador K) y ${\displaystyle \sigma ,\tau }$ ${\displaystyle \lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma }$
• Para tipos , un término (el combinador S). ${\displaystyle \tau ,\tau ',\tau ''}$ ${\displaystyle \lambda x{\mathbin {:}}\tau \to \tau '\to \tau ''.\lambda y{\mathbin {:}}\tau \to \tau '.\lambda z{\mathbin {:}}\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''}$

Estas son las representaciones del cálculo lambda tipificadas de los combinadores básicos de la lógica combinatoria .

A cada tipo se le asigna un orden, un número . Para tipos de base, ; para tipos de funciones, . Es decir, el orden de un tipo mide la profundidad de la flecha anidada más a la izquierda. Por eso: ${\displaystyle \tau }$ ${\displaystyle o(\tau )}$ ${\displaystyle o(T)=0}$ ${\displaystyle o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))}$

${\displaystyle o(\iota \to \iota \to \iota )=1}$

${\displaystyle o((\iota \to \iota )\to \iota )=2}$

Semántica

Interpretaciones intrínsecas versus extrínsecas

En términos generales, hay dos formas diferentes de asignar significado al cálculo lambda simplemente tipado, así como a los lenguajes tipificados en general, llamados intrínseco versus extrínseco, ontológico versus semántico, o estilo Church versus estilo Curry. ^{[1] [7] [8]} Una semántica intrínseca sólo asigna significado a términos bien tipificados, o más precisamente, asigna significado directamente a derivaciones tipográficas. Esto tiene el efecto de que a los términos que difieren sólo por las anotaciones de tipo se les pueden asignar significados diferentes. Por ejemplo, el término de identidad en números enteros y el término de identidad en booleanos pueden significar cosas diferentes. (Las interpretaciones clásicas previstas son la función de identidad en números enteros y la función de identidad en valores booleanos). Por el contrario, una semántica extrínseca asigna significado a los términos independientemente de su tipo, tal como se interpretarían en un lenguaje sin tipo. Desde este punto de vista, y significan lo mismo ( es decir , lo mismo que ). ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}$ ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}$ ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}$ ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}$ ${\displaystyle \lambda x.~x}$

La distinción entre semántica intrínseca y extrínseca a veces se asocia con la presencia o ausencia de anotaciones en abstracciones lambda, pero estrictamente hablando, este uso es impreciso. Es posible definir una semántica extrínseca en términos anotados simplemente ignorando los tipos ( es decir , mediante el borrado de tipos ), del mismo modo que es posible dar una semántica intrínseca en términos no anotados cuando los tipos se pueden deducir del contexto ( es decir , mediante inferencia de tipos ). ). La diferencia esencial entre los enfoques intrínseco y extrínseco es simplemente si se considera que las reglas de tipificación definen el lenguaje o como un formalismo para verificar las propiedades de un lenguaje subyacente más primitivo. La mayoría de las diferentes interpretaciones semánticas que se analizan a continuación pueden verse desde una perspectiva intrínseca o extrínseca.

Teoría ecuacional

El cálculo lambda de tipo simple (STLC) tiene la misma teoría ecuacional de equivalencia βη que el cálculo lambda sin tipo , pero sujeto a restricciones de tipo. La ecuación para la reducción beta ^[i]

${\displaystyle (\lambda x{\mathbin {:}}\sigma .~t)\,u=_{\beta }t[x:=u]}$

se mantiene en contexto siempre que y , mientras que la ecuación para la reducción de eta ^[j] ${\displaystyle \Gamma }$ ${\displaystyle \Gamma ,x{\mathbin {:}}\sigma \vdash t{\mathbin {:}}\tau }$ ${\displaystyle \Gamma \vdash u{\mathbin {:}}\sigma }$

${\displaystyle \lambda x{\mathbin {:}}\sigma .~t\,x=_{\eta }t}$

se mantiene siempre y no aparece libre en . La ventaja del cálculo lambda tipificado es que STLC permite acortar (es decir, reducir ) cálculos potencialmente no terminantes. ^[9] ${\displaystyle \Gamma \vdash t\!:\sigma \to \tau }$ ${\displaystyle x}$ ${\displaystyle t}$

Semántica operativa

Del mismo modo, la semántica operativa del cálculo lambda con tipo simple se puede corregir como para el cálculo lambda sin tipo, usando llamada por nombre , llamada por valor u otras estrategias de evaluación . Como ocurre con cualquier lenguaje mecanografiado, la seguridad de tipos es una propiedad fundamental de todas estas estrategias de evaluación. Además, la fuerte propiedad de normalización que se describe a continuación implica que cualquier estrategia de evaluación terminará en todos los términos simplemente escritos. ^[10]

Semántica categórica

El cálculo lambda escrito simplemente y enriquecido con tipos de productos, operadores de emparejamiento y proyección (con -equivalencia) es el lenguaje interno de las categorías cartesianas cerradas (CCC), como lo observó por primera vez Joachim Lambek . ^[11] Dado cualquier CCC, los tipos básicos del cálculo lambda correspondiente son los objetos y los términos son los morfismos . Por el contrario, el cálculo lambda de tipo simple con tipos de productos y operadores de emparejamiento sobre una colección de tipos base y términos dados forma un CCC cuyos objetos son los tipos, y los morfismos son clases de equivalencia de términos. ${\displaystyle \beta \eta }$

Existen reglas de escritura para emparejamiento , proyección y término unitario . Dados dos términos y , el término tiene tipo . Asimismo, si se tiene un término , entonces hay términos y donde corresponden a las proyecciones del producto cartesiano. El término unitario , de tipo 1, escrito y vocalizado como 'nil', es el objeto final . La teoría ecuacional se amplía de la misma manera, de modo que se tiene ${\displaystyle s{\mathbin {:}}\sigma }$ ${\displaystyle t{\mathbin {:}}\tau }$ ${\displaystyle (s,t)}$ ${\displaystyle \sigma \times \tau }$ ${\displaystyle u{\mathbin {:}}\tau _{1}\times \tau _{2}}$ ${\displaystyle \pi _{1}(u){\mathbin {:}}\tau _{1}}$ ${\displaystyle \pi _{2}(u){\mathbin {:}}\tau _{2}}$ ${\displaystyle \pi _{i}}$ ${\displaystyle ()}$

${\displaystyle \pi _{1}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=s{\mathbin {:}}\sigma }$

${\displaystyle \pi _{2}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=t{\mathbin {:}}\tau }$

${\displaystyle (\pi _{1}(u{\mathbin {:}}\sigma \times \tau ),\pi _{2}(u{\mathbin {:}}\sigma \times \tau ))=u{\mathbin {:}}\sigma \times \tau }$

${\displaystyle t{\mathbin {:}}1=()}$

Esto último se lee como " si t tiene tipo 1, entonces se reduce a cero ".

Lo anterior se puede convertir en una categoría tomando los tipos como objetos . Los morfismos son clases de equivalencia de pares donde x es una variable (de tipo ) y t es un término (de tipo ), que no contiene variables libres, excepto (opcionalmente) x . El conjunto de términos en el lenguaje es la clausura de este conjunto de términos bajo las operaciones de abstracción y aplicación . ${\displaystyle \sigma \to \tau }$ ${\displaystyle (x{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )}$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$

Esta correspondencia se puede ampliar para incluir "homomorfismos del lenguaje" y functores entre la categoría de categorías cerradas cartesianas y la categoría de teorías lambda simplemente tipificadas.

Parte de esta correspondencia se puede extender a categorías monoidales simétricas cerradas mediante el uso de un sistema de tipo lineal .

Semántica de la teoría de la prueba

El cálculo lambda simplemente tipificado está estrechamente relacionado con el fragmento implicacional de la lógica intuicionista proposicional , es decir, el cálculo proposicional implicacional , a través del isomorfismo de Curry-Howard : los términos corresponden precisamente a pruebas en la deducción natural , y los tipos habitados son exactamente las tautologías de esta lógica. .

A partir de su método logístico, Church 1940 ^[1] p.58 expuso un esquema de axioma , ^[1] p. 60, que Henkin 1949 completó ^[3] para mostrar los dominios de tipos (por ejemplo, los números naturales, los números reales, etc.). Henkin 1996 pág. 146 describió cómo el método logístico de Church podría buscar proporcionar una base para las matemáticas (aritmética de Peano y análisis real), ^[4] a través de la teoría de modelos .

Sintaxis alternativas

La presentación anterior no es la única forma de definir la sintaxis del cálculo lambda simplemente tipado. Una alternativa es eliminar las anotaciones de tipo por completo (para que la sintaxis sea idéntica al cálculo lambda sin tipo), garantizando al mismo tiempo que los términos estén bien tipificados mediante la inferencia de tipos Hindley-Milner . El algoritmo de inferencia es terminante, sólido y completo: siempre que un término se puede tipificar, el algoritmo calcula su tipo. Más precisamente, calcula el tipo principal del término , ya que a menudo un término sin anotaciones (como ) puede tener más de un tipo ( ,, etc., que son todas instancias del tipo principal ). ${\displaystyle \lambda x.~x}$ ${\displaystyle {\mathtt {int}}\to {\mathtt {int}}}$ ${\displaystyle {\mathtt {bool}}\to {\mathtt {bool}}}$ ${\displaystyle \alpha \to \alpha }$

Otra presentación alternativa del cálculo lambda de tipo simple se basa en la verificación de tipos bidireccional , que requiere más anotaciones de tipo que la inferencia de Hindley-Milner pero es más fácil de describir. El sistema de tipos se divide en dos juicios, que representan tanto la verificación como la síntesis , escritas y respectivamente. Operacionalmente, los tres componentes , y son entradas para el juicio de verificación , mientras que el juicio de síntesis solo toma y como entradas, produciendo el tipo como salida. Estos juicios se derivan de las siguientes reglas: ${\displaystyle \Gamma \vdash e\Leftarrow \tau }$ ${\displaystyle \Gamma \vdash e\Rightarrow \tau }$ ${\displaystyle \Gamma }$ ${\displaystyle e}$ ${\displaystyle \tau }$ ${\displaystyle \Gamma \vdash e\Leftarrow \tau }$ ${\displaystyle \Gamma \vdash e\Rightarrow \tau }$ ${\displaystyle \Gamma }$ ${\displaystyle e}$ ${\displaystyle \tau }$

Observe que las reglas [1] a [4] son ​​casi idénticas a las reglas (1) a (4) anteriores, excepto por la cuidadosa elección de los juicios de verificación o síntesis. Estas opciones se pueden explicar así:

1. Si está en el contexto, podemos sintetizar el tipo de . ${\displaystyle x{\mathbin {:}}\sigma }$ ${\displaystyle \sigma }$ ${\displaystyle x}$
2. Los tipos de constantes de término son fijos y se pueden sintetizar.
3. Para comprobar que tiene tipo en algún contexto, ampliamos el contexto con y comprobamos que tiene tipo . ${\displaystyle \lambda x.~e}$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle x{\mathbin {:}}\sigma }$ ${\displaystyle e}$ ${\displaystyle \tau }$
4. Si sintetiza el tipo (en algún contexto) y lo compara con el tipo (en el mismo contexto), entonces sintetiza el tipo . ${\displaystyle e_{1}}$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle e_{2}}$ ${\displaystyle \sigma }$ ${\displaystyle e_{1}~e_{2}}$ ${\displaystyle \tau }$

Observe que las reglas de síntesis se leen de arriba hacia abajo, mientras que las reglas de verificación se leen de abajo hacia arriba. Tenga en cuenta en particular que no necesitamos ninguna anotación en la abstracción lambda en la regla [3], porque el tipo de variable vinculada se puede deducir del tipo en el que verificamos la función. Finalmente, explicamos las reglas [5] y [6] de la siguiente manera:

5. Para comprobar que tiene tipo , basta con sintetizar el tipo . ${\displaystyle e}$ ${\displaystyle \tau }$ ${\displaystyle \tau }$
6. Si se compara con el tipo , entonces el término anotado explícitamente se sintetiza . ${\displaystyle e}$ ${\displaystyle \tau }$ ${\displaystyle (e{\mathbin {:}}\tau )}$ ${\displaystyle \tau }$

Debido a estas dos últimas reglas que obligan entre síntesis y verificación, es fácil ver que cualquier término bien tipificado pero sin anotaciones puede verificarse en el sistema bidireccional, siempre que insertemos "suficientes" anotaciones de tipo. Y, de hecho, las anotaciones sólo son necesarias en β-redexes.

Observaciones generales

Dada la semántica estándar, el cálculo lambda simplemente tipificado es fuertemente normalizador : cada secuencia de reducciones eventualmente termina. ^[10] Esto se debe a que las reglas de tipificación no permiten la recursividad: es imposible encontrar tipos para combinadores de punto fijo y el término de bucle . La recursividad se puede agregar al lenguaje ya sea teniendo un operador de tipo especial o agregando tipos recursivos generales , aunque ambos eliminan una fuerte normalización. ${\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)}$ ${\displaystyle {\mathtt {fix}}_{\alpha }}$ ${\displaystyle (\alpha \to \alpha )\to \alpha }$

A diferencia del cálculo lambda sin tipo, el cálculo lambda simplemente tipificado no es Turing completo . Todos los programas en el cálculo lambda simplemente tecleado se detienen. Para el cálculo lambda sin tipo, existen programas que no se detienen y, además, no existe ningún procedimiento de decisión general que pueda determinar si un programa se detiene.

Resultados importantes

• Tait demostró en 1967 que la reducción es fuertemente normalizadora . ^[10] Como corolario: la equivalencia es decidible . Statman demostró en 1979 que el problema de normalización no es recursivo elemental , ^[12] una prueba que luego fue simplificada por Mairson. ^[13] Se sabe que el problema está en el conjunto de la jerarquía de Grzegorczyk . ^[14] Berger y Schwichtenberg dieron una prueba de normalización puramente semántica (ver normalización por evaluación ) en 1991. ^[15] ${\displaystyle \beta }$ ${\displaystyle \beta \eta }$ ${\displaystyle {\mathcal {E}}^{4}}$
• El problema de la unificación para la equivalencia es indecidible. Huet demostró en 1973 que la unificación de tercer orden es indecidible ^[16] y esto fue mejorado por Baxter en 1978 ^[17] y luego por Goldfarb en 1981 ^[18] al mostrar que la unificación de segundo orden ya es indecidible. Colin Stirling anunció en 2006 una prueba de que la coincidencia de orden superior (unificación donde solo un término contiene variables existenciales) es decidible, y en 2009 se publicó una prueba completa ^. ${\displaystyle \beta \eta }$
• Podemos codificar números naturales mediante términos del tipo ( números de Iglesia ). Schwichtenberg demostró en 1975 que exactamente los polinomios extendidos son representables como funciones sobre los números de Church; ^[20] estos son aproximadamente los polinomios cerrados bajo un operador condicional. ${\displaystyle (o\to o)\to (o\to o)}$ ${\displaystyle \lambda ^{\to }}$
• Se obtiene un modelo completo interpretando los tipos base como conjuntos y tipos de funciones mediante el espacio funcional de la teoría de conjuntos . Friedman demostró en 1975 que esta interpretación es completa para la equivalencia, si los tipos base se interpretan como conjuntos infinitos. ^[21] Statman demostró en 1983 que la equivalencia - es la equivalencia máxima que es típicamente ambigua , es decir, cerrada bajo sustituciones de tipos ( Teorema de ambigüedad típica de Statman ). ^[22] Un corolario de esto es que la propiedad del modelo finito se cumple, es decir, los conjuntos finitos son suficientes para distinguir términos que no están identificados por -equivalencia. ${\displaystyle \lambda ^{\to }}$ ${\displaystyle \beta \eta }$ ${\displaystyle \beta \eta }$ ${\displaystyle \beta \eta }$
• Plotkin introdujo las relaciones lógicas en 1973 para caracterizar los elementos de un modelo que se pueden definir mediante términos lambda. ^[23] En 1993, Jung y Tiuryn ​​demostraron que una forma general de relación lógica (relaciones lógicas de Kripke con aridad variable) caracteriza exactamente la definibilidad lambda. ^[24] Plotkin y Statman conjeturaron que es decidible si un elemento dado de un modelo generado a partir de conjuntos finitos se puede definir mediante un término lambda ( conjetura de Plotkin-Statman ). Loader demostró que la conjetura era falsa en 2001. ^[25]

Notas

1. Alonzo Church (1956) Introducción a la lógica matemática págs. 47-68 ^[2]
2. Church 1940, p.57 denota variables con subíndices para su tipo: ^[1] ${\displaystyle a_{\alpha },b_{\alpha },...z_{\alpha },...{\bar {a}}_{\alpha },{\bar {b}}_{\alpha },...{\bar {z}}_{\alpha },...}$
3. Church 1940, p.57: el segundo y tercer símbolo primitivo enumerados () denotan alcance: ^[1] ${\displaystyle \lambda ,(,),N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}$
4. Church 1940, p.60: son cuatro constantes que denotan negación, disyunción, cuantificación universal y selección respectivamente. ^[1] ${\displaystyle N_{oo},A_{ooo},\Pi _{o(o\alpha )},\iota _{\alpha (o\alpha )}}$
5. Iglesia 1940, p.59 ^[1] Henkin 1949 p.160; ^[3] Henkin 1996 p.144 ^[4]
6. Iglesia 1940, p.57 ^[1]
7. Church 1940 p.58 enumera 24 fórmulas abreviadas. ^[1]
8. Este artículo muestra 4 juicios mecanografiados a continuación, en palabras. es el entorno de escritura . ^[5] ${\displaystyle \Gamma }$
9. El ' ' denota el proceso de producir la sustitución de la expresión u por x, en la forma t ${\displaystyle =_{\beta }}$
10. El ' ' denota el proceso de producción de la expansión de la forma t aplicada a x ${\displaystyle =_{\eta }}$

1. Iglesia abcdefghij, Alonzo (junio de 1940). "Una formulación de la teoría simple de tipos" (PDF) . Revista de Lógica Simbólica . 5 (2): 56–68. doi :10.2307/2266170. JSTOR  2266170. S2CID  15889861. Archivado desde el original (PDF) el 12 de enero de 2019.
2. Church, Alonzo (1956) Introducción a la lógica matemática
3. Leon Henkin (septiembre de 1949) La integridad del cálculo funcional de primer orden p.160
4. Leon Henkin (junio de 1996) El descubrimiento de mis pruebas de integridad
5. Aprendizaje hedonista: aprender por diversión (Última actualización el 25 de noviembre de 2021 a las 14:00 UTC) Comprender los criterios de mecanografía
6. Pfenning, Frank, Church y Curry: combinación de tipificación intrínseca y extrínseca (PDF) , p. 1 , consultado el 26 de febrero de 2022.
7. Curry, Haskell B (20 de septiembre de 1934). "Funcionalidad en lógica combinatoria". Actas de la Academia Nacional de Ciencias de los Estados Unidos de América . 20 (11): 584–90. Código bibliográfico : 1934PNAS...20..584C. doi : 10.1073/pnas.20.11.584 . ISSN  0027-8424. PMC 1076489 . PMID  16577644. (presenta una lógica combinatoria tipificada extrínsecamente, posteriormente adaptada por otros al cálculo lambda) ^[6]
8. Reynolds, John (1998). Teorías de los lenguajes de programación . Cambridge, Inglaterra: Cambridge University Press. págs.327, 334. ISBN 9780521594141.
9. Norman Ramsey (primavera de 2019) Estrategias de reducción para el cálculo Lambda
10. Tait, WW (agosto de 1967). "Interpretaciones intensionales de funcionales de tipo finito I". La revista de lógica simbólica . 32 (2): 198–212. doi :10.2307/2271658. ISSN  0022-4812. JSTOR  2271658. S2CID  9569863.
11. Lambek, J. (1986). "Categorías cartesianas cerradas y cálculos λ mecanografiados". Combinadores y lenguajes de programación funcionales . Apuntes de conferencias sobre informática. vol. 242. Saltador. págs. 136-175. doi :10.1007/3-540-17184-3_44. ISBN 978-3-540-47253-7.
12. Statman, Richard (1 de julio de 1979). "El cálculo λ escrito no es recursivo elemental". Informática Teórica . 9 (1): 73–81. doi : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN  0304-3975.
13. Mairson, Harry G. (14 de septiembre de 1992). "Una prueba sencilla de un teorema de Statman". Informática Teórica . 103 (2): 387–394. doi :10.1016/0304-3975(92)90020-G. ISSN  0304-3975.
14. Statman, Richard (julio de 1979). "El cálculo λ escrito no es recursivo elemental". Informática Teórica . 9 (1): 73–81. doi : 10.1016/0304-3975(79)90007-0 . hdl : 2027.42/23535 . ISSN  0304-3975.
15. Berger, U.; Schwichtenberg, H. (julio de 1991). "Una inversa de la evaluación funcional para el cálculo lambda escrito". [1991] Actas del Sexto Simposio Anual del IEEE sobre Lógica en Ciencias de la Computación. págs. 203–211. doi :10.1109/LICS.1991.151645. ISBN 0-8186-2230-X. S2CID  40441974.
16. Huet, Gérard P. (1 de abril de 1973). "La indecidibilidad de la unificación en la lógica de tercer orden". Información y Control . 22 (3): 257–267. doi :10.1016/S0019-9958(73)90301-X. ISSN  0019-9958.
17. Baxter, Lewis D. (1 de agosto de 1978). "La indecidibilidad del problema de unificación diádica de tercer orden". Información y Control . 38 (2): 170–178. doi : 10.1016/S0019-9958(78)90172-9 . ISSN  0019-9958.
18. Goldfarb, Warren D. (1 de enero de 1981). "La indecidibilidad del problema de unificación de segundo orden". Informática Teórica . 13 (2): 225–230. doi :10.1016/0304-3975(81)90040-2. ISSN  0304-3975.
19. Stirling, Colin (22 de julio de 2009). "Decidibilidad del emparejamiento de orden superior". Métodos lógicos en informática . 5 (3): 1–52. arXiv : 0907.3804 . doi :10.2168/LMCS-5(3:2)2009. S2CID  1478837.
20. Schwichtenberg, Helmut (1 de septiembre de 1975). "Definierbare Funktionen imλ-Kalkül mit Typen". Archiv für mathematische Logik und Grundlagenforschung (en alemán). 17 (3): 113–114. doi :10.1007/BF02276799. ISSN  1432-0665. S2CID  11598130.
21. Friedman, Harvey (1975). "Igualdad entre funcionales". Coloquio de Lógica . Apuntes de conferencias de matemáticas. vol. 453. Saltador. págs. 22-37. doi :10.1007/BFb0064870. ISBN 978-3-540-07155-6.
22. Statman, R. (1 de diciembre de 1983). " λ {\displaystyle \lambda } -funcionales definibles y conversión β η {\displaystyle \beta \eta }". Archiv für mathematische Logik und Grundlagenforschung . 23 (1): 21-26. doi :10.1007/BF02023009. ISSN  1432-0665. S2CID  33920306.
23. Plotkin, GD (1973). Definibilidad lambda y relaciones lógicas (PDF) (Reporte técnico). Universidad de Edimburgo . Consultado el 30 de septiembre de 2022 .
24. Jung, Achim; Tiuryn, Jerzy (1993). "Una nueva caracterización de la definibilidad lambda". Cálculos Lambda mecanografiados y aplicaciones . Apuntes de conferencias sobre informática. vol. 664. Saltador. págs. 245-257. doi :10.1007/BFb0037110. ISBN 3-540-56517-5.
25. Cargador, Ralph (2001). "La indecidibilidad de la λ-definibilidad". Lógica, Significado y Computación . Springer Países Bajos. págs. 331–342. doi :10.1007/978-94-010-0526-5_15. ISBN 978-94-010-3891-1.

Referencias

• H. Barendregt , Lambda Calculi with Types, Manual de lógica en informática, volumen II, Oxford University Press, 1993. ISBN 0-19-853761-1 . 

enlaces externos

• Cargador, Ralph (febrero de 1998). "Notas sobre el cálculo Lambda mecanografiado simplemente".
• Entrada "Teoría de tipos de la Iglesia" en la Enciclopedia de Filosofía de Stanford