Cálculo lambda - Lambda calculus

Lambda calculus (também escrito como λ-calculus ) é um sistema formal em lógica matemática para expressar computação baseada na abstração de função e aplicação usando ligação e substituição de variável . É 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 sobre eles. Na forma mais simples do 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 de função ( M é um termo lambda). A variável x torna-se limitada 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 Renomeando as variáveis ​​associadas na expressão. Usado para evitar colisões de nomes .
((λ x . M ) E ) → ( M [ x  : = E ]) redução β Substituindo as variáveis ​​associadas pela expressão do 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 das etapas 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 pode criar qualquer comportamento de função chamando-a em si mesma em várias combinações.

Explicação e aplicações

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

O cálculo lambda pode ser digitado ou não digitado . No cálculo lambda digitado, as funções podem ser aplicadas apenas se forem capazes de aceitar o "tipo" de dados da entrada fornecida. Os cálculos lambda digitados são mais fracos do que os cálculos lambda não digitados , que é o assunto principal deste artigo, no sentido de que os cálculos lambda digitados podem expressar menos do que os cálculos não digitados, mas, por outro lado, cálculos lambda digitados permitem que mais coisas sejam provadas ; no cálculo lambda simplesmente digitado , é, por exemplo, um teorema que toda estratégia de avaliação termina para cada termo lambda simplesmente digitado, enquanto a avaliação de termos lambda não digitados não precisa terminar. Uma razão pela qual existem muitos cálculos lambda tipados diferentes é 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 da matemática , filosofia , linguística e ciência da computação . O cálculo lambda desempenhou um papel importante no desenvolvimento da teoria das linguagens de programação . Linguagens de programação funcional implementam cálculo lambda. O cálculo lambda também é um tópico de pesquisa atual na teoria das categorias .

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 . O sistema original mostrou ser logicamente inconsistente em 1935, quando Stephen Kleene e JB Rosser desenvolveram o paradoxo de Kleene-Rosser .

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

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 de outros linguistas na semântica da linguagem natural, o cálculo lambda começou a desfrutar de um lugar respeitável tanto na linguística quanto na ciência da computação.

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 “ ” usada 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: um símbolo era necessário e λ por acaso foi escolhido.

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

Caro Professor Church,

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 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 matemática. O cálculo lambda fornece uma semântica simples para computação, permitindo que propriedades de 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 dar-lhes nomes explícitos. Por exemplo, a função

pode ser reescrito de forma anônima como

