cálculo lambda

Da Wikipédia, a enciclopédia livre
Ir para a navegação Saltar para pesquisar

Lambda calculus (também escrito como λ -calculus ) é um sistema formal em lógica matemática para expressar a computação baseada na abstração e aplicação de funções usando associação e substituição de variáveis . É um modelo universal de computação que pode ser usado para simular qualquer máquina de Turing . Foi introduzido pelo matemático Alonzo Church na década de 1930 como parte de sua pesquisa sobre os fundamentos da matemática .

O cálculo lambda consiste em construir termos lambda e realizar operações de redução neles. Na forma mais simples de cálculo lambda, os termos são construídos usando apenas as seguintes regras:

Sintaxe Nome Descrição
x Variável Um caractere ou string que representa um parâmetro ou valor matemático/lógico.
x . M ) Abstração Definição da função ( M é um termo lambda). A variável x torna -se vinculada na expressão.
( M N ) Aplicativo Aplicando uma função a um argumento. M e N são termos lambda.

produzindo expressões como: (λ xy .(λ z .(λ x . zx ) (λ y . zy )) ( xy )). Os parênteses podem ser eliminados se a expressão não for ambígua. Para algumas aplicações, podem ser incluídos termos para constantes e operações lógicas e matemáticas.

As operações de redução incluem:

Operação Nome Descrição
x . M [ x ]) → (λ y . M [ y ]) α-conversão Renomear as variáveis ​​vinculadas na expressão. Usado para evitar colisões de nomes .
((λ x . M ) E ) → ( M [ x  := E ]) β-redução Substituindo as variáveis ​​vinculadas pela expressão de argumento no corpo da abstração.

Se a indexação De Bruijn for usada, a conversão α não será mais necessária, pois não haverá colisões de nomes. Se a aplicação repetida dos passos de redução eventualmente terminar, então pelo teorema de Church-Rosser ela produzirá uma forma β-normal .

Os nomes de variáveis ​​não são necessários se estiver usando uma função lambda universal, como Iota e Jot , que podem criar qualquer comportamento de função chamando-a em várias combinações.

Explicação e aplicações

O cálculo lambda é Turing complete , ou seja, é um modelo universal de computação que pode ser usado para simular qualquer máquina de Turing . [1] Seu homônimo, a letra grega lambda (λ), é usado em expressões lambda e termos lambda para denotar a ligação de uma variável em uma função .

O cálculo lambda pode ser digitado ou não tipado . No cálculo lambda tipado, as funções podem ser aplicadas somente se forem capazes de aceitar o "tipo" de dados da entrada fornecida. Os cálculos lambda tipados são mais fracos do que os cálculos lambda não tipados, que é o assunto principal deste artigo, no sentido de que os cálculos lambda tipados podem expressar menos do que os cálculos não tipados, mas por outro lado os cálculos lambda tipados permitem que mais coisas sejam provadas ; no cálculo lambda simplesmente digitadoé, por exemplo, um teorema de que toda estratégia de avaliação termina para cada termo lambda simplesmente tipado, enquanto a avaliação de termos lambda não tipados não precisa terminar. Uma razão pela qual existem muitos cálculos lambda tipados é o desejo de fazer mais (do que o cálculo não tipado pode fazer) sem desistir de ser capaz de provar teoremas fortes sobre o cálculo.

O cálculo lambda tem aplicações em muitas áreas diferentes em matemática , filosofia , [2] linguística , [3] [4] e ciência da computação . [5] O cálculo lambda desempenhou um papel importante no desenvolvimento da teoria das linguagens de programação . As linguagens de programação funcionais implementam o cálculo lambda. O cálculo lambda também é um tópico de pesquisa atual na teoria das categorias . [6]

História

O cálculo lambda foi introduzido pelo matemático Alonzo Church na década de 1930 como parte de uma investigação sobre os fundamentos da matemática . [7] [a] O sistema original mostrou-se logicamente inconsistente em 1935, quando Stephen Kleene e JB Rosser desenvolveram o paradoxo de Kleene-Rosser . [8] [9]

Posteriormente, em 1936, Church isolou e publicou apenas a parte relevante para a computação, o que hoje é chamado de cálculo lambda não tipado. [10] Em 1940, ele também introduziu um sistema computacionalmente mais fraco, mas logicamente consistente, conhecido como cálculo lambda simplesmente tipado . [11]

Até a década de 1960, quando sua relação com as linguagens de programação foi esclarecida, o cálculo lambda era apenas um formalismo. Graças às aplicações de Richard Montague e outros linguistas na semântica da linguagem natural, o cálculo lambda começou a ter um lugar respeitável tanto na linguística [12] quanto na ciência da computação. [13]

Origem do símbolo lambda

Há alguma incerteza sobre a razão do uso da letra grega lambda (λ) por Church como a notação para abstração de função no cálculo lambda, talvez em parte devido a explicações conflitantes do próprio Church. De acordo com Cardone e Hindley (2006):

A propósito, por que Church escolheu a notação “λ”? Em [uma carta não publicada de 1964 para Harald Dickson] ele afirmou claramente que veio da notação “” usado para abstração de classe por Whitehead e Russell , modificando primeiro “" para "” para distinguir abstração de função de abstração de classe e, em seguida, alterando “” para “λ” para facilitar a impressão.

Essa origem também foi relatada em [Rosser, 1984, p.338]. Por outro lado, em seus últimos anos, Church disse a dois inquiridores que a escolha foi mais acidental: era necessário um símbolo e λ acabou de ser escolhido.

Dana Scott também abordou essa questão em várias palestras públicas. [14] Scott conta que certa vez fez uma pergunta sobre a origem do símbolo lambda ao genro de Church, John Addison, que então escreveu um cartão postal para seu sogro:

Prezada Professora Igreja,

Russell tinha o operador iota , Hilbert tinha o operador epsilon . Por que você escolheu lambda para sua operadora?

Segundo Scott, toda a resposta de Church consistiu em devolver o cartão postal com a seguinte anotação: " eeny, meeny, miny, moe ".

Descrição informal

Motivação

Funções computáveis são um conceito fundamental dentro da ciência da computação e da matemática. O cálculo lambda fornece uma semântica simples para computação, permitindo que as propriedades da computação sejam estudadas formalmente. O cálculo lambda incorpora duas simplificações que tornam essa semântica simples. A primeira simplificação é que o cálculo lambda trata as funções "anonimamente", sem lhes dar nomes explícitos. Por exemplo, a função

pode ser reescrito de forma anônima como

(que é lido como "uma tupla de x e y é mapeada para"). Da mesma forma, a função

pode ser reescrito de forma anônima como

onde a entrada é simplesmente mapeada para si mesma.

A segunda simplificação é que o cálculo lambda usa apenas funções de uma única entrada. Uma função comum que requer duas entradas, por exemplo, ofunção, pode ser retrabalhada em uma função equivalente que aceita uma única entrada e, como saída, retorna outra função, que por sua vez aceita uma única entrada. Por exemplo,

pode ser retrabalhado em

Esse método, conhecido como currying , transforma uma função que recebe vários argumentos em uma cadeia de funções, cada uma com um único argumento.

