Cálculo lambda de tipo simple

Sistema formal en lógica matemática

El cálculo lambda de tipado 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 función . Es el ejemplo canónico y más simple de un cálculo lambda tipificado. El cálculo lambda de tipado simple 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 tipos simples con construcciones como productos , coproductos o números naturales ( Sistema T ) o incluso recursión 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 de tipos simples . Los tipos simples, excepto la recursión completa, todavía se consideran simples porque las codificaciones de Church de tales estructuras se pueden hacer usando solo variables de tipo adecuadas, mientras que el polimorfismo y la dependencia no pueden. ${\displaystyle \to }$

Sintaxis

En la década de 1930, Alonzo Church intentó utilizar el método logístico : ^[a] su cálculo lambda , como lenguaje formal basado en expresiones simbólicas, consistía en una serie infinita de axiomas y variables, ^[b] pero también un conjunto finito de símbolos primitivos, ^[c] que denotan abstracción y alcance, así como cuatro constantes: negación, disyunción, cuantificación universal y selección respectivamente; ^{[d] [e]} y también, un conjunto finito de reglas I a VI. Este conjunto finito de reglas incluía la regla V modus ponens , así como 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 solo como un lenguaje sintáctico (es decir, un lenguaje metamatemático) para describir expresiones simbólicas sin interpretaciones. ^[f]

En 1940 Church se decidió 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 base: para "el tipo de proposiciones" y para "el tipo de individuos". El tipo no tiene constantes de término, mientras que tiene una constante de término. Con frecuencia se considera el cálculo con un solo tipo base, normalmente . Los subíndices de letras griegas , etc. denotan variables de tipo; el subíndice entre paréntesis denota el tipo de función . Church 1940 p.58 utilizó 'flecha o ' para denotar significa , o es una abreviatura de . ^[g] En la década de 1970 se utilizaba la notación de flecha independiente; por ejemplo, en este artículo los símbolos sin subíndice y pueden abarcar varios tipos. Entonces se vio que el número infinito de axiomas era una consecuencia de aplicar las reglas I a VI a los tipos (ver Axiomas de Peano ). De manera informal, 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, se asocia 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 los llama tipos atómicos o constantes de tipo . Una vez que esto se soluciona, la sintaxis de los 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érmino 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 en sí. El término indica 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 una constante de término. Una referencia de variable está vinculada si está dentro de un enlace de abstracción . Un término está cerrado si no hay variables no vinculadas. ${\displaystyle c}$ ${\displaystyle x}$ ${\displaystyle x}$

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

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

Mientras que en el cálculo lambda tipado 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 tipificación o entornos de tipificación , que son conjuntos de suposiciones de tipificación. Una suposición de tipificación tiene la forma , lo que significa que la variable tiene el 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 tipificado (tiene tipo ). Las instancias de la relación de tipificación se denominan juicios de tipificación . La validez de un juicio de tipificación se demuestra proporcionando una derivación de tipificación , construida utilizando reglas de tipificación (donde las premisas por encima de la línea nos permiten derivar la conclusión por debajo de la línea). El cálculo lambda de tipificación simple 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 base apropiados.
3. Si, en un determinado contexto con que tiene 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 determinado contexto, 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 tipificables en el contexto vacío, son:

• Para cada tipo , un término ( función 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 los tipos , un término (el S-combinador). ${\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 ''}$

Éstas son las representaciones de cálculo lambda tipificado de los combinadores básicos de la lógica combinatoria .

A cada tipo se le asigna un orden, un número . Para los tipos base, ; para los tipos de función, . Es decir, el orden de un tipo mide la profundidad de la flecha anidada más a la izquierda. Por lo tanto: ${\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 vs. extrínsecas

En términos generales, hay dos formas diferentes de asignar significado al cálculo lambda de tipado simple, como a los lenguajes tipados en general, llamadas de diversas formas: intrínseca vs. extrínseca, ontológica vs. semántica, o estilo Church vs. estilo Curry. ^{[1] [7] [8]} Una semántica intrínseca solo asigna significado a términos bien tipados, o más precisamente, asigna significado directamente a derivaciones de tipado. Esto tiene el efecto de que a los términos que difieren solo por las anotaciones de tipo se les pueden asignar, no obstante, significados diferentes. Por ejemplo, el término identidad en números enteros y el término identidad en valores booleanos pueden significar cosas diferentes. (Las interpretaciones clásicas previstas son la función identidad en números enteros y la función identidad en valores booleanos). Por el contrario, una semántica extrínseca asigna significado a los términos independientemente del tipado, como se interpretarían en un lenguaje no tipado. En esta visión, 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 , a través del borrado de tipos ), como es posible dar una semántica intrínseca en términos no anotados cuando los tipos se pueden deducir del contexto ( es decir , a través de la inferencia de tipos ). La diferencia esencial entre los enfoques intrínsecos y extrínsecos es simplemente si las reglas de tipificación se consideran como la definición del 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 discutidas a continuación se pueden ver a través de una perspectiva intrínseca o extrínseca.

Teoría de ecuaciones

El cálculo lambda de tipo simple (STLC) tiene la misma teoría ecuacional de βη-equivalencia que el cálculo lambda sin tipo , pero está 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 cumple 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 cumple siempre que y no aparece libre en . La ventaja del cálculo lambda tipado es que STLC permite acortar los cálculos potencialmente no terminantes (es decir, reducir ). ^[9] ${\displaystyle \Gamma \vdash t\!:\sigma \to \tau }$ ${\displaystyle x}$ ${\displaystyle t}$

Semántica operacional

De la misma manera, la semántica operacional del cálculo lambda de tipado simple se puede fijar como para el cálculo lambda sin tipar, utilizando llamadas por nombre , llamadas por valor u otras estrategias de evaluación . Como en cualquier lenguaje tipado, la seguridad de tipos es una propiedad fundamental de todas estas estrategias de evaluación. Además, la propiedad de normalización fuerte que se describe a continuación implica que cualquier estrategia de evaluación terminará en todos los términos de tipado simple. ^[10]

Semántica categórica

El cálculo lambda de tipos simples enriquecido con tipos de producto, operadores de emparejamiento y proyección (con -equivalencia) es el lenguaje interno de las categorías cerradas cartesianas (CCC), como 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 tipos simples con tipos de producto y operadores de emparejamiento sobre una colección de tipos base y términos dados forma una CCC cuyos objetos son los tipos y los morfismos son clases de equivalencia de términos. ${\displaystyle \beta \eta }$

Existen reglas de tipificación para el emparejamiento , la proyección y un término unitario . Dados dos términos y , el término tiene tipo . Del mismo modo, si uno 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 como y vocalizado como 'nil', es el objeto final . La teoría de ecuaciones se extiende de la misma manera, de modo que uno 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 puede entonces convertirse en una categoría tomando los tipos como los 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 tiene variables libres en él, 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 puede extenderse para incluir "homomorfismos del lenguaje" y funtores entre la categoría de categorías cartesianas cerradas y la categoría de teorías lambda simplemente tipificadas.

Parte de esta correspondencia puede extenderse a categorías monoidales simétricas cerradas utilizando un sistema de tipos lineal .

Semántica basada en la teoría de la prueba

El cálculo lambda simplemente tipado 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 las 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 estableció un esquema de axiomas , ^[1] p. 60, que Henkin 1949 completó ^[3] con dominios de tipos (por ejemplo, los números naturales, los números reales, etc.). Henkin 1996 p. 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 dada anteriormente no es la única forma de definir la sintaxis del cálculo lambda de tipado simple. Una alternativa es eliminar las anotaciones de tipo por completo (de modo que la sintaxis sea idéntica a la del cálculo lambda sin tipo), al tiempo que se garantiza que los términos estén bien tipificados mediante la inferencia de tipos de Hindley-Milner . El algoritmo de inferencia es terminante, sólido y completo: siempre que un término sea tipificable, el algoritmo calcula su tipo. Más precisamente, calcula el tipo principal del término , ya que a menudo un término no anotado (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 tipos simples se basa en la comprobación de tipos bidireccional , que requiere más anotaciones de tipos 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 comprobación como la síntesis , escritos y respectivamente. Operativamente, los tres componentes , y son todos entradas para el juicio de comprobación , mientras que el juicio de síntesis solo toma y como entradas, produciendo el tipo como salida. Estos juicios se derivan a través 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 }$

Obsérvese que las reglas [1]–[4] son ​​casi idénticas a las reglas (1)–(4) anteriores, excepto por la elección cuidadosa de los juicios de comprobación o síntesis. Estas elecciones se pueden explicar de la siguiente manera:

1. Si está en el contexto, podemos sintetizar el tipo para . ${\displaystyle x{\mathbin {:}}\sigma }$ ${\displaystyle \sigma }$ ${\displaystyle x}$
2. Los tipos de constantes de término son fijos y pueden sintetizarse.
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 verifica contra 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 para la síntesis se leen de arriba hacia abajo, mientras que las reglas para la comprobación se leen de abajo hacia arriba. Observe en particular que no necesitamos ninguna anotación sobre la abstracción lambda en la regla [3], porque el tipo de la variable ligada se puede deducir del tipo en el que comprobamos la función. Finalmente, explicamos las reglas [5] y [6] de la siguiente manera:

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

Debido a que estas dos últimas reglas ejercen presión entre la síntesis y la comprobación, es fácil ver que cualquier término bien tipificado pero no anotado puede comprobarse en el sistema bidireccional, siempre que insertemos "suficientes" anotaciones de tipo. Y, de hecho, las anotaciones solo son necesarias en los β-redexes.

Observaciones generales

Dada la semántica estándar, el cálculo lambda de tipos simples es fuertemente normalizador : cada secuencia de reducciones termina eventualmente. ^[10] Esto se debe a que las reglas de tipado no permiten la recursión: es imposible encontrar tipos para combinadores de punto fijo y el término de bucle . La recursión se puede agregar al lenguaje ya sea con un operador especial de tipo o agregando tipos recursivos generales , aunque ambos eliminan la normalización fuerte. ${\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 con tipos simples no es Turing completo . Todos los programas del cálculo lambda con tipos simples se detienen. En el caso del cálculo lambda sin tipo, hay programas que no se detienen y, además, no existe un 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 normalizante . ^[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 fue simplificada posteriormente por Mairson. ^[13] Se sabe que el problema está en el conjunto de la jerarquía de Grzegorczyk . ^[14] Una prueba de normalización puramente semántica (véase normalización por evaluación ) fue presentada por Berger y Schwichtenberg en 1991. ^[15] ${\displaystyle \beta }$ ${\displaystyle \beta \eta }$ ${\displaystyle {\mathcal {E}}^{4}}$
• El problema de unificación para la equivalencia es indecidible. Huet demostró en 1973 que la unificación de tercer orden es indecidible ^[16] y Baxter mejoró este planteamiento en 1978 ^[17] y luego Goldfarb en 1981 ^[18] al demostrar que la unificación de segundo orden ya es indecidible. Colin Stirling anunció en 2006 una prueba de que la correspondencia de orden superior (unificación en la que solo un término contiene variables existenciales) es decidible, y en 2009 se publicó una prueba completa ^[19]. ${\displaystyle \beta \eta }$
• Podemos codificar números naturales mediante términos del tipo ( números de Church ). 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 }}$
• Un modelo completo de se da interpretando los tipos base como conjuntos y los tipos de función por el espacio de funciones de teoría de conjuntos . Friedman mostró en 1975 que esta interpretación es completa para -equivalencia, si los tipos base son interpretados por conjuntos infinitos. ^[21] Statman mostró en 1983 que -equivalencia es la equivalencia máxima que es típicamente ambigua , es decir, cerrada bajo sustituciones de tipo ( 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 son definibles por 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 es definible por 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 pp.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 ( ) indican 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ág. 59 ^[1] Henkin 1949 pág. 160; ^[3] Henkin 1996 pág. 144 ^[4]
6. Iglesia 1940, p.57 ^[1]
7. Church 1940 p.58 enumera 24 fórmulas abreviadas. ^[1]
8. Este artículo muestra a continuación 4 juicios de mecanografía, en palabras. es el entorno de mecanografía . ^[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. Church, Alonzo (junio de 1940). "Una formulación de la teoría simple de tipos" (PDF) . Journal of Symbolic Logic . 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 completitud del cálculo funcional de primer orden p.160
4. Leon Henkin (junio de 1996) El descubrimiento de mis pruebas de completitud
5. Aprendizaje hedonista: aprender por el placer de hacerlo (Última actualización el 25 de noviembre de 2021 a las 14:00 UTC) Comprender los juicios de mecanografía
6. Pfenning, Frank, Church and 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. Bibcode :1934PNAS...20..584C. doi : 10.1073/pnas.20.11.584 . ISSN  0027-8424. PMC 1076489 . PMID  16577644. (presenta una lógica combinatoria extrínsecamente tipada, posteriormente adaptada por otros al cálculo lambda) ^[6]
8. Reynolds, John (1998). Teorías de lenguajes de programación . Cambridge, Inglaterra: Cambridge University Press. pp. 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". The Journal of Symbolic Logic . 32 (2): 198–212. doi :10.2307/2271658. ISSN  0022-4812. JSTOR  2271658. S2CID  9569863.
11. Lambek, J. (1986). "Categorías cerradas cartesianas y cálculos λ tipificados". Combinadores y lenguajes de programación funcional . Apuntes de clase en informática. Vol. 242. Springer. 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 λ tipado no es recursivo elemental". Ciencias de la Computación 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 simple de un teorema de Statman". Ciencias Informáticas Teóricas . 103 (2): 387–394. doi :10.1016/0304-3975(92)90020-G. ISSN  0304-3975.
14. Statman, Richard (julio de 1979). "El cálculo λ tipado no es recursivo elemental". Ciencias de la Computación 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 función de evaluación para el cálculo lambda tipado". [1991] Actas del Sexto Simposio Anual 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". Ciencias Informáticas Teóricas . 13 (2): 225–230. doi :10.1016/0304-3975(81)90040-2. ISSN  0304-3975.
19. Stirling, Colin (22 de julio de 2009). "Decidibilidad de la correspondencia 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 clase de matemáticas. Vol. 453. Springer. 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). Lambda-definability and logical relationships (PDF) (Informe 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 de lambda". Cálculos lambda tipificados y aplicaciones . Apuntes de clase en informática. Vol. 664. Springer. págs. 245–257. doi :10.1007/BFb0037110. ISBN. 3-540-56517-5.
25. Loader, Ralph (2001). "La indecidibilidad de la λ-definibilidad". Lógica, significado y computación . Springer Netherlands. págs. 331–342. doi :10.1007/978-94-010-0526-5_15. ISBN 978-94-010-3891-1.

Referencias

• H. Barendregt , Cálculos lambda con tipos, Manual de lógica en informática, Volumen II, Oxford University Press, 1993. ISBN 0-19-853761-1 . 

Enlaces externos

• Loader, Ralph (febrero de 1998). "Notas sobre cálculo lambda de tipos simples".
• Entrada sobre la "Teoría de tipos de Church" en la Enciclopedia de Filosofía de Stanford