Cálculo lambda simplesmente digitado - Simply typed lambda calculus

O cálculo lambda de tipo simples ( ), uma forma de teoria dos tipos , é uma interpretação tipada do cálculo lambda com apenas um construtor de tipo ( ) que constrói tipos de função . É o exemplo canônico e mais simples de um cálculo lambda tipado. O cálculo lambda simplesmente digitado foi originalmente introduzido por Alonzo Church em 1940 como uma tentativa de evitar usos paradoxais do cálculo lambda não tipado , e exibe muitas propriedades desejáveis ​​e interessantes. ${\ displaystyle \ lambda ^ {\ to}}$${\ displaystyle \ to}$

O termo tipo simples também é usado para se referir a extensões do cálculo lambda simplesmente digitado, como produtos , coprodutos ou números naturais ( Sistema T ) ou mesmo recursão completa (como PCF ). Em contraste, os sistemas que introduzem tipos polimórficos (como o Sistema F ) ou tipos dependentes (como a Estrutura Lógica ) não são considerados simplesmente digitados . Os primeiros, exceto recursão completa, ainda são considerados simples porque as codificações de Church de tais estruturas podem ser feitas usando apenas variáveis ​​de tipo adequadas, enquanto o polimorfismo e a dependência não podem. ${\ displaystyle \ to}$

Sintaxe