Aplicação da função do função para os argumentos (5, 2), produz de uma vez

,

Considerando que a avaliação da versão ao curry requer mais uma etapa

// a definição de tem sido usado com na expressão interior. Isso é como redução β.
// a definição de tem sido usado com . Novamente, semelhante à redução β.

para chegar ao mesmo resultado.

O cálculo lambda

O cálculo lambda consiste em uma linguagem de termos lambda , que são definidos por uma certa sintaxe formal, e um conjunto de regras de transformação, que permitem a manipulação dos termos lambda. Essas regras de transformação podem ser vistas como uma teoria equacional ou como uma definição operacional .

Conforme descrito acima, todas as funções no cálculo lambda são funções anônimas, sem nomes. Eles aceitam apenas uma variável de entrada, com currying usado para implementar funções com várias variáveis.

Termos lambda

A sintaxe do cálculo lambda define algumas expressões como expressões de cálculo lambda válidas e outras como inválidas, assim como algumas cadeias de caracteres são programas C válidos e outras não. Uma expressão de cálculo lambda válida é chamada de "termo lambda".

As três regras a seguir fornecem uma definição indutiva que pode ser aplicada para construir todos os termos lambda sintaticamente válidos:

  • uma variável, x , é um termo lambda válido
  • se t é um termo lambda e x é uma variável, então(às vezes escrito em ASCII como) é um termo lambda (chamado de abstração );
  • se t e s são termos lambda, entãoé um termo lambda (chamado de aplicativo ).

Nada mais é um termo lambda. Assim, um termo lambda é válido se e somente se puder ser obtido pela aplicação repetida dessas três regras. No entanto, alguns parênteses podem ser omitidos de acordo com certas regras. Por exemplo, os parênteses externos geralmente não são escritos. Veja Notação , abaixo.

Uma abstração é uma definição de uma função anônima que é capaz de receber uma única entrada x e substituí-la na expressão t . Assim, define uma função anônima que recebe x e retorna t . Por exemplo, é uma abstração da função usando o termo para t . A definição de uma função com uma abstração meramente "configura" a função, mas não a invoca. A abstração vincula a variável x no termo t .

Uma aplicação ts representa a aplicação de uma função t a uma entrada s , ou seja, representa o ato de chamar a função t na entrada s para produzir.

Não há conceito no cálculo lambda de declaração de variável. Em uma definição como(ou seja), o cálculo lambda trata y como uma variável que ainda não está definida. A abstraçãoé sintaticamente válido e representa uma função que adiciona sua entrada ao ainda desconhecido y .

O colchete pode ser usado e pode ser necessário para desambiguar os termos. Por exemplo,edenotam termos diferentes (embora coincidentemente reduzam ao mesmo valor). Aqui, o primeiro exemplo define uma função cujo termo lambda é o resultado da aplicação de x à função filha, enquanto o segundo exemplo é a aplicação da função mais externa à entrada x, que retorna a função filha. Portanto, ambos os exemplos avaliam a função identidade .

Funções que operam em funções

No cálculo lambda, as funções são consideradas ' valores de primeira classe ', portanto, as funções podem ser usadas como entradas ou retornadas como saídas de outras funções.

Por exemplo,representa a função identidade ,, e representa a função identidade aplicada a . Avançar,representa a função constante , a função que sempre retorna , não importa a entrada. No cálculo lambda, a aplicação da função é considerada associativa à esquerda , de modo que meios .

Existem várias noções de "equivalência" e "redução" que permitem que termos lambda sejam "reduzidos" a termos lambda "equivalentes".

Equivalência alfa

Uma forma básica de equivalência, definível em termos lambda, é a equivalência alfa. Ele captura a intuição de que a escolha particular de uma variável vinculada, em uma abstração, não importa (geralmente). Por exemplo,esão termos lambda equivalentes a alfa e ambos representam a mesma função (a função de identidade). Os termosenão são alfa-equivalentes, porque eles não estão vinculados a uma abstração. Em muitas apresentações, é comum identificar termos lambda equivalentes a alfa.

As seguintes definições são necessárias para poder definir β-redução:

Variáveis ​​livres

As variáveis ​​livres de um termo são aquelas variáveis ​​não vinculadas por uma abstração. O conjunto de variáveis ​​livres de uma expressão é definido indutivamente:

  • As variáveis ​​livres desão apenas
  • O conjunto de variáveis ​​livres deé o conjunto de variáveis ​​livres de, mas comremovido
  • O conjunto de variáveis ​​livres deé a união do conjunto de variáveis ​​livres dee o conjunto de variáveis ​​livres de.

Por exemplo, o termo lambda que representa a identidadenão tem variáveis ​​livres, mas a funçãotem uma única variável livre,.

Substituições que evitam a captura

Suponha,esão termos lambda eesão variáveis. A notação indica substituição de por dentro de forma a evitar a captura . Isso é definido para que:

  • ;
  • E se ;
  • ;
  • ;
  • E se e não está nas variáveis ​​livres de . A variável é dito ser "fresco" para .

Por exemplo,, e.

A condição de frescor (exigindo que não está nas variáveis ​​livres de ) é crucial para garantir que a substituição não altere o significado das funções. Por exemplo, uma substituição feita que ignora a condição de atualização pode levar a erros:. Esta substituição torna a função constantena identidadepor substituição.

Em geral, a falha em atender à condição de frescor pode ser corrigida pela renomeação alfa com uma variável fresca adequada. Por exemplo, voltando à nossa noção correta de substituição, ema abstração pode ser renomeada com uma nova variável, obter, e o significado da função é preservado por substituição.

β-redução

A regra de redução β afirma que uma aplicação da formareduz ao prazo. A notaçãoé usado para indicar queβ-reduz a. Por exemplo, para cada,. Isso demonstra querealmente é a identidade. Similarmente,, o que demonstra queé uma função constante.

O cálculo lambda pode ser visto como uma versão idealizada de uma linguagem de programação funcional, como Haskell ou Standard ML . Sob essa visão, a β-redução corresponde a uma etapa computacional. Esta etapa pode ser repetida por reduções β adicionais até que não haja mais aplicações para reduzir. No cálculo lambda não tipado, conforme apresentado aqui, esse processo de redução pode não terminar. Por exemplo, considere o termo. Aqui. Ou seja, o termo se reduz a si mesmo em uma única β-redução e, portanto, o processo de redução nunca terminará.

Outro aspecto do cálculo lambda não tipado é que ele não distingue entre diferentes tipos de dados. Por exemplo, pode ser desejável escrever uma função que opere apenas em números. No entanto, no cálculo lambda não tipado, não há como impedir que uma função seja aplicada a valores de verdade , strings ou outros objetos não numéricos.

Definição formal

Definição

As expressões lambda são compostas por:

  • variáveis v 1 , v 2 , ...;
  • os símbolos de abstração λ (lambda) e . (ponto);
  • parênteses ().

O conjunto de expressões lambda, Λ , pode ser definido indutivamente :

  1. Se x é uma variável, então x ∈ Λ.
  2. Se x é uma variável e M ∈ Λ, então x . M ) ∈ Λ.
  3. Se M , N ∈ Λ, então ( MN ) ∈ Λ.

