Como o combinador Y exemplifica "inconsistência no cálculo Lambda"?

Na página da Wikipedia para Combinadores de ponto fixo, está escrito o texto bastante misterioso

O combinador Y é um exemplo do que torna o cálculo Lambda inconsistente. Portanto, deve ser encarado com desconfiança. No entanto, é seguro considerar o combinador Y quando definido apenas na lógica matemática.

Eu entrei em algum tipo de romance de espionagem? O que no mundo significa as afirmações de que -calculus é "inconsistente" e que deve ser "considerado com suspeita" ? $\lambda$

lambda-calculus combinatory-logic Ben I.
fonte

FWIW, esse parágrafo está no artigo da Wikipedia desde janeiro de 2014, quando foi introduzido nesta reescrita maciça de quase todo o artigo .

Ilmari Karonen

Respostas:

É inspirado em eventos reais, mas a maneira como é declarada é quase irreconhecível e "deve ser encarada com desconfiança" não faz sentido.

A consistência tem um significado preciso na lógica: uma teoria consistente é aquela em que nem todas as afirmações podem ser provadas. Na lógica clássica, isto é equivalente à ausência de uma contradição, teoria ou seja, um é inconsistente se e somente se há uma declaraçãotal que a teoria prova ambose sua negação. $A$ $A$ $\neg A$

Então, o que isso significa em relação ao cálculo lambda? Nada. O cálculo lambda é um sistema de reescrita, não uma teoria lógica.

É possível visualizar o cálculo lambda em relação à lógica. Considere as variáveis como representando uma hipótese em uma prova, as abstrações lambda como provas sob uma determinada hipótese (representada pela variável) e a aplicação como reunindo uma prova condicional e uma prova da hipótese. Então a regra beta corresponde à simplificação de uma prova aplicando o modus ponens , um princípio fundamental da lógica.

Isso, no entanto, só funciona se a prova condicional for combinada com uma prova da hipótese correta. Se você tem uma prova condicional que assume e também tem uma prova de , não pode combiná-las. Se você deseja que essa interpretação do cálculo lambda funcione, é necessário adicionar uma restrição para que apenas as provas da hipótese adequada sejam aplicadas a provas condicionais. Isso é chamado de sistema de tipos e a restrição é a regra de digitação que diz que, quando você passa um argumento para uma função, o tipo do argumento deve corresponder ao tipo de parâmetro da função. $n=3$ $n=2$

A correspondência de Curry-Howard é um paralelo entre cálculos digitados e sistemas de prova.

tipos correspondem a declarações lógicas;
termos correspondem a provas;
tipos habitados (ou seja, tipos que exijam um termo desse tipo) correspondem a afirmações verdadeiras (ou seja, afirmações de que existe uma prova dessa afirmação);
a avaliação do programa (ou seja, regras como beta) corresponde a transformações de provas (que melhor transformavam as provas corretas em provas corretas).

Um cálculo digitado que possui um combinador de pontos fixos como permite construir um termo de qualquer tipo (tente avaliar ); portanto, se você interpretar a lógica através da correspondência de Curry-Howard, obterá uma teoria inconsistente. Consulte O combinador Y contradiz a correspondência de Curry-Howard? para mais detalhes. $Y$ $Y (\lambda x.x)$

Isso não é significativo para o cálculo lambda puro, ou seja, para o cálculo lambda sem tipos.

Em muitos cálculos digitados, é impossível definir um combinador de ponto fixo. Esses cálculos digitados são úteis em relação à sua interpretação lógica, mas não como base para uma linguagem de programação completa de Turing. Em alguns cálculos digitados, é possível definir um combinador de ponto fixo. Esses cálculos digitados são úteis como base para uma linguagem de programação completa de Turing, mas não com relação à sua interpretação lógica.

Em conclusão:

O cálculo lambda não é "inconsistente", esse conceito não se aplica.
Um cálculo lambda digitado que atribui um tipo a cada termo lambda é inconsistente. Alguns cálculos lambda digitados são assim, outros tornam alguns termos não tipáveis e são consistentes.
Os cálculos lambda digitados não são a única razão de ser para o cálculo lambda, e mesmo cálculos lambda digitados inconsistentes são ferramentas muito úteis - apenas para não provar as coisas.

Gilles 'SO- parar de ser mau'
fonte

Uau, há muito para descompactar aqui. Obrigado pela explicação detalhada. Vai levar algum tempo para tentar entender tudo.

Ben I.

Tecnicamente, a visualização não tipificada como un i digitado, você pode fazer uma correspondência CH entre o cálculo lambda não tipado e uma lógica. É apenas uma lógica muito, muito chata (e certamente inconsistente). Assistentes de prova como o NuPRL enlamear um pouco as águas. O idioma do objeto do NuPRL contém o cálculo lambda sem tipo e você pode definir facilmente o combinador Y. O NuPRL divide as coisas de maneira um pouco diferente, de modo que possui um sistema de refinamento de tipos em vez de um sistema de tipos, e o exercício não é produzir termos bem digitados, mas produzir derivações de digitação.