(que é lido como "um tuplo de x e y é mapeado 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 a funçã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

Este 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.

A aplicação da função da função aos argumentos (5, 2), produz de uma vez

,

enquanto a avaliação da versão curry requer mais uma etapa

// a definição de foi usada com na expressão interna. Isso é como a redução β.
// a definição de foi usada 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 algumas 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,, é em si um termo lambda válido
  • if é um termo lambda e é uma variável, então (às vezes escrito em ASCII as ) é um termo lambda (chamado de abstração );
  • se e forem 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 é a definição de uma função anônima que é capaz de pegar uma única entrada e substituí-la na expressão . Portanto, define uma função anônima que recebe e retorna . Por exemplo, é uma abstração da função usando o termo para . 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 no termo .

Um aplicativo representa a aplicação de uma função a uma entrada , ou seja, representa o ato de chamar a função na entrada a produzir .

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

O colchete pode ser usado e pode ser necessário para eliminar a ambigüidade dos termos. Por exemplo, e denotam termos diferentes (embora eles 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 de 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 de identidade , e representa a função de identidade aplicada para . Além disso, 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 , o que significa .

Existem várias noções de "equivalência" e "redução" que permitem que os 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 limitada, em uma abstração, (normalmente) não importa. Por exemplo, e são termos lambda equivalentes a alfa, e ambos representam a mesma função (a função de identidade). Os termos e não são equivalentes a alfa, porque 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 definir a redução β:

Variáveis ​​livres

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

  • As variáveis ​​livres de são apenas
  • O conjunto de variáveis ​​livres de é o conjunto de variáveis ​​livres de , mas com removido
  • O conjunto de variáveis ​​livres de é a união do conjunto de variáveis ​​livres de e o conjunto de variáveis ​​livres de .

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

Substituições evitando captura

Suponha que , e sejam termos lambda e e sejam variáveis. A notação indica substituição de para dentro em um -evitando captura maneira. Isso é definido para que:

  • ;
  • se ;
  • ;
  • ;
  • se e não está nas variáveis ​​livres de . A variável é considerada "fresca" para .

Por exemplo , e .

A condição de atualização (exigindo que não esteja 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, que é feita ignora a condição frescura: . Essa substituição transforma a função constante na identidade por substituição.

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

redução β

A regra de redução β estabelece que uma aplicação da forma se reduz ao prazo . A notação é usada para indicar que β-se reduz a . Por exemplo, para cada , . Isso demonstra que realmente é a identidade. Da mesma forma,, 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 esta 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 não pode 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 sem tipo é que ele não distingue entre diferentes tipos de dados. Por exemplo, pode ser desejável escrever uma função que opere apenas com números. No entanto, no cálculo lambda sem tipo, não há como evitar que uma função seja aplicada a valores 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 for 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 .

Notação

Para manter a notação de expressões lambda organizada, as seguintes convenções são geralmente 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 ).
  • O corpo de uma abstração se estende tanto à direita quanto possível : λ x . MN significa λ x . ( MN ) e não (λ x . M ) N .
  • Uma sequência de abstrações é contraída: λ xyz . N é abreviado como λ xyz . N .

Variáveis ​​livres e limitadas

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 consideradas limitadas . Em uma expressão λ x . H , a parte λ x é muitas vezes chamado ligante , como uma indicação de que a variável X é ficar ligado anexando λ x para M . Todas as outras variáveis ​​são chamadas de livres . Por exemplo, na expressão λ y . xxy , y é uma variável limitada 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 é limitada pelo segundo lambda: λ x . yx . 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, da seguinte forma:

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

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

Redução

O significado das expressões lambda é definido por como as expressões podem ser reduzidas.

Existem três tipos de redução:

  • α-conversão : alteração das variáveis ​​de limite;
  • β-redução : aplicação de funções aos seus argumentos;
  • η-redução : que capta uma noção de extensionalidade.

Também falamos das equivalências resultantes: duas expressões são α-equivalentes , se puderem 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 em expressar a substituição de N para X em M . A expressão à qual um redex se reduz é chamada de seu reduto ; o reduto de (λ x . M ) N é M [ x  : = N ].

Se x não for livre em M , λ x . H x é também um η-REDEX, com um reduct de M .

α-conversão

A conversão α, às vezes conhecida como renomeação α, permite que os nomes das variáveis ​​associadas sejam alterados. Por exemplo, conversão α de λ x . x pode render λ y . y . Termos que diferem apenas pela conversão α são chamados de equivalentes α . Freqüentemente, no uso do cálculo lambda, os termos α-equivalentes são considerados equivalentes.

As regras precisas para a conversão α não são completamente triviais. Primeiro, ao converter uma abstração em α, as únicas ocorrências de variáveis ​​que são renomeadas são aquelas que estão ligadas à mesma abstração. Por exemplo, uma conversão α de λ xx . x pode resultar em λ yx . x , mas poderia não resultar em λ yx . y . 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 , que não é o mesmo.

Em linguagens de programação com escopo estático, a conversão α pode ser usada para tornar a resolução de nomes mais simples, 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 de índice De Bruijn , quaisquer dois termos α-equivalentes são sintaticamente idênticos.

Substituição

Substituição, escrito H [ V  : = N ], é o processo de substituição de todos livres ocorrências da variável V na expressão M com expressão N . A substituição nos termos do cálculo lambda é definida pela 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 em α. Por exemplo, não é correto que (λ x . Y ) [ y  : = x ] resulte em λ x . x , porque o x substituído era para ser livre, mas acabou sendo limitado. 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 da aplicação da função. β-redução é definida em termos de substituição: a-β redução de (λ V . M ) N é H [ 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 sendo o mesmo que o 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 fornecem o mesmo resultado para todos os argumentos. A redução de η converte entre λ x . f x e f sempre que x não aparecer livre em f .

A redução-η pode ser vista 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 normaliza fortemente nem normaliza fracamente .

No entanto, pode ser mostrado que a redução β é confluente quando se trabalha para a conversão α (isto é, consideramos duas formas normais iguais se for possível converter uma α na outra).

Portanto, os termos de normalização forte e os termos de normalização fraca têm uma forma normal única. Para termos de normalização forte, qualquer estratégia de redução é garantida para produzir a forma normal, enquanto para termos de normalização fracamente, algumas estratégias de redução podem falhar em encontrá-lo.

Tipos de dados de codificação

O cálculo lambda básico pode ser usado para modelar booleanos, aritméticos , 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: = λ fx . f x
2: = λ fx . f ( f x )
3: = λ fx . f ( f ( f x ))

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

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

Um numeral de Igreja é uma função de ordem superior - ela recebe uma função f de argumento único e retorna outra função de argumento único. O numeral da 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. Isto é indicado f ( n ) e é de facto a n poder -ésimo de f (considerado como um operador); f (0) é definido para ser a função de identidade. Essas composições repetidas (de uma única função f ) obedecem às leis dos expoentes , razão pela qual esses números podem ser usados ​​para a 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 acima de 0. )

Uma maneira de pensar sobre o numeral da Igreja n , que muitas vezes é ú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 (vinculada) de n elementos todos iguais a x repetindo 'prefixar outro elemento x ' n vezes, começando de uma lista vazia. O termo lambda é

λ nx . n (PAR x ) NIL

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

Podemos definir uma função sucessora, que recebe um numeral de Igreja ne 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 ( n f x )

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 . m f ( n f x )

PLUS pode ser pensado como uma função que toma dois números naturais como argumentos e retorna um número natural; pode ser verificado que

MAIS 2 3

e

5

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

MAIS: = λ mn . m SUCC n 

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

MULT: = λ mnf . m ( n f )

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 então aplicá-la a zero. A exponenciação tem uma representação bastante simples em numerais de Igreja, a saber

POW: = λ be . e b

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 m - n quando m > n e 0 caso contrário.

Lógica e predicados

Por convenção, as duas definições a seguir (conhecidas como booleanos de Igreja) 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 (são apenas formulações possíveis; outras expressões são igualmente corretas):

AND: = λ pq . p q p
OR: = λ pq . p p q
NÃO: = λ p . p FALSE TRUE
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 VERDADEIRO se seu argumento for o numeral de Igreja 0 , e FALSO se seu argumento for qualquer outro numeral de Igreja:

ISZERO: = λ n . nx .FALSO) VERDADEIRO

O seguinte predicado 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 , é simples 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" no 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

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

Pares

Um par (2 tuplas) pode ser definido em termos de VERDADEIRO e FALSO , usando a codificação Church para pares . 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 FALSE
NIL: = λ x. VERDADEIRO
NULL: = λ p . pxy .FALSE)