As instâncias da regra 2 são conhecidas como abstrações e as instâncias da regra 3 são conhecidas como aplicativos . [15] [16]

Notação

Para manter a notação das expressões lambda organizada, as seguintes convenções geralmente são aplicadas:

  • Os parênteses mais externos são eliminados: M N em vez de ( M N ).
  • As aplicações são assumidas como associativas à esquerda: M N P pode ser escrito em vez de (( M N ) P ). [17]
  • O corpo de uma abstração se estende o mais à direita possível : λ x . MN significa λx . ( MN ) e não ( λx.M ) N .
  • Uma sequência de abstrações é contratada: λ xyz . N é abreviado como λ xyz . N. _ [18] [17]

Variáveis ​​livres e vinculadas

Diz-se que o operador de abstração, λ, liga sua variável onde quer que ela ocorra no corpo da abstração. As variáveis ​​que se enquadram no escopo de uma abstração são ditas vinculadas . Em uma expressão λ x . M , a parte λ x é freqüentemente chamada de binder , como uma dica de que a variável x está sendo vinculada ao anexar λ x a M . Todas as outras variáveis ​​são chamadas de livres . Por exemplo, na expressão λ y . xxy , y é uma variável vinculada e xé uma variável livre. Além disso, uma variável é limitada por sua abstração mais próxima. No exemplo a seguir, a única ocorrência de x na expressão está vinculada ao segundo lambda: λ x . y (λx . zx ) .

O conjunto de variáveis ​​livres de uma expressão lambda, M , é denotado como FV( M ) e é definido por recursão na estrutura dos termos, como segue:

  1. FV( x ) = { x }, onde x é uma variável.
  2. FV(λ x . M ) = FV( M ) \ { x }.
  3. FV( MN ) = FV( M ) ∪FV( N ). [19]

Uma expressão que não contém variáveis ​​livres é dita fechada . Expressões lambda fechadas também são conhecidas como combinadores e são equivalentes a termos em lógica combinatória .

Redução

O significado das expressões lambda é definido pela forma como as expressões podem ser reduzidas. [20]

Existem três tipos de redução:

  • α-conversão : variável de limite variável;
  • β-redução : aplicando funções aos seus argumentos;
  • η-redução : que captura uma noção de extensionalidade.

Também falamos das equivalências resultantes: duas expressões são α-equivalentes , se elas podem ser α-convertidas na mesma expressão. A β-equivalência e a η-equivalência são definidas de forma semelhante.

O termo redex , abreviação de expressão redutível , refere-se a subtermos que podem ser reduzidos por uma das regras de redução. Por exemplo, (λ x . M ) N é um β-redex ao expressar a substituição de N por x em M . A expressão à qual um redex reduz é chamada de redução ; o redutor de (λ x . M ) N é M [ x  := N ].

Se x não é livre em M , λ x . M x também é um η-redex, com um redutor de M .

α-conversão

A conversão α, às vezes conhecida como renomeação α, [21] permite que os nomes das variáveis ​​vinculadas sejam alterados. Por exemplo, α-conversão de λ x . x pode render λ y . sim _ Os termos que diferem apenas pela conversão α são chamados de equivalentes α . Freqüentemente, em usos de cálculo lambda, os termos α-equivalentes são considerados equivalentes.

As regras precisas para conversão α não são completamente triviais. Primeiro, ao converter α uma abstração, as únicas ocorrências de variáveis ​​que são renomeadas são aquelas que estão vinculadas à mesma abstração. Por exemplo, uma conversão α de λ xx . x pode resultar em λ yx . x , mas não poderia resultar em λ yx . sim _ Este último tem um significado diferente do original. Isso é análogo à noção de programação de sombreamento variável .

Em segundo lugar, a conversão α não é possível se resultar em uma variável sendo capturada por uma abstração diferente. Por exemplo, se substituirmos x por y em λ xy . x , obtemos λ yy . y , o que não é o mesmo.

Em linguagens de programação com escopo estático, a conversão α pode ser usada para simplificar a resolução de nomes , garantindo que nenhum nome de variável mascare um nome em um escopo contido (consulte α-renomeação para tornar a resolução de nomes trivial ).

Na notação do índice De Bruijn , quaisquer dois termos equivalentes a α são sintaticamente idênticos.

Substituição

A substituição, escrita M [ V  := N ], é o processo de substituir todas as ocorrências livres da variável V na expressão M pela expressão N . A substituição em termos do cálculo lambda é definida por recursão na estrutura dos termos, como segue (nota: x e y são apenas variáveis ​​enquanto M e N são qualquer expressão lambda):

x [ x  := N ] = N
y [ x  := N ] = y , se xy
( M 1 M 2 )[ x  := N ] = M 1 [ x  := N ] M 2 [ x  := N ]
x . M )[ x  := N ] = λ x . M
y . M )[ x  := N ] = λ y .( M [ x  := N ]), se xy e y ∉ FV( N )

Para substituir em uma abstração, às vezes é necessário α-converter a expressão. Por exemplo, não é correto para (λ x . y )[ y  := x ] resultar em λ x . x , porque o x substituído deveria ser livre, mas acabou sendo vinculado. A substituição correta neste caso é λ z . x , até α-equivalência. A substituição é definida exclusivamente até a α-equivalência.

β-redução

A β-redução captura a ideia de aplicação da função. A β-redução é definida em termos de substituição: a β-redução de (λ V . M ) N é M [ V  := N ].

Por exemplo, assumindo alguma codificação de 2, 7, ×, temos a seguinte β-redução: (λ n . n × 2) 7 → 7 × 2.

A β-redução pode ser vista como o mesmo conceito de redutibilidade local na dedução natural , via isomorfismo de Curry-Howard .

η-redução

η-redução expressa a ideia de extensionalidade , que neste contexto é que duas funções são as mesmas se e somente se elas dão o mesmo resultado para todos os argumentos. η-redução converte entre λ x . f x e f sempre que x não aparece livre em f .

η-redução pode ser visto como o mesmo que o conceito de completude local na dedução natural , via isomorfismo de Curry-Howard .

Formas normais e confluência

Para o cálculo lambda não tipado, a β-redução como regra de reescrita não é normalizadora forte nem normalizadora fraca .

No entanto, pode-se mostrar que a β-redução é confluente quando se trabalha até a α-conversão (ou seja, consideramos duas formas normais iguais se for possível α-converter uma na outra).

Portanto, tanto os termos de normalização forte quanto os termos de normalização fraca têm uma única forma normal. Para termos de normalização forte, qualquer estratégia de redução garante a obtenção da forma normal, enquanto para termos de normalização fraca, algumas estratégias de redução podem falhar em encontrá-la.

Tipos de dados de codificação

O cálculo lambda básico pode ser usado para modelar booleanos, aritmética , estruturas de dados e recursão, conforme ilustrado nas subseções a seguir.

Aritmética em cálculo lambda

Existem várias maneiras possíveis de definir os números naturais no cálculo lambda, mas de longe as mais comuns são os numerais da Igreja , que podem ser definidos da seguinte forma:

0 := λ fx . x
1 : = λf.λx. _ f x
2 : = λf.λx. _ f ( fx ) _
3 : = λf.λx. _ f ( f ( fx ) )

e assim por diante. Ou usando a sintaxe alternativa apresentada acima em Notação :

0 := λfx . x
1 := λfx . f x
2 := λfx . f ( fx ) _
3 := λfx . f ( f ( fx ) )

Um numeral Church é uma função de ordem superior — ele recebe uma função de argumento único f e retorna outra função de argumento único. O numeral de igreja n é uma função que recebe uma função f como argumento e retorna a n -ésima composição de f , ou seja, a função f composta consigo mesma n vezes. Isso é denotado por f ( n ) e é de fato a n -ésima potência de f (considerada como um operador); f (0) é definida como a função identidade. Tais composições repetidas (de uma única função f) obedecem às leis dos expoentes , razão pela qual esses numerais podem ser usados ​​para aritmética. (No cálculo lambda original de Church, era necessário que o parâmetro formal de uma expressão lambda ocorresse pelo menos uma vez no corpo da função, o que tornava impossível a definição de 0 acima.)

Uma maneira de pensar sobre o numeral da Igreja n , que geralmente é útil ao analisar programas, é como uma instrução 'repita n vezes'. Por exemplo, usando as funções PAIR e NIL definidas abaixo, pode-se definir uma função que constrói uma lista (ligada) de n elementos todos iguais a x repetindo 'prefixar outro elemento x ' n vezes, começando de uma lista vazia. O termo lambda é

λn.λx. _ _ _ _ n (PAR x ) NIL

Variando o que está sendo repetido, e variando o argumento ao qual a função que está sendo repetida é aplicada, muitos efeitos diferentes podem ser alcançados.

Podemos definir uma função sucessora, que recebe um numeral de Igreja n e retorna n + 1 adicionando outra aplicação de f , onde '(mf)x' significa que a função 'f' é aplicada 'm' vezes em 'x':

SUCC := λ nfx . f ( nfx ) _ _

Como a m -ésima composição de f composta com a n -ésima composição de f dá a m + n -ésima composição de f , a adição pode ser definida da seguinte forma:

MAIS := λ mnfx . mf ( nfx ) _ _ _

PLUS pode ser pensado como uma função que recebe dois números naturais como argumentos e retorna um número natural; pode-se verificar que

MAIS 2 3

e

5

são expressões lambda equivalentes β. Como adicionar m a um número n pode ser feito adicionando 1 m vezes, uma definição alternativa é:

MAIS := λ mn . m SUCC n  [22]

Da mesma forma, a multiplicação pode ser definida como

MULT := λ mnf . m ( n f ) [18]

alternativamente

MULT := λ mn . m (mais n ) 0

já que multiplicar m e n é o mesmo que repetir a função add n m vezes e depois aplicá-la a zero. A exponenciação tem uma tradução bastante simples em algarismos da Igreja, ou seja,

POW := λ be . eb [ 19 ]

A função predecessora definida por PRED n = n − 1 para um inteiro positivo n e PRED 0 = 0 é consideravelmente mais difícil. A fórmula

PRED := λ nfx . ngh . h ( g f )) (λ u . x ) (λ u . u )

pode ser validado mostrando indutivamente que se T denota gh . h ( g f )) , então T ( n )u . x ) = (λ h . h ( f ( n −1) ( x ))) para n > 0 . Duas outras definições de PRED são fornecidas abaixo, uma usando condicionais e a outra usando pares . Com a função predecessora, a subtração é direta. Definindo

SUB := λ mn . n PRED m ,

SUB m n produz mn quando m > n e 0 caso contrário.

Lógica e predicados

Por convenção, as duas definições a seguir (conhecidas como Church booleans) são usadas para os valores booleanos TRUE e FALSE :

VERDADEIRO := λ xy . x
FALSO := λ xy . y
(Observe que FALSE é equivalente ao número zero da Igreja definido acima)

Então, com esses dois termos lambda, podemos definir alguns operadores lógicos (estas são apenas formulações possíveis; outras expressões estão igualmente corretas):

E := λ pq . p q p
OU := λ pq . p p q
NÃO := λp . p FALSO VERDADEIRO
IFTHENELSE := λ pab . p a b

Agora podemos calcular algumas funções lógicas, por exemplo:

E VERDADEIRO FALSO
≡ (λ pq . p q p ) VERDADEIRO FALSO → β VERDADEIRO FALSO VERDADEIRO
≡ (λ xy . x ) FALSO VERDADEIRO → β FALSO

e vemos que AND TRUE FALSE é equivalente a FALSE .

Um predicado é uma função que retorna um valor booleano. O predicado mais fundamental é ISZERO , que retorna TRUE se seu argumento for o numeral Church 0 , e FALSE se seu argumento for qualquer outro numeral Church:

ISZERO := λ n . nx .FALSO) VERDADEIRO

O predicado a seguir testa se o primeiro argumento é menor ou igual ao segundo:

LEQ := λ mn .ISZERO (SUB m n ) ,

e como m = n , se LEQ m n e LEQ n m , é direto construir um predicado para igualdade numérica.

A disponibilidade de predicados e a definição acima de TRUE e FALSE tornam conveniente escrever expressões "if-then-else" em cálculo lambda. Por exemplo, a função predecessora pode ser definida como:

PRED := λ n . ngk .ISZERO ( g 1) k (MAIS ( g k ) 1)) (λ v .0) 0

que pode ser verificado mostrando indutivamente que ngk .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) é a função add n − 1 para n > 0.

Pares

Um par (2-tupla) pode ser definido em termos de TRUE e FALSE , usando a codificação Church para pairs . Por exemplo, PAIR encapsula o par ( x , y ), FIRST retorna o primeiro elemento do par e SECOND retorna o segundo.

PAR := λ xyf . f x y
PRIMEIRO := λ p . p VERDADEIRO
SEGUNDO := λ p . p FALSO
NIL := λ x .TRUE
NULL := λ p . pxy .FALSO)

Uma lista encadeada pode ser definida como NIL para a lista vazia ou como PAIR de um elemento e uma lista menor. O predicado NULL testa o valor NIL . (Alternativamente, com NIL := FALSE , a construção lhtz .deal_with_head_ h _and_tail_ t ) (deal_with_nil) elimina a necessidade de um teste NULL explícito).

Como exemplo do uso de pares, a função shift-and-increment que mapeia ( m , n ) para ( n , n + 1) pode ser definida como

Φ := λ x .PAR (SEGUNDO x ) (SUCC (SEGUNDO x ))

o que nos permite dar talvez a versão mais transparente da função predecessora:

PRED := λ n .PRIMEIRO ( n Φ (PAR 0 0)).

Técnicas de programação adicionais

Existe um corpo considerável de idiomas de programação para cálculo lambda. Muitos deles foram originalmente desenvolvidos no contexto do uso do cálculo lambda como base para a semântica da linguagem de programação , efetivamente usando o cálculo lambda como uma linguagem de programação de baixo nível . Como várias linguagens de programação incluem o cálculo lambda (ou algo muito semelhante) como um fragmento, essas técnicas também são usadas na programação prática, mas podem ser percebidas como obscuras ou estrangeiras.