Derek Elkins

Sou apenas eu, ou é estranho impor o paradigma "proposições como tipos" no cálculo lambda não tipado? Eu sempre vi pessoas falarem sobre lógica no cálculo lambda sem tipo, introduzindo objetos específicos para serem os valores booleanos truee false, e proposições eram coisas que tinham saída com valor booleano. (e só foram consideradas proposições sobre o domínio das coisas onde ele faz a saída de um valor booleano).

Trivial (prova cada afirmação) e contém contradições são duas propriedades diferentes. Embora sejam equivalentes na lógica clássica, para lógicas paraconsistentes, um sistema pode ser inconsistente e não trivial.

Taemyr 30/10

"Inconsistente", para uma lógica baseada no cálculo λ, significa "atribui todo tipo a algum termo", não "atribui um tipo a todo termo" (embora o primeiro siga do último); existem muitas linguagens baseadas em λ-cálculo que correspondem a lógicas inconsistentes, mas onde nem todos os termos de λ-cálculo são tipificáveis.

Jonathan fundido

Eu gostaria de adicionar um ao que o @Giles disse.

A correspondência de Curry-Howard faz um paralelo entre os termos (mais especificamente, os tipos de termos ) e os sistemas de prova. $\lambda$ $\lambda$

Por exemplo, tem o tipo (onde significa "função de para "), que corresponde à instrução lógica . A função possui o tipo , correspondente a . Podemos converter qualquer tipo de cálculo lambda em uma tautologia lógica, de certa forma, "correspondência de padrões" em funções. $\lambda x.\lambda y.x$ $a \to (b \to a)$ $a \to b$ $a$ $b$ $a \implies (b \implies a)$ $\lambda x.\lambda y.xy$ $(a \to b) \to (a \to b)$ $(a \implies b) \implies (a \implies b)$

O problema surge quando consideramos o combinador Y, definido como . O problema surge porque esperamos que o combinador Y, como um combinador de "ponto de correção", tenha o tipo (porque leva uma função de um tipo para o mesmo tipo e encontra um ponto para essa função, que possui esse tipo). Converter isso em uma instrução lógica gera . Isso é uma contradição: $\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$ $(a \to a) \to a$ $(a \implies a) \implies a$

(a ⟹ a) ⟹ a ⊤ ⟹ a a (\neg a ⟹ \neg a) ⟹ (\neg a) ⊤ ⟹ \neg a \neg a

$(a \implies a) \implies a \\ \top \implies a \\ a \\(\neg a \implies \neg a) \implies (\neg a) \\ \top \implies \neg a \\ \neg a$

Aceitar em um sistema de tipos leva ao sistema de tipos que é inconsistente. Isso significa que podemos $(a \to a) \to a$

Não permitir tipos como em um sistema de tipos (isso fornece o -calculus Simply digitado ) ou $(a \to a) \to a$ $\lambda$
Viva com o sistema de tipos inconsistente como um sistema de dedução lógica.

Ortografia não contextual
fonte

O CH relaciona tipos a proposições, programas a provas e até reduções a transformações de provas. Não se trata apenas de tipos. Em seguida, apenas os tipos habitados correspondem a tautologias. é um tipo de cálculo lambda (polimórfico) mesmo que nenhum termo o habite. Supondo que você queira dizer tipos como , e aceitá- los perfeitamente, a questão é se esse tipo tem ou não um habitante. Por outro lado, podemos adicionar termos primitivos ao STLC que tornarão a lógica correspondente inconsistente sem estender o sistema de tipos.

\forall a, b . a \to b

$\forall a, b.a\to b$

\forall a . (a \to a) \to a

$\forall a.(a\to a) \to a$

Derek Elkins

@DerekElkins, que tipo de termos primitivos? Além disso, se eu entendi corretamente, isso é apenas para supor (a -> a) -> a é sempre habitado, o que produz a inconsistência? Portanto, não há mais inconsistência com uma linguagem de programação que requer uma prova de terminação? Ou existe outra fonte de inconsistência no cálculo lambda sem tipo ou com Hindley-Milner?

Hibou57 27/03

@ Hibou57 Termos primitivos, como constantes, como fix. Você pode apenas afirmar que não é uma constante para cada tipo . Isso já lhe dará um sistema inconsistente no que diz respeito ao CH, pois implicaria que todo tipo é habitado por . Além disso, você pode adicionar -rules para fazer calcular, e isso transformaria, digamos, o STLC com naturais em um sistema completo de Turing, mas você não precisa adicionar essas regras computacionais e o sistema ainda seria inconsistente.

{f i x}_{A}

$\mathsf{fix}_A$

A

$A$

f i x (λ x . x)

$\mathsf{fix}(\lambda x.x)$

δ

$\delta$

f i x

$\mathsf{fix}$

Derek Elkins