Uma lista vinculada pode ser definida como NIL para a lista vazia ou o 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 um exemplo do uso de pares, a função shift-and-increment que mapeia ( m , n ) para ( n , n + 1) pode ser definida como

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

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

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

Técnicas de programação adicionais

Existe um corpo considerável de expressões idiomáticas de programação para cálculo lambda. Muitos deles foram desenvolvidos originalmente no contexto do uso do cálculo lambda como base para a semântica da linguagem de programação , usando efetivamente 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 podem ser usadas na programação prática, mas podem ser percebidas como obscuras ou estranhas.

Constantes nomeadas

No cálculo lambda, uma biblioteca tomaria a forma de uma coleção de funções previamente definidas, as quais, como termos lambda, são meramente constantes particulares. O cálculo lambda puro não tem um conceito de constantes nomeadas uma vez que todos os termos lambda atômicos são variáveis, mas pode-se emular ter constantes nomeadas colocando 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 costumam introduzir açúcar sintático , como let , para permitir a escrita acima na ordem mais intuitiva

deixe f = M em N

Encadeando tais definições, pode-se escrever um "programa" de cálculo lambda como zero ou mais definições de função, seguidas 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 é definido em M , uma vez 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 sintática mais avançada do letrec, que permite escrever definições de função recursiva naquele 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 recursividade ainda pode ser obtido dispondo para uma expressão lambda para receber em si o seu valor como argumento, por exemplo em  x . X x ) E .

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

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

Na expressão lambda que deve representar essa 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 - aplicá-la a um argumento - resultará em recursão. Assim, para atingir a recursão, o argumento pretendido como auto-referência (chamado de 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; caso contrário, n × ( r r ( n −1)))
com  r r x = F x = G r x  para manter, então  {{{1}}}  e
F: = GG = (λ x . X x ) G

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

Isso resolve, mas requer a reescrita de cada chamada recursiva como autoaplicação. Gostaríamos de ter uma solução genérica, sem a necessidade de qualquer reescrita:

G: = λ r . λ n . (1, se n = 0; caso contrário, n × ( r ( n −1)))
com  r x = F x = G r x  para manter, então  r = G r =: FIX G  e
F: = FIX G  onde  FIX g  : = ( r onde r = g r ) = g (FIX g )
de modo que  FIX G = G (FIX G) = (λ n . (1, se n = 0; do contrário n × ((FIX G) ( n −1))))

Dado um termo lambda com o primeiro argumento representando uma chamada recursiva (por exemplo, G aqui), o combinador de ponto fixo FIX retornará uma expressão lambda auto-replicante que representa 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 com antecedência, quando é criada, para ser feita cada vez que é chamada. Assim, a expressão lambda original (FIX G) é recriada dentro de si mesma, no ponto de chamada, alcançando a auto-referência .

Na verdade, 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 do qual estamos calculando o fatorial. Dado n = 4, por exemplo, isso dá:

( Y G) 4
G ( Y G) 4
rn . (1, se n = 0; caso contrário, n × ( r ( n −1)))) ( Y G) 4
n . (1, se n = 0; caso contrário, 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; caso contrário, n × (( Y G) ( n −1)))) (4−1))
4 × (1, se 3 = 0; caso contrário, 3 × (( Y G) (3−1)))
4 × (3 × (G ( Y G) (3−1)))
4 × (3 × ((λ n . (1, se n = 0; caso contrário, n × (( Y G) ( n −1)))) (3−1)))
4 × (3 × (1, se 2 = 0; caso contrário, 2 × (( Y G) (2−1))))
4 × (3 × (2 × (G ( Y G) (2−1))))
4 × (3 × (2 × ((λ n . (1, se n = 0; caso contrário n × (( Y G) ( n −1)))) (2−1))))
4 × (3 × (2 × (1, se 1 = 0; caso contrário, 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; caso contrário, 0 × (( Y G) (0−1))))))
4 × (3 × (2 × (1 × (1))))
24

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

Termos padrão

Certos termos têm nomes comumente aceitos:

I  : = λ x . x
K  : = λ xy . x
S  : = λ xyz . x z ( y z )
B  : = λ xyz . x ( y z )
C  : = λ xyz . x z y
W  : = λ xy . x y y
U  : = λ x . x x
ω  : = λ x . x x
Ω  : = ω ω
Y  : = λ g . (Λ x . G ( x x )) (λ x . G ( x x ))

Vários deles têm aplicações diretas na eliminação da abstração que transforma os termos lambda em termos de cálculo combinador .

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 anonimato, já que 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 por ter o combinador inicial I , K ou S agarrar o argumento P , assim como a redução β de x . N ) P faria. Eu retorno esse argumento. K lança o argumento de distância, assim como x . N ) faria se x não tem nenhuma ocorrência livre em N . S passa o argumento para ambos os subtermos da aplicação 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 ele possa ser usado em dois lugares. O combinador W faz apenas o último, produzindo o sistema B, C, K, W como uma alternativa ao cálculo combinador SKI .

Cálculo lambda digitado

Um cálculo lambda digitado é um formalismo digitado 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 atribuídos a termos lambda; a natureza exata de um tipo depende do cálculo considerado (consulte Tipos de cálculos lambda digitados ). De um certo ponto de vista, os cálculos lambda digitados podem ser vistos como refinamentos do cálculo lambda não digitado, mas de outro ponto de vista, eles também podem ser considerados a teoria mais fundamental e o cálculo lambda não digitado um caso especial com apenas um tipo.

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

Os cálculos lambda digitados estão intimamente relacionados à lógica matemática e à teoria da prova por meio do isomorfismo de Curry-Howard e podem ser considerados como a linguagem interna das classes de categorias , por exemplo, o cálculo lambda simplesmente digitado é 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 for, depende em grande parte da estratégia de redução usada. As estratégias comuns de redução do cálculo lambda incluem:

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 candidatura
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 de aplicação sempre tenta aplicar funções às formas normais, mesmo quando isso não é 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 foi reduzido a um valor (variável ou abstração). Apenas os redexes externos são reduzidos.
Chamada pelo nome
Como ordem normal, mas nenhuma redução é realizada dentro das abstrações. Por exemplo, λ x . (Λ x . X ) x está na forma normal de acordo com esta estratégia, embora contenha o redex x . X ) x .