Constantes nomeadas

No cálculo lambda, uma biblioteca assumiria a forma de uma coleção de funções previamente definidas, que como termos lambda são apenas constantes particulares. O cálculo lambda puro não tem um conceito de constantes nomeadas, pois todos os termos lambda atômicos são variáveis, mas pode-se emular tendo constantes nomeadas deixando de lado uma variável como o nome da constante, usando abstração para vincular essa variável no corpo principal , e aplique essa abstração à definição pretendida. Assim, para usar f para significar M (algum termo lambda explícito) em N (outro termo lambda, o "programa principal"), pode-se dizer

f . N ) M

Os autores geralmente introduzem açúcar sintático , como let , para permitir escrever o acima na ordem mais intuitiva

seja f = M em N

Ao encadear tais definições, pode-se escrever um "programa" de cálculo lambda como zero ou mais definições de função, seguido por um termo lambda usando as funções que constituem o corpo principal do programa.

Uma restrição notável deste let é que o nome f não está definido em M , já que M está fora do escopo da ligação de abstração f ; isso significa que uma definição de função recursiva não pode ser usada como o M com let . A construção de açúcar sintática letrec mais avançada que permite escrever definições de funções recursivas nesse estilo ingênuo, em vez disso, emprega combinadores de ponto fixo.

Recursão e pontos fixos

Recursão é a definição de uma função usando a própria função. O cálculo lambda não pode expressar isso tão diretamente quanto algumas outras notações: todas as funções são anônimas no cálculo lambda, então não podemos nos referir a um valor que ainda não foi definido, dentro do termo lambda que define esse mesmo valor. No entanto, a recursão ainda pode ser alcançada organizando uma expressão lambda para receber a si mesma como seu valor de argumento, por exemplo em  x . x x ) E .

Considere a função fatorial F( n ) recursivamente definida por

F( n ) = 1, se n = 0; senão n × F( n − 1) .

Na expressão lambda que deve representar esta função, um parâmetro (normalmente o primeiro) será assumido para receber a própria expressão lambda como seu valor, de modo que chamá-la – aplicando-a a um argumento – resultará em recursão. Assim, para alcançar a recursão, o argumento pretendido como auto-referência (chamado r aqui) deve sempre ser passado para si mesmo dentro do corpo da função, em um ponto de chamada:

G := λ r . λ n .(1, se n = 0; senão n × ( r r ( n −1)))
com  r r x = F x = G r x  para segurar, então  r = G  e
F := GG = (λ x . x x ) G

A auto-aplicação obtém a replicação aqui, passando a expressão lambda da função para a próxima invocação como um valor de argumento, tornando-a disponível para ser referenciada e chamada lá.

Isso resolve, mas requer reescrever cada chamada recursiva como auto-aplicação. Gostaríamos de ter uma solução genérica, sem a necessidade de reescrever:

G := λ r . λ n .(1, se n = 0; senão n × ( r ( n −1)))
com  r x = F x = G r x  para segurar, então  r = G r =: FIX G  e
F := FIX G  where  FIX g := (r where r = g r) = g (FIX g)
so that  FIX G = G (FIX G) = (λn.(1, if n = 0; else n × ((FIX G) (n−1))))

Dado um termo lambda com o primeiro argumento representando a chamada recursiva (por exemplo , G aqui), o combinador de ponto fixo FIX retornará uma expressão lambda auto-replicante representando a função recursiva (aqui, F ). A função não precisa ser explicitamente passada para si mesma em nenhum ponto, pois a autorreplicação é organizada antecipadamente, quando é criada, para ser feita toda vez que for chamada. Assim, a expressão lambda original (FIX G) é recriada dentro de si mesma, no ponto de chamada, alcançando a auto-referência .

De fato, existem muitas definições possíveis para este operador FIX , sendo a mais simples delas:

Y  := λ g .(λ x . g ( x x )) (λ x . g ( x x ))

No cálculo lambda, Y g   é um ponto fixo de g , à medida que se expande para:

Y g
h .(λ x . h ( x x )) (λ x . h ( x x ))) g
x . g ( x x )) (λ x . g ( x x ))
g ((λ x . g ( x x )) (λ x . g ( x x )))
g ( Y g )

Agora, para realizar nossa chamada recursiva para a função fatorial, simplesmente chamaríamos ( Y G) n , onde n é o número para o qual estamos calculando o fatorial. Dado n = 4, por exemplo, isso dá:

( Y G) 4
G ( Y G) 4
rn .(1, se n = 0; senão n × ( r ( n −1)))) ( Y G) 4
n .(1, se n = 0; senão n × (( Y G) ( n −1))))) 4
1, se 4 = 0; senão 4 × (( Y G) (4−1))
4 × (G ( Y G) (4−1))
4 × ((λ n .(1, se n = 0; senão n × (( Y G) ( n −1)))) (4−1))
4 × (1, se 3 = 0; senão 3 × (( Y G) (3−1)))
4 × (3 × (G ( Y G) (3−1)))
4 × (3 × ((λ n .(1, se n = 0; senão n × (( Y G) ( n −1)))) (3−1)))
4 × (3 × (1, se 2 = 0; senão 2 × (( Y G) (2−1))))
4 × (3 × (2 × (G ( Y G) (2−1))))
4 × (3 × (2 × ((λ n .(1, se n = 0; senão n × (( Y G) ( n −1)))) (2−1))))
4 × (3 × (2 × (1, se 1 = 0; senão 1 × (( Y G) (1−1))))))
4 × (3 × (2 × (1 × (G ( Y G) (1−1))))))
4 × (3 × (2 × (1 × ((λ n .(1, se n = 0; senão n × (( Y G) ( n −1)))) (1−1))))))
4 × (3 × (2 × (1 × (1, se 0 = 0; senão 0 × (( Y G) (0−1)))))))
4 × (3 × (2 × (1 × (1))))
24

Toda função definida recursivamente pode ser vista como um ponto fixo de alguma função definida adequadamente fechando a chamada recursiva com um argumento extra e, portanto, usando Y , toda função definida recursivamente pode ser expressa como uma expressão lambda. Em particular, agora podemos definir claramente o predicado de subtração, multiplicação e comparação de números naturais recursivamente.

Termos padrão

Certos termos têm nomes comumente aceitos: [23] [24] [25]

I  := λ x . x
S  := λ xyz . xz ( yz ) _ _
K  := λ xy . x
B  := λ xyz . x ( yz ) _
C  := λ xyz . x z y
W  := λ xy . x y y
ω ou Δ  := λ x . x x
Ω  := ω ω

I é a função identidade. SK e BCKW formam sistemas completos de cálculo combinador que podem expressar qualquer termo lambda – veja a próxima seção . Ω é Y I , o menor termo que não tem forma normal. Y é padrão e definido acima . VERDADEIRO e FALSO definidos acima são comumente abreviados como T e F .

Eliminação de abstração

