Caracterizando equivalências invisíveis por regras de reescrita confluentes

14

Em resposta a outra pergunta, Extensões da teoria beta do cálculo lambda , Evgenij ofereceu a resposta:

beta + a regra {s = t | s e termos fechados insolúveis}

onde um termo M é solucionável se podemos encontrar uma seqüência de termos tais que M aplicação 's para eles é igual a eu .

A resposta de Evgenij fornece uma teoria equacional sobre o cálculo lambda, mas não uma caracterizada por um sistema de redução, isto é, um conjunto recursivo e confluente de regras de reescrita.

Vamos chamar uma equivalência invisível sobre uma teoria do cálculo lambda, um sistema de redução que equaciona um conjunto não trivial de termos lambda fechados e insolúveis, mas não adiciona nenhuma nova equação envolvendo termos solucionáveis.

Existem equivalências invisíveis sobre a teoria beta do cálculo lambda?

Postscript Um exemplo que caracteriza uma equivalência invisível, mas não é confluente. Seja M = (λx.xx) e N = (λx.xxx) , dois termos insolúveis. A adição da regra de reescrita NN ao MM induz uma equivalência invisível contendo MM = NN , mas possui o par crítico ruim em que NN se reduz a MM e MMN , cada um com uma reescrita disponível, que é reescrita para si mesma.

pl.programming-languages lambda-calculus lo.logic Charles Stewart
fonte
A noção de equivalência invisível está relacionada à noção de extensão conservadora . Uma extensão conservadora de uma teoria é uma coleção de termos e equações adicionais à teoria que não adicionam novas equações entre os termos na teoria original.
Dave Clarke
@supercooldave: termos insolúveis são termos normais da teoria, como (λx.xx) (λx.xx) , e são redutíveis a outros termos (insolúveis), portanto fazem parte da teoria normal do cálculo lambda. O ponto é que eles são ortogonais à semântica do cálculo lambda que obtemos do teorema de Böhm.
Charles Stewart
Então, você está procurando por além de algumas regras do mesmo tipo que a regra beta (especificada pela sintaxe em vez de pela semântica) tais que <resto do post>? λβ
Evgenij Thorstensen
@ Evgenij: Sim. É crucial que as novas regras sejam confluentes e, é claro, trivial para encontrar exemplos, se não forem. Vou adicionar um exemplo para mostrar o problema.
Charles Stewart

Respostas:

6

Sim. Com M = (λx.xx) de acordo com a pergunta, considere a reescrita ζ que leva MM p para MM .

É confluente e, portanto, caracteriza um sistema de redução sobre o cálculo lambda. Esboço de argumento para confluência: como MM está fechado, precisamos considerar apenas pares críticos do formato MMN 1 ... N k . Estes podem ser resolvidos.

É uma equivalência invisível, porque termos da forma MMI ... I (com zero ou mais eu s) são fechados termos insolúveis que reduzem apenas para si mesmos no cálculo de base lambda, assim, são distintos, e de modo que o conjunto infinito delas termos não é trivial e é obviamente igualado por ζ.

Não gosto de aceitar minha resposta à minha pergunta, então aceitarei uma resposta de alguém que forneça um argumento de confluência menos absurdamente incompleto.

Charles Stewart
fonte