Sobre a correspondência da introdução à esquerda e eliminação da implicação no Cálculo Sequencial e na Dedução Natural resp.

8

Alguém poderia dar uma explicação intuitiva ( não intucionista) da correspondência da introdução à esquerda e eliminação da implicação no Cálculo Sequencial (SC) e Dedução Natural (ND), respectivamente? Eu sei que eles deveriam pela simetria de SC, mas não vejo como eles se correspondem. De maneira mais geral, não entendo como a introdução à esquerda de um conectivo no SC processa exatamente a eliminação dele no ND intuitivamente.

dia
fonte

Respostas:

9

Em termos computacionais, um termo de cálculo sequencial é uma sequencialização de um termo lambda. Ou seja, visto como um sistema de tipos, o cálculo sequencial pode ser visto como uma ordem de avaliação de um termo lambda.

Então, suponha que , e y- e 2 : A .Γe1:UMABΓe2:UMA

Na dedução natural, o prazo para a eliminação implicação é - isto é, aplicação. No entanto, observe que isso não nos diz se deve avaliar e 1 primeiro ou e 2 primeiro.Γe1e2:Be1e2

No cálculo sequencial, uma atribuição de termo de prova correspondente deve ser semelhante a

euetf=e1Euneuetv=e2Euneuetx=fvEunx

ou então deve parecer

euetv=e2Euneuetf=e1Euneuetx=fvEunx

Aqui, let-form é o termo de prova correspondente ao uso da regra de corte e, como todas as regras da esquerda atuam apenas em hipóteses / variáveis, isso nos obriga a vincular todos os resultados intermediários a variáveis. Esse requisito garante que somos forçados a dizer explicitamente qual ou e 2 reduzimos e ligamos primeiro a uma variável.e1e2

Para linguagens puramente funcionais, essa explicitação não importa, mas à medida que você adiciona efeitos, fica mais fácil trabalhar com cálculos sequenciais. É por isso que coisas como cálculo de efeitos de controle / lógica clássica geralmente são apresentadas como cálculo sequencial.

Neel Krishnaswami
fonte
Neel, obrigado também por esta interessante interpretação do ponto de vista da computação.
Dia
Neel, você pode dar trabalhos ou capítulos de livros onde é possível encontrar mais detalhes?
bellpeace
8

Apenas para recapitular: no ND, a eliminação de um conectivo nos diz como usá-lo:

- - - AUMAB
---
UMA

- - - BUMAB
---
B

são as regras de elim para conjunção. Eles dizem que nós podemos usar para obter A , ou para obter B .UMABUMAB

Da mesma forma, em SC:

- - - - - - Γ , A B ΔΓ,UMAΔ
------
Γ,UMABΔ

- - - - - - Γ , A B ΔΓ,BΔ
------
Γ,UMABΔ

O que as regras SC estão nos dizendo é que, se "necessidade" ou B , então podemos usar A B no lugar de A ou B .UMABUMABUMAB

Em geral, as regras de introdução à esquerda do SC nos dizem "quando" podemos usar um conectivo, e as regras de eliminação do ND nos dizem "como" usar um conectivo.

Agora, por implicação, no ND, temos:

A - - - - - - BUMAB       UMA
------
B

Em SC:

Σ , B Π - - - - - - - - - - Γ , Σ , A B ô , ΠΓUMA,Δ       Σ,BΠ
----------
Γ,Σ,UMABΔ,Π

Agora, a primeira coisa a fazer com a regra do SC é ignorar a "porcaria". e Σ podem ser ignorados para fins de intuição:ΔΣ

B ¸ - - - - - - - Γ , A B ¸ΓUMA       BΠ
-------
Γ,UMABΠ

O que isso diz é que, se soubermos usar o que "temos" ( ) para provar A , e soubermos usar B para provar o que queremos ( Π ) , poderemos usar A B para obter o que queremos. quer ( Π ). Ou seja, mais uma vez a regra de introdução à esquerda está nos dizendo "quando" podemos usar o conectivo.ΓUMAB(Π)UMABΠ

Mark Reitblatt
fonte
Boa resposta, mas a pergunta é sobre implicação, não conjunção.
Dave Clarke
@ Radu sim, mas isso faz com que eles saiam minúsculos. Eu acho que dessa maneira funciona bem o suficiente.
Re: Reitblatt