Se N é um termo lambda sem abstração, mas possivelmente contendo constantes nomeadas ( combinadores ), então existe um termo lambda T ( x , N ) que é equivalente a λ x . N mas carece de abstração (exceto como parte das constantes nomeadas, se estas forem consideradas não atômicas). Isso também pode ser visto como variáveis ​​de anonimização, pois T ( x , N ) remove todas as ocorrências de x de N , enquanto ainda permite que os valores dos argumentos sejam substituídos nas posições onde N contém um x. A função de conversão T pode ser definida por:

T ( x , x ):= I
T ( x , N ) := K N se x não é livre em N .
T ( x , M N ) := S T ( x , M ) T ( x , N )

Em ambos os casos, um termo da forma T ( x , N ) P pode reduzir fazendo com que o combinador inicial I , K ou S pegue o argumento P , exatamente como a redução β de x . N ) P faria. Eu retorna esse argumento. K descarta o argumento, assim como x . N ) faria se x não tivesse ocorrência livre em N . S passa o argumento para ambos os subtermos do aplicativo e, em seguida, aplica o resultado do primeiro ao resultado do segundo.

Os combinadores B e C são semelhantes a S , mas passam o argumento para apenas um subtermo de uma aplicação ( B para o subtermo "argumento" e C para o subtermo "função"), salvando assim um K subsequente se não houver ocorrência de x em um subtermo. Em comparação com B e C , o combinador S na verdade combina duas funcionalidades: reorganizar argumentos e duplicar um argumento para que possa ser usado em dois lugares. O combinador W faz apenas o último, produzindo o sistema B, C, K, W como uma alternativa paraCálculo combinador SKI .

Cálculo lambda digitado

Um cálculo lambda tipado é um formalismo tipado que usa o símbolo lambda () para denotar abstração de função anônima. Nesse contexto, os tipos geralmente são objetos de natureza sintática que são atribuídos a termos lambda; a natureza exata de um tipo depende do cálculo considerado (consulte Tipos de cálculos lambda tipados ). De um certo ponto de vista, os cálculos lambda tipados podem ser vistos como refinamentos do cálculo lambda não tipado, mas de outro ponto de vista, eles também podem ser considerados a teoria mais fundamental e o cálculo lambda não tipado um caso especial com apenas um tipo. [26]

Os cálculos lambda tipados são linguagens de programação fundamentais e são a base de linguagens de programação funcionais tipadas , como ML e Haskell e, mais indiretamente, linguagens de programação imperativas tipadas . Cálculos lambda tipados desempenham um papel importante no projeto de sistemas de tipos para linguagens de programação; aqui a tipabilidade geralmente captura as propriedades desejáveis ​​do programa, por exemplo, o programa não causará uma violação de acesso à memória.

Os cálculos lambda tipados estão intimamente relacionados à lógica matemática e à teoria da prova através do isomorfismo de Curry-Howard e podem ser considerados como a linguagem interna das classes de categorias , por exemplo, o cálculo lambda simplesmente tipado é a linguagem das categorias fechadas cartesianas (CCCs).

Estratégias de redução

Se um termo está normalizando ou não, e quanto trabalho precisa ser feito para normalizá-lo, se estiver, depende em grande parte da estratégia de redução usada. As estratégias comuns de redução de cálculo lambda incluem: [27]

Ordem normal
O redex mais à esquerda e mais externo é sempre reduzido primeiro. Ou seja, sempre que possível os argumentos são substituídos no corpo de uma abstração antes que os argumentos sejam reduzidos.
Pedido de pedido
O redex mais à esquerda e mais interno é sempre reduzido primeiro. Intuitivamente, isso significa que os argumentos de uma função são sempre reduzidos antes da própria função. A ordem do aplicativo sempre tenta aplicar funções a formas normais, mesmo quando isso não for possível.
β-reduções completas
Qualquer redex pode ser reduzido a qualquer momento. Isso significa essencialmente a falta de qualquer estratégia de redução específica - com relação à redutibilidade, "todas as apostas estão canceladas".

Estratégias de redução fracas não reduzem sob abstrações lambda:

Chamada por valor
Um redex é reduzido apenas quando seu lado direito é reduzido a um valor (variável ou abstração). Apenas os redexes mais externos são reduzidos.
Chamar pelo nome
Como ordem normal, mas nenhuma redução é realizada dentro de abstrações. Por exemplo, λ x .(λ x . x ) x está na forma normal de acordo com essa estratégia, embora contenha o redex x . x ) x .

Estratégias com compartilhamento reduzem computações que são "iguais" em paralelo:

Redução ideal
Como ordem normal, mas os cálculos que têm o mesmo rótulo são reduzidos simultaneamente.
Ligue por necessidade
Como chamar pelo nome (portanto, fraco), mas aplicativos de função que duplicariam termos, em vez disso, nomeiam o argumento, que é reduzido apenas "quando necessário".

Computabilidade

Não há algoritmo que receba como entrada duas expressões lambda e produza VERDADEIRO ou FALSO , dependendo se uma expressão se reduz à outra. [10] Mais precisamente, nenhuma função computável pode decidir a questão. Este foi historicamente o primeiro problema para o qual a indecidibilidade pôde ser provada. Como de costume para tal prova, computável significa computável por qualquer modelo de computação que seja Turing completo . De fato, a própria computabilidade pode ser definida através do cálculo lambda: uma função F : NNde números naturais é uma função computável se e somente se existe uma expressão lambda f tal que para cada par de x , y em N , F ( x )= y se e somente se f x  = β y , onde x e y são os algarismos Church correspondentes a xey , respectivamente e = β significando equivalência com β-redução. Veja a tese de Church-Turing para outras abordagens para definir computabilidade e sua equivalência.  

A prova de incomputabilidade de Church primeiro reduz o problema para determinar se uma determinada expressão lambda tem uma forma normal . Em seguida, ele assume que esse predicado é computável e, portanto, pode ser expresso em cálculo lambda. Com base em trabalhos anteriores de Kleene e construindo uma numeração de Gödel para expressões lambda, ele constrói uma expressão lambda e que segue de perto a prova do primeiro teorema da incompletude de Gödel . Se e for aplicado ao seu próprio número de Gödel, resulta uma contradição.

Complexidade

A noção de complexidade computacional para o cálculo lambda é um pouco complicada, pois o custo de uma β-redução pode variar dependendo de como ela é implementada. [28] Para ser preciso, deve-se, de alguma forma, encontrar a localização de todas as ocorrências da variável ligada V na expressão E , implicando um custo de tempo, ou deve-se acompanhar de alguma forma a localização das variáveis ​​livres, implicando uma custo do espaço. Uma busca ingênua pelas localizações de V em E é O ( n ) no comprimento n de E. Strings do diretorforam uma abordagem inicial que trocou esse custo de tempo por um uso quadrático do espaço. [29] De maneira mais geral, isso levou ao estudo de sistemas que usam substituição explícita .