Estratégias com compartilhamento reduzem cálculos que são "iguais" em paralelo:

Redução ótima
Como ordem normal, mas os cálculos que possuem o mesmo rótulo são reduzidos simultaneamente.
Ligue por necessidade
Como chamada pelo nome (portanto, fraca), mas os aplicativos de função que duplicariam os termos, em vez disso nomeiam o argumento, que é então reduzido apenas "quando for necessário".

Computabilidade

Não há algoritmo que tome como entrada quaisquer duas expressões lambda e produza TRUE ou FALSE dependendo se uma expressão se reduz à outra. 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 comprovada. Como de costume para tal prova, computável significa computável por qualquer modelo de computação que seja Turing completo . Na verdade, a computabilidade pode ser definida por meio do cálculo lambda: uma função F : NN de 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 números Church correspondente a x e y , 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 dada expressão lambda tem uma forma normal . Então ele assume que esse predicado é computável e, portanto, pode ser expresso em cálculo lambda. Com base no trabalho anterior 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, o resultado será uma contradição.

Complexidade

A noção de complexidade computacional para o cálculo lambda é um pouco complicada, porque o custo de uma redução β pode variar dependendo de como ela é implementada. Para ser mais 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 em um custo de tempo, ou deve-se manter o controle das localizações de variáveis ​​livres de alguma forma, implicando em um custo de espaço. Uma pesquisa ingénuos para os locais de V em E é S ( n ) no comprimento n de E . As sequências de diretor foram uma abordagem inicial que trocou esse custo de tempo por um uso de espaço quadrático. 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 etapas de redução β tomadas pela redução de ordem normal para reduzir um prazo é um modelo de custo de tempo razoável , ou seja, a redução pode ser simulada em uma máquina de Turing em um tempo polinomialmente proporcional ao número de etapas . 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 o que seria uma boa medida de complexidade do espaço.

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 β per se, mas sim ao manuseio da duplicação de redexes durante a redução β. Não se sabe se as implementações de redução ideal 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 mostrado para fragmentos do cálculo lambda que o algoritmo de redução ideal é eficiente e tem no máximo uma sobrecarga quadrática em comparação com o mais externo à esquerda. Além disso, a implementação do protótipo BOHM da redução ideal superou o Caml Light e o Haskell em termos de lambda puro.

Cálculo lambda e linguagens de programação

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

Funções anônimas

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

(lambda (x) (* x x))

O exemplo acima é uma expressão avaliada como 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 por meio do mecanismo de ponteiros de função . No entanto, os ponteiros de função não são uma condição suficiente para as funções serem 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 podem 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 # ("delegados") e C ++ 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 Futuros ao cálculo lambda. Outros cálculos de processo foram desenvolvidos para descrever a comunicação e a simultaneidade.

Semântica

O fato de que os termos do cálculo lambda atuam como funções em outros termos do cálculo lambda, e mesmo neles mesmos, levou a questões sobre a semântica do cálculo lambda. Poderia um significado lógico ser atribuído aos termos do cálculo lambda? A semântica natural era encontrar um conjunto D isomorfo ao espaço funcional 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 maior cardinalidade do que D , a menos que D seja um conjunto singleton .

Na década de 1970, Dana Scott mostrou que se apenas funções contínuas fossem consideradas, um conjunto ou domínio D com a propriedade necessária poderia ser encontrado, fornecendo assim um modelo para o cálculo lambda.

Este trabalho também formou a base para a semântica denotacional das linguagens de programação.

Variações e extensões

Essas extensões estão no cubo lambda :

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
  • SKI combinator calculus - 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

Referências

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, da variedade sem tipo ao lambda mais digitado cálculos , incluindo desenvolvimentos mais recentes, como sistemas de tipo puro e o cubo lambda . Não cobre extensões de subtipagem .
  • Pierce, Benjamin (2002), Types and Programming Languages , MIT Press, ISBN 0-262-16209-1abrange cálculos lambda de uma perspectiva de sistema de tipo prático; alguns tópicos como tipos dependentes são apenas mencionados, mas a subtipagem é um tópico importante.

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

links externos

  1. ^ Church, Alonzo (1941). O Cálculo da Conversão Lambda . Princeton: Princeton University Press . Página visitada em 2020-04-14 .
  2. ^ Frink Jr., Orrin (1944). "Revisão: 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 .