Neste artigo, usamos e para vários tipos. Informalmente, o tipo de função se refere ao tipo de funções que, dada uma entrada do tipo , produzem uma saída do tipo . Por convenção, associados à direita: lemos como . ${\ 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 os tipos, começamos pela fixação de um conjunto de tipos de base , . Às vezes, eles são chamados de tipos atômicos ou constantes de tipo . Com isso corrigido, a sintaxe dos tipos é: ${\ displaystyle B}$

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

Por exemplo, gera um conjunto infinito de tipos começando com${\ displaystyle B = \ {a, b \}}$${\ displaystyle a, b,}$${\ displaystyle a \ to a,}$${\ displaystyle a \ para b, b \ para b,}$${\ displaystyle b \ to a,}$${\ displaystyle a \ to (a \ to a), \ ldots,}$${\ displaystyle (b \ to a) \ to (a \ to b), \ ldots}$

Também fixamos um conjunto de constantes de termos para os tipos de base. Por exemplo, podemos assumir um tipo de base nat , e o termo constantes podem ser os números naturais. Na apresentação original, Church usou apenas dois tipos de base: para "o tipo de proposições" e para "o tipo de indivíduos". O tipo não tem constantes de termo, mas tem uma constante de termo. Freqüentemente, o cálculo com apenas um tipo de base, geralmente , é considerado. ${\ displaystyle o}$${\ displaystyle \ iota}$${\ displaystyle o}$${\ displaystyle \ iota}$${\ displaystyle o}$

A sintaxe do cálculo lambda de digitação simples é essencialmente a mesma do próprio cálculo lambda. Escrevemos para denotar que a variável é do tipo . O termo sintaxe, em BNF, é então: ${\ displaystyle x {\ mathbin {:}} \ tau}$${\ displaystyle x}$${\ displaystyle \ tau}$

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

onde é uma constante de termo. ${\ displaystyle c}$

Ou seja, referência de variável , abstrações , aplicativo e constante . Uma referência de variável é vinculada se estiver dentro de uma associação de abstração . Um termo é fechado se não houver variáveis ​​não associadas. ${\ displaystyle x}$${\ displaystyle x}$

Compare isso com a sintaxe do cálculo lambda não tipado:

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

Vemos que no cálculo lambda tipado cada função ( abstração ) deve especificar o tipo de seu argumento.

Regras de digitação

Para definir o conjunto de termos lambda bem tipados de um determinado tipo, definiremos uma relação de tipagem entre termos e tipos. Primeiro, introduzimos contextos de digitação ou ambientes de digitação , que são conjuntos de suposições de digitação. Uma suposição de digitação tem a forma , o significado tem tipo . ${\ displaystyle \ Gamma, \ Delta, \ dots}$${\ displaystyle x {\ mathbin {:}} \ sigma}$${\ displaystyle x}$${\ displaystyle \ sigma}$

A relação de digitação indica que é um termo do tipo no contexto . Neste caso, é dito que está bem digitado (tendo tipo ). As instâncias da relação de tipagem são chamadas de julgamentos de tipagem . A validade de um julgamento de digitação é mostrada fornecendo uma derivação de digitação , construída usando regras de digitação (em que as premissas acima da linha nos permitem derivar a conclusão abaixo da linha). O cálculo lambda simplesmente digitado usa estas regras: ${\ displaystyle \ Gamma \ vdash e {\ mathbin {:}} \ sigma}$${\ displaystyle e}$${\ displaystyle \ sigma}$${\ displaystyle \ Gamma}$${\ displaystyle e}$${\ displaystyle \ sigma}$

${\ displaystyle {\ frac {x {\ mathbin {:}} \ sigma \ in \ Gamma} {\ Gamma \ vdash x {\ mathbin {:}} \ sigma}}}$ (1)	${\ displaystyle {\ frac {c {\ text {é uma constante do tipo}} T} {\ Gamma \ vdash c {\ mathbin {:}} T}}}$ (2)
${\ displaystyle {\ frac {\ Gamma, x {\ mathbin {:}} \ sigma \ vdash e {\ mathbin {:}} \ tau} {\ Gamma \ vdash (\ lambda x {\ mathbin {:}} \ sigma. ~ e) {\ mathbin {:}} (\ sigma \ to \ tau)}}}$ (3)	${\ displaystyle {\ frac {\ Gamma \ vdash e_ {1} {\ mathbin {:}} \ sigma \ to \ tau \ quad \ Gamma \ vdash e_ {2} {\ mathbin {:}} \ sigma} {\ Gamma \ vdash e_ {1} ~ e_ {2} {\ mathbin {:}} \ tau}}}$ (4)

Em palavras,

1. Se tem tipo no contexto, sabemos que tem tipo .${\ displaystyle x}$${\ displaystyle \ sigma}$${\ displaystyle x}$${\ displaystyle \ sigma}$
2. As constantes de termo têm os tipos de base apropriados.
3. Se, em um determinado contexto com ter tipo , tem tipo , então, no mesmo contexto sem , tem tipo .${\ displaystyle x}$${\ displaystyle \ sigma}$${\ displaystyle e}$${\ displaystyle \ tau}$${\ displaystyle x}$${\ displaystyle \ lambda x {\ mathbin {:}} \ sigma. ~ e}$${\ displaystyle \ sigma \ to \ tau}$
4. Se, em um determinado contexto, tiver tipo e tiver tipo , então terá tipo .${\ displaystyle e_ {1}}$${\ displaystyle \ sigma \ to \ tau}$${\ displaystyle e_ {2}}$${\ displaystyle \ sigma}$${\ displaystyle e_ {1} ~ e_ {2}}$${\ displaystyle \ tau}$

Exemplos de termos fechados, ou seja , termos tipáveis ​​no contexto vazio, são:

• Para cada tipo , um termo (função de identidade / combinador I),${\ displaystyle \ tau}$${\ displaystyle \ lambda x {\ mathbin {:}} \ tau .x {\ mathbin {:}} \ tau \ to \ tau}$
• Para tipos , um termo (o combinador K), e${\ displaystyle \ sigma, \ tau}$${\ displaystyle \ lambda x {\ mathbin {:}} \ sigma. \ lambda y {\ mathbin {:}} \ tau .x {\ mathbin {:}} \ sigma \ to \ tau \ to \ sigma}$
• Para tipos , um termo (o 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 ''}$

Estas são as representações do cálculo lambda tipado dos combinadores básicos da lógica combinatória .

Cada tipo recebe um pedido, um número . Para tipos de base ,; para tipos de função ,. Ou seja, a ordem de um tipo mede a profundidade da seta aninhada mais à esquerda. Portanto: ${\ 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

Interpretações intrínsecas vs. extrínsecas

Falando de maneira geral, existem duas maneiras diferentes de atribuir significado ao cálculo lambda simplesmente digitado, quanto às linguagens digitadas de forma mais geral, às vezes chamadas de intrínseco x extrínseco , ou estilo Church x estilo Curry . Uma semântica intrínseca / de estilo de Igreja apenas atribui significado a termos bem digitados ou, mais precisamente, atribui significado diretamente às derivações de digitação. Isso tem o efeito de que termos que diferem apenas por tipo de anotações podem, no entanto, receber significados diferentes. Por exemplo, o termo de identidade em inteiros e o termo de identidade em booleanos podem significar coisas diferentes. (As interpretações clássicas pretendidas são a função de identidade em inteiros e a função de identidade em valores booleanos.) Em contraste, uma semântica extrínseca / estilo Curry atribui significado aos termos independentemente da digitação, pois eles seriam interpretados em uma linguagem não digitada. Nesta visão, e significam a mesma coisa ( ou seja , a mesma coisa 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}$

A distinção entre semântica intrínseca e extrínseca às vezes está associada à presença ou ausência de anotações em abstrações lambda, mas estritamente falando esse uso é impreciso. É possível definir uma semântica de estilo Curry em termos anotados simplesmente ignorando os tipos ( ou seja , por meio de apagamento de tipo ), pois é possível dar uma semântica de estilo Church em termos não anotados quando os tipos podem ser deduzidos do contexto ( ou seja, , por meio de inferência de tipo ). A diferença essencial entre as abordagens intrínseca e extrínseca é apenas se as regras de digitação são vistas como definidoras da linguagem ou como um formalismo para verificar as propriedades de uma linguagem subjacente mais primitiva. A maioria das diferentes interpretações semânticas discutidas abaixo podem ser vistas através da perspectiva da Igreja ou de Curry.

Teoria equacional

O cálculo lambda simplesmente digitado tem a mesma teoria equacional de βη-equivalência que o cálculo lambda não tipado , mas sujeito a restrições de tipo. A equação para redução beta

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

mantém-se no contexto sempre que e , enquanto a equação para redução eta${\ 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}$

é retido quando e não aparece livre em . ${\ displaystyle \ Gamma \ vdash t \!: \ sigma \ to \ tau}$${\ displaystyle x}$${\ displaystyle t}$

Semântica operacional

Da mesma forma, a semântica operacional do cálculo lambda simplesmente digitado pode ser fixada como para o cálculo lambda não tipado, usando chamada por nome , chamada por valor ou outras estratégias de avaliação . Como para qualquer linguagem digitada, a segurança de tipo é uma propriedade fundamental de todas essas estratégias de avaliação. Além disso, a propriedade de normalização forte descrita abaixo implica que qualquer estratégia de avaliação será encerrada em todos os termos simplesmente digitados.

Semântica categórica

O cálculo lambda simplesmente digitado (com -equivalência) é a linguagem interna das categorias fechadas cartesianas (CCCs), como foi observado pela primeira vez por Lambek . Dado qualquer CCC específico, os tipos básicos do cálculo lambda correspondente são apenas os objetos , e os termos são os morfismos . Por outro lado, todo cálculo lambda simplesmente digitado fornece um CCC cujos objetos são os tipos e os morfismos são classes de equivalência de termos. ${\ displaystyle \ beta \ eta}$

Para tornar a correspondência clara, um construtor de tipo para o produto cartesiano é normalmente adicionado ao acima. Para preservar a categoricidade do produto cartesiano , adicionam-se regras de tipo para emparelhamento , projeção e um termo de unidade . Dados dois termos e , o termo tem tipo . Da mesma forma, se se tem um prazo , então existem termos e onde correspondem às projeções do produto cartesiano. O termo da unidade , do tipo 1, é escrito como e vocalizado como 'nil', é o objeto final . A teoria equacional é estendida da mesma forma, de modo que se tenha ${\ 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 = ()}$

Este último é lido como " se t tiver o tipo 1, então se reduz a nulo ".

O acima pode então ser transformado em uma categoria tomando os tipos como os objetos . Os morfismos são classes de equivalência de pares onde x é uma variável (do tipo ) e t é um termo (do tipo ), não tendo variáveis ​​livres nele, exceto para (opcionalmente) x . O fecho é obtido a partir da carilagem e aplicação , como habitualmente. ${\ displaystyle \ sigma \ to \ tau}$${\ displaystyle (x {\ mathbin {:}} \ sigma, t {\ mathbin {:}} \ tau)}$${\ displaystyle \ sigma}$${\ displaystyle \ tau}$

Mais precisamente, existem functores entre a categoria das categorias fechadas cartesianas e a categoria das teorias lambda simplesmente tipadas.

É comum estender este caso para categorias monoidais simétricas fechadas usando um sistema de tipo linear . A razão para isso é que o CCC é um caso especial da categoria monoidal simétrica fechada, que normalmente é considerada a categoria dos conjuntos . Isso é bom para estabelecer as bases da teoria dos conjuntos , mas o topos mais geral parece fornecer uma base superior.

Semântica teórica de prova

O cálculo lambda simplesmente digitado está intimamente relacionado ao fragmento implicacional da lógica intuicionista proposicional , ou seja, lógica mínima , por meio do isomorfismo de Curry-Howard : os termos correspondem precisamente às provas na dedução natural , e os tipos habitados são exatamente as tautologias da lógica mínima.

Sintaxes alternativas

A apresentação dada acima não é a única maneira de definir a sintaxe do cálculo lambda simplesmente digitado. Uma alternativa é remover totalmente as anotações de tipo (de modo que a sintaxe seja idêntica ao cálculo lambda não tipado), ao mesmo tempo que garante que os termos sejam bem digitados por meio da inferência de tipo Hindley-Milner . O algoritmo de inferência é finalizador, sólido e completo: sempre que um termo é tipificável, o algoritmo calcula seu tipo. Mais precisamente, ele calcula o termo tipo principais , pois muitas vezes um termo não anotadas (como ) pode ter mais de um tipo ( , , etc., que são todas as instâncias do tipo diretor ). ${\ displaystyle \ lambda x. ~ x}$${\ displaystyle {\ mathtt {int}} \ to {\ mathtt {int}}}$${\ displaystyle {\ mathtt {bool}} \ to {\ mathtt {bool}}}$${\ displaystyle \ alpha \ to \ alpha}$

Outra apresentação alternativa do cálculo lambda simplesmente digitado é baseada na verificação de tipo bidirecional , que requer mais anotações de tipo do que a inferência de Hindley-Milner, mas é mais fácil de descrever. O sistema de tipos é dividido em dois julgamentos, representando a verificação e a síntese , escrita e respectivamente. Operacionalmente, os três componentes , e são todos entradas para o julgamento de verificação , ao passo que o julgamento de síntese usa apenas e como entradas, produzindo o tipo como saída. Esses julgamentos são derivados por meio das seguintes regras: ${\ 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}$

${\ displaystyle {\ frac {x {\ mathbin {:}} \ sigma \ in \ Gamma} {\ Gamma \ vdash x \ Rightarrow \ sigma}}}$ [1]	${\ displaystyle {\ frac {c {\ text {é uma constante do tipo}} T} {\ Gamma \ vdash c \ Rightarrow T}}}$ [2]
${\ displaystyle {\ frac {\ Gamma, x {\ mathbin {:}} \ sigma \ vdash e \ Leftarrow \ tau} {\ Gamma \ vdash \ lambda x. ~ e \ Leftarrow \ sigma \ to \ tau}}}$ [3]	${\ displaystyle {\ frac {\ Gamma \ vdash e_ {1} \ Rightarrow \ sigma \ to \ tau \ quad \ Gamma \ vdash e_ {2} \ Leftarrow \ sigma} {\ Gamma \ vdash e_ {1} ~ e_ { 2} \ Rightarrow \ tau}}}$ [4]
${\ displaystyle {\ frac {\ Gamma \ vdash e \ Rightarrow \ tau} {\ Gamma \ vdash e \ Leftarrow \ tau}}}$ [5]	${\ displaystyle {\ frac {\ Gamma \ vdash e \ Leftarrow \ tau} {\ Gamma \ vdash (e {\ mathbin {:}} \ tau) \ Rightarrow \ tau}}}$ [6]

Observe que as regras [1] - [4] são quase idênticas às regras (1) - (4) acima, exceto pela escolha cuidadosa de verificação ou síntese de julgamentos. Essas escolhas podem ser explicadas da seguinte forma:

1. Se estiver no contexto, podemos sintetizar o tipo para .${\ displaystyle x {\ mathbin {:}} \ sigma}$${\ displaystyle \ sigma}$${\ displaystyle x}$
2. Os tipos de constantes de termo são fixos e podem ser sintetizados.
3. Para verificar se há tipo em algum contexto, estendemos o contexto com e verificamos se há tipo .${\ displaystyle \ lambda x. ~ e}$${\ displaystyle \ sigma \ to \ tau}$${\ displaystyle x {\ mathbin {:}} \ sigma}$${\ displaystyle e}$${\ displaystyle \ tau}$
4. Se sintetiza o tipo (em algum contexto) e verifica o tipo (no mesmo contexto), então sintetiza o tipo .${\ displaystyle e_ {1}}$${\ displaystyle \ sigma \ to \ tau}$${\ displaystyle e_ {2}}$${\ displaystyle \ sigma}$${\ displaystyle e_ {1} ~ e_ {2}}$${\ displaystyle \ tau}$

Observe que as regras de síntese são lidas de cima para baixo, enquanto as regras de verificação são lidas de baixo para cima. Observe em particular que não precisamos de nenhuma anotação na abstração lambda na regra [3], porque o tipo da variável limitada pode ser deduzido do tipo no qual verificamos a função. Finalmente, explicamos as regras [5] e [6] da seguinte forma:

5. Para verificar se há tipo , basta sintetizar o tipo .${\ displaystyle e}$${\ displaystyle \ tau}$${\ displaystyle \ tau}$
6. Se verificar em relação ao tipo , o termo explicitamente anotado é sintetizado . ${\ displaystyle e}$${\ displaystyle \ tau}$${\ displaystyle (e {\ mathbin {:}} \ tau)}$${\ displaystyle \ tau}$

Por causa dessas duas últimas regras coagindo entre síntese e verificação, é fácil ver que qualquer termo bem digitado, mas não anotado, pode ser verificado no sistema bidirecional, desde que insira anotações de tipo "suficiente". E, de fato, as anotações são necessárias apenas em β-redexes.

Observações gerais

Dada a semântica padrão, o cálculo lambda simplesmente digitado é fortemente normalizador : isto é, termos bem digitados sempre se reduzem a um valor, isto é, uma abstração. Isso ocorre porque a recursão não é permitida pelas regras de digitação: é impossível encontrar tipos para combinadores de ponto fixo e o termo de loop . A recursão pode ser adicionada à linguagem tendo um operador especial de tipo ou adicionando tipos recursivos gerais , embora ambos eliminem a normalização forte. ${\ displaystyle \ lambda}$${\ displaystyle \ Omega = (\ lambda x. ~ x ~ x) (\ lambda x. ~ x ~ x)}$${\ displaystyle {\ mathtt {fix}} _ {\ alpha}}$${\ displaystyle (\ alpha \ to \ alpha) \ to \ alpha}$

Uma vez que é fortemente normalizando, é decidível se um programa de cálculo lambda simplesmente digitado será interrompido ou não: na verdade, ele sempre para . Podemos, portanto, concluir que a linguagem não é Turing completa .

Resultados importantes

• Tait mostrou em 1967 que a redução é fortemente normalizadora . Como corolário, a equivalência é decidível . Statman mostrou em 1977 que o problema de normalização não é recursivo elementar , prova que foi posteriormente simplificada por Mairson (1992). O problema é conhecido por estar no conjunto da hierarquia Grzegorczyk . Uma prova de normalização puramente semântica (ver normalização por avaliação ) foi fornecida por Berger e Schwichtenberg em 1991.${\ displaystyle \ beta}$${\ displaystyle \ beta \ eta}$${\ displaystyle {\ mathcal {E}} ^ {4}}$
• O problema de unificação para -equivalência é indecidível. Huet mostrou em 1973 que a unificação de 3ª ordem é indecidível e isso foi melhorado por Baxter em 1978 e depois por Goldfarb em 1981, mostrando que a unificação de 2ª ordem já é indecidível. Uma prova de que a correspondência de ordem superior (unificação onde apenas um termo contém variáveis ​​existenciais) é decidível foi anunciada por Colin Stirling em 2006, e uma prova completa foi publicada em 2009.${\ displaystyle \ beta \ eta}$
• Podemos codificar os números naturais pelos termos do tipo ( numerais da Igreja ). Schwichtenberg mostrou em 1976 que exatamente os polinômios estendidos são representáveis ​​como funções sobre numerais de Igreja; estes são aproximadamente os polinômios fechados sob um operador condicional.${\ displaystyle (o \ a o) \ a (o \ a o)}$${\ displaystyle \ lambda ^ {\ to}}$
• Um modelo completo de é dado interpretando os tipos de base como conjuntos e tipos de função pelo espaço de função teórica dos conjuntos . Friedman mostrou em 1975 que essa interpretação é completa para -equivalência, se os tipos de base são interpretados por conjuntos infinitos. Statman mostrou em 1983 que -equivalência é a equivalência máxima que é tipicamente ambígua , isto é, fechada sob substituições de tipo ( Teorema da Ambiguidade Típica de Statman ). Um corolário disso é que a propriedade do modelo finito é válida, ou seja, conjuntos finitos são suficientes para distinguir termos que não são identificados por -equivalência.${\ displaystyle \ lambda ^ {\ to}}$${\ displaystyle \ beta \ eta}$${\ displaystyle \ beta \ eta}$${\ displaystyle \ beta \ eta}$
• Plotkin introduziu relações lógicas em 1973 para caracterizar os elementos de um modelo que são definíveis por termos lambda. Em 1993, Jung e Tiuryn ​​mostraram que uma forma geral de relação lógica (relações lógicas de Kripke com aridade variável) caracteriza exatamente a definibilidade lambda. Plotkin e Statman conjeturaram que é decidível se um determinado elemento de um modelo gerado a partir de conjuntos finitos é definível por um termo lambda ( conjectura de Plotkin-Statman ). A conjectura foi demonstrada como falsa por Loader em 1993.

Notas

Referências

• A. Igreja: Uma Formulação da Teoria Simples dos Tipos , JSL 5, 1940
• WWTait : Intensional Interpretations of Functionals of Finite Type I, JSL 32 (2), 1967
• GD Plotkin: Lambda-definibilidade e relações lógicas, Relatório técnico, 1973
• GP Huet: The Undecidability of Unification in Third Order Logic Information and Control 22 (3): 257-267 (1973)
• H. Friedman: Igualdade entre funcionais . LogicColl. '73, páginas 22-37, LNM 453, 1975.
• H. Schwichtenberg: Funções definíveis no cálculo lambda simplesmente tipado, Arch. Math Logik 17 (1976) 113-114.
• R. Statman: The Typed lambda-Calculus is not Elementary Recursive FOCS 1977: 90-94
• WD Goldfarb: A indecidibilidade do problema de unificação de 2ª ordem, TCS (1981), no. 13, 225-230.
• R. Statman. -funcionais e conversão definíveis . Arco. Matemática. Logik, 23: 21-26, 1983.${\ displaystyle \ lambda}$${\ displaystyle \ beta \ eta}$
• J. Lambek : Categorias fechadas cartesianas e Lambda-cálculos digitados . Combinators and Functional Programming Languages ​​1985: 136-175
• U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus LICS 1991: 203-211
• H. Mairson: Uma prova simples de um teorema de Statman , TCS 103 (2): 387-394, 1992.
• Jung, A., Tiuryn, J .: A New Characterization of Lambda Definability , TLCA 1993
• R. Loader: The Undecidability of λ-definability , publicado no Church Festschrift, 2001
• H. Barendregt, Lambda Calculi with Types , Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN  0-19-853761-1 .
• L. Baxter: A indecidibilidade do problema de unificação diádica de terceira ordem , Information and Control 38 (2), 170-178 (1978)

links externos

• Loader, Ralph (fevereiro de 1998). "Notas sobre o cálculo lambda simplesmente digitado" .
• Entrada "Church's Type Theory" na Stanford Encyclopedia of Philosophy