Em 2014 foi mostrado que o número de passos de β-redução tomados pela redução de ordem normal para reduzir um termo é um modelo de custo de tempo razoável , ou seja, a redução pode ser simulada em uma máquina de Turing em tempo polinomialmente proporcional ao número de passos . [30] Este era um problema aberto de longa data, devido à explosão de tamanho , a existência de termos lambda que crescem exponencialmente em tamanho para cada β-redução. O resultado contorna isso trabalhando com uma representação compartilhada compacta. O resultado deixa claro que a quantidade de espaço necessária para avaliar um termo lambda não é proporcional ao tamanho do termo durante a redução. Não se sabe atualmente qual seria uma boa medida de complexidade espacial. [31]

Um modelo irracional não significa necessariamente ineficiente. A redução ótima reduz todos os cálculos com o mesmo rótulo em uma etapa, evitando trabalho duplicado, mas o número de etapas de redução β paralelas para reduzir um determinado termo à forma normal é aproximadamente linear no tamanho do termo. Isso é muito pequeno para ser uma medida de custo razoável, pois qualquer máquina de Turing pode ser codificada no cálculo lambda em tamanho linearmente proporcional ao tamanho da máquina de Turing. O verdadeiro custo da redução dos termos lambda não se deve à β-redução em si, mas sim ao manuseio da duplicação de redexs durante a β-redução. [32]Não se sabe se implementações de redução ótima são razoáveis ​​quando medidas em relação a um modelo de custo razoável, como o número de etapas mais externas à esquerda para a forma normal, mas foi demonstrado para fragmentos do cálculo lambda que o algoritmo de redução ótima é eficiente e tem no máximo uma sobrecarga quadrática em comparação com o mais externo à esquerda. [31] Além disso, a implementação do protótipo BOHM de redução ótima superou tanto Caml Light quanto Haskell em termos lambda puros. [32]

Cálculo lambda e linguagens de programação

Conforme apontado pelo artigo de 1965 de Peter Landin "A Correspondence between ALGOL 60 and Church's Lambda-notation", [33] linguagens de programação procedural sequenciais podem ser entendidas em termos do cálculo lambda, que fornece os mecanismos básicos para abstração procedural e procedimento (subprograma).

Funções anônimas

Por exemplo, em Lisp a função "quadrado" pode ser expressa como uma expressão lambda da seguinte forma:

( lambda  ( x )  ( *  x  x ))

O exemplo acima é uma expressão que resulta em uma função de primeira classe. O símbolo lambdacria uma função anônima, dada uma lista de nomes de parâmetros, (x)– apenas um único argumento neste caso, e uma expressão que é avaliada como o corpo da função, (* x x). As funções anônimas às vezes são chamadas de expressões lambda.

Por exemplo, Pascal e muitas outras linguagens imperativas há muito suportam a passagem de subprogramas como argumentos para outros subprogramas através do mecanismo de ponteiros de função . No entanto, os ponteiros de função não são uma condição suficiente para que as funções sejam tipos de dados de primeira classe , porque uma função é um tipo de dados de primeira classe se e somente se novas instâncias da função puderem ser criadas em tempo de execução. E essa criação de funções em tempo de execução é suportada em Smalltalk , JavaScript e Wolfram Language , e mais recentemente em Scala , Eiffel ("agentes"), C# ("delegates") eC++11 , entre outros.

Paralelismo e simultaneidade

A propriedade de Church–Rosser do cálculo lambda significa que a avaliação (β-redução) pode ser realizada em qualquer ordem , mesmo em paralelo. Isso significa que várias estratégias de avaliação não determinísticas são relevantes. No entanto, o cálculo lambda não oferece nenhuma construção explícita para paralelismo . Pode-se adicionar construções como Futures ao cálculo lambda. Outros cálculos de processo foram desenvolvidos para descrever a comunicação e a concorrência.

Semântica

O fato de termos de cálculo lambda atuarem como funções em outros termos de cálculo lambda, e até mesmo em si mesmos, levou a questões sobre a semântica do cálculo lambda. Poderia um significado sensato ser atribuído aos termos do cálculo lambda? A semântica natural foi encontrar um conjunto D isomórfico ao espaço de funções DD , de funções sobre si mesmo. No entanto, nenhum D não trivial pode existir, por restrições de cardinalidade porque o conjunto de todas as funções de D a D tem cardinalidade maior que D , a menos que D seja um conjunto singleton .

In the 1970s, Dana Scott showed that if only continuous functions were considered, a set or domain D with the required property could be found, thus providing a model for the lambda calculus.

This work also formed the basis for the denotational semantics of programming languages.

Variations and extensions

These extensions are in the lambda cube:

Esses sistemas formais são extensões do cálculo lambda que não estão no cubo lambda:

Esses sistemas formais são variações do cálculo lambda:

Esses sistemas formais estão relacionados ao cálculo lambda:

  • Lógica combinatória - Uma notação para lógica matemática sem variáveis
  • Cálculo combinador SKI – Um sistema computacional baseado nos combinadores S , K e I , equivalente ao cálculo lambda, mas redutível sem substituições de variáveis

Veja também

Notas

  1. Para uma história completa, veja "History of Lambda-calculus and Combinatory Logic" de Cardone e Hindley (2006).

Referências

  1. ^ Turing, Alan M. (dezembro de 1937). "Computabilidade e λ-Definibilidade". O Jornal de Lógica Simbólica . 2 (4): 153-163. doi : 10.2307/2268280 . JSTOR  2268280 .
  2. ^ Coquand, Thierry (8 de fevereiro de 2006). Zalta, Edward N. (ed.). "Teoria dos Tipos" . The Stanford Encyclopedia of Philosophy (Verão 2013 ed.) . Recuperado em 17 de novembro de 2020 .
  3. ^ Moortgat, Michael (1988). Investigações Categoriais: Aspectos Lógicos e Linguísticos do Cálculo Lambek . Publicações Foris. ISBN 9789067653879.
  4. ^ Bunt, Harry; Muskens, Reinhard, eds. (2008). Computação Significado . Springer. ISBN 978-1-4020-5957-5.
  5. ^ Mitchell, John C. (2003). Conceitos em Linguagens de Programação . Cambridge University Press. pág. 57. ISBN 978-0-521-78098-8..
  6. ^ Pierce, teoria básica da categoria de Benjamin C. para cientistas de computador . pág. 53.
  7. ^ Igreja, Alonzo (1932). "Um conjunto de postulados para a fundação da lógica". Anais de Matemática . Série 2. 33 (2): 346–366. doi : 10.2307/1968337 . JSTOR 1968337 . 
  8. ^ Kleene, Stephen C. ; Rosser, JB (julho de 1935). "A inconsistência de certas lógicas formais". Os Anais da Matemática . 36 (3): 630. doi : 10.2307/1968646 . JSTOR 1968646 . 
  9. ^ Igreja, Alonzo (dezembro de 1942). "Revisão de Haskell B. Curry, A Inconsistência de Certas Lógicas Formais ". O Jornal de Lógica Simbólica . 7 (4): 170–171. doi : 10.2307/2268117 . JSTOR 2268117 . 
  10. ^ a b Igreja, Alonzo (1936). "Um problema insolúvel da teoria elementar dos números". Revista Americana de Matemática . 58 (2): 345–363. doi : 10.2307/2371045 . JSTOR 2371045 . 
  11. ^ Igreja, Alonzo (1940). "Uma formulação da teoria simples dos tipos". Jornal de lógica simbólica . 5 (2): 56–68. doi : 10.2307/2266170 . JSTOR 2266170 . 
  12. ^ Partee, BBH; ter Meulen, A. ; Parede, RE (1990). Métodos Matemáticos em Lingüística . Springer. ISBN 9789027722454. Recuperado em 29 de dezembro de 2016 .
  13. ^ Alma, Jessé. Zalta, Edward N. (ed.). "O Cálculo Lambda" . The Stanford Encyclopedia of Philosophy (Verão 2013 ed.) . Recuperado em 17 de novembro de 2020 .
  14. Dana Scott, " Looking Backward; Looking Forward ", Palestra Convidada no Workshop em homenagem ao 85º aniversário de Dana Scott e 50 anos de teoria de domínio, 7–8 de julho, FLoC 2018 (conversa em 7 de julho de 2018). A passagem relevante começa às 32:50 . (Veja também este trecho de uma palestra de maio de 2016 na Universidade de Birmingham, Reino Unido.)
  15. ^ Barendregt, Hendrik Pieter (1984). O cálculo lambda: sua sintaxe e semântica . Estudos em Lógica e os Fundamentos da Matemática. Vol. 103 (edição revisada). Holanda do Norte. ISBN 0-444-87508-5.
  16. ^ Correções .
  17. ^ a b "Exemplo de regras de associatividade" . Lambda-bound . com . Recuperado 2012-06-18 .
  18. ^ a b Selinger, Peter (2008), Lecture Notes on the Lambda Calculus (PDF) , vol. 0804, Departamento de Matemática e Estatística, Universidade de Ottawa, p. 9, arXiv : 0804.3434 , Bibcode : 2008arXiv0804.3434S
  19. ^ a b Barendregt, Henk ; Barendsen, Erik (março de 2000), Introdução ao cálculo lambda (PDF)
  20. ^ de Queiroz, Ruy JGB (1988). "Uma Conta Teórica de Prova de Programação e o Papel das Regras de Redução". Dialética . 42 (4): 265–282. doi : 10.1111/j.1746-8361.1988.tb00919.x .
  21. ^ Turbak, Franklyn; Gifford, David (2008), Conceitos de design em linguagens de programação , MIT press, p. 251, ISBN 978-0-262-20175-9
  22. ^ Felleisen, Matthias; Flatt, Matthew (2006), Programming Languages and Lambda Calculi (PDF), p. 26, archived from the original (PDF) on 2009-02-05; A note (accessed 2017) at the original location suggests that the authors consider the work originally referenced to have been superseded by a book.
  23. ^ Ker, Andrew D. "Lambda Calculus and Types" (PDF). p. 6. Retrieved 14 January 2022.
  24. ^ Dezani-Ciancaglini, Mariangiola; Ghilezan, Silvia (2014). "Precisão da Subtipagem em Tipos de Interseção e União" (PDF) . Reescrevendo e digitando cálculos lambda . Notas de aula em Ciência da Computação. 8560 : 196. doi : 10.1007/978-3-319-08918-8_14 . hdl : 2318/149874 . ISBN  978-3-319-08917-1. Recuperado em 14 de janeiro de 2022 .
  25. ^ Forster, Yannick; Smolka, Gert (agosto de 2019). "Call-by-Value Lambda Calculus as a Model of Computation in Coq" (PDF) . Jornal de raciocínio automatizado . 63 (2): 393–413. doi : 10.1007/s10817-018-9484-2 . S2CID 53087112 . Recuperado em 14 de janeiro de 2022 .  
  26. ^ Tipos e linguagens de programação, p. 273, Benjamin C. Pierce
  27. ^ Pierce, Benjamin C. (2002). Tipos e Linguagens de Programação . Imprensa do MIT . pág. 56. ISBN 0-262-16209-1.
  28. ^ Frandsen, Gudmund Skovbjerg; Sturtivant, Carl (26 de agosto de 1991). "O que é uma implementação eficiente do \lambda-calculus?" . Anais da 5ª Conferência da ACM sobre Linguagens de Programação Funcionais e Arquitetura de Computadores . Notas de aula em Ciência da Computação. Springer-Verlag. 523 : 289-312. CiteSeerX 10.1.1.139.6913 . doi : 10.1007/3540543961_14 . ISBN  9783540543961.
  29. ^ Sinot, F.-R. (2005). "Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting" (PDF). Journal of Logic and Computation. 15 (2): 201–218. doi:10.1093/logcom/exi010.
  30. ^ Accattoli, Beniamino; Dal Lago, Ugo (14 de julho de 2014). "Redução beta é invariável, de fato" (PDF) . Anais da Reunião Conjunta da Vigésima Terceira Conferência Anual da EACSL sobre Lógica da Ciência da Computação (CSL) e do Vigésimo Nono Simpósio Anual ACM/IEEE sobre Lógica na Ciência da Computação (LICS) : 1–10. arXiv : 1601.01233 . doi : 10.1145/2603088.2603105 . ISBN  9781450328869. S2CID  11485010 .
  31. ^ a b Accattoli, Beniamino (outubro de 2018). "Modelos de (in)eficiência e custo razoável" . Notas Eletrônicas em Informática Teórica . 338 : 23–43. doi : 10.1016/j.entcs.2018.10.003 .
  32. ^ a b Asperti, Andrea (16 de janeiro de 2017). "Sobre a redução eficiente de termos lambda" (PDF) . arXiv : 1701.04240v1 . Recuperado em 19 de agosto de 2021 . {{cite journal}}: Cite journal requires |journal= (help)
  33. ^ Landin, PJ (1965). "Uma correspondência entre ALGOL 60 e a notação Lambda da Igreja". Comunicações da ACM . 8 (2): 89–101. doi : 10.1145/363744.363749 . S2CID 6505810 . 

Leitura adicional

Monografias/livros didáticos para alunos de pós-graduação:

  • Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry–Howard isomorphism , Elsevier, 2006, ISBN 0-444-52077-5 é uma monografia recente que cobre os principais tópicos do cálculo lambda desde a variedade sem tipo, até a mais tipada lambda calculi , incluindo desenvolvimentos mais recentes como sistemas de tipo puro e o cubo lambda . Ele não cobre extensões de subdigitação . 
  • Pierce, Benjamin (2002), Tipos e linguagens de programação , MIT Press, ISBN 0-262-16209-1cobre cálculos lambda de uma perspectiva de sistema de tipo prático; alguns tópicos como tipos dependentes são apenas mencionados, mas a subdigitação é um tópico importante.

Algumas partes deste artigo são baseadas em material do FOLDOC , usado com permissão .

Links externos

  1. ^ Igreja, Alonzo (1941). O Cálculo de Lambda-Conversão . Princeton: Princeton University Press . Recuperado 2020-04-14 .
  2. ^ Frink Jr., Orrin (1944). "Review: The Calculi of Lambda-Conversion by Alonzo Church" (PDF) . Touro. Amer. Matemática. Soc . 50 (3): 169–172. doi : 10.1090/s0002-9904-1944-08090-7 .