Existem teorias eta intermediárias para o cálculo lambda?

Existem duas teorias estudadas principais do cálculo lambda, a teoria beta e sua extensão pós-completa, a teoria beta-eta.

Essas duas teorias têm um meio termo, uma regra eta intermediária que fornece uma teoria de reescrita confluente? Existe alguma noção interessante de extensionalidade parcial a que corresponde?

Esta é a segunda pergunta que eu fiz na busca do eta intermediário, sendo as Extensões da teoria beta do cálculo lambda , que levaram a questionar sobre uma noção ortogonal de extensão. Caracterizando equivalências invisíveis por regras de reescrita confluentes , que procuravam responda a essa pergunta anterior.

Para cálculos digitados, se você considerar os tipos negativos ( , × , → ), poderá ativar ou desativar as regras eta basicamente à vontade, sem afetar a confluência.$1$$\times$$\to$

Para tipos positivos (somas e pares com a eliminação da correspondência de padrões), a situação é muito mais confusa. Basicamente, a questão é se o termo possui uma forma de eliminação em escopo fechado, que permite que os contextos interajam de maneiras complicadas com as eta-expansões. Por exemplo, se tem o tipo A × B , sua eta-expansão é l e $e$$A \times B$ . Mas, para obter a teoria equational um teórico categoria seria de esperar, é preciso considerar contextos C [ - ] , e generalizar a equação a ser C [ e ] ≡ l e $\mathsf{let}\;(a,b) = e \;\mathsf{in}\; (a,b)$$\mathbb{C}[-]$ (com as restrições de escopo esperadas).$\mathbb{C}[e] \equiv \mathsf{let}\;(a,b) = e\;\mathsf{in}\;\mathbb{C}[(a,b)]$

Acho que você ainda pode provar um resultado de confluência se não permitir as conversões pendulares. Mas isso é boato - nunca tentei eu mesmo, nem vi documentos documentando.

Eu realmente não sei nada sobre cálculo lambda sem tipo, no entanto.

EDIT: Charles pergunta sobre eta-reduções. Isso é promissor para o tipo de exemplo que ele procura, porque acho que em geral eles não serão fortes o suficiente para modelar a teoria da igualdade completa, que ilustrarei com um exemplo simples envolvendo booleanos. A eta-expansão para booleanos é . (A eta-redução é, obviamente, a outra direção.)$\mathbb{C}[e] \mapsto \mathsf{if}(e, \mathbb{C}[\mathsf{true}], \mathbb{C}[\mathsf{false}])$

Agora, considere o termo . Mostrando que esse termo é equivalente a i f ( e , $\mathsf{if}(e, f, g)\;\mathsf{if}(e, x, y)$ tem de passar por uma eta-expansão, porque temos de substituir o e em uma do-se, em seguida,-tinha o com t r u e e f um l s e , a fim de conduzir uma β -redução. $\mathsf{if}(e, f\;x, g\;y)$$e$$\mathsf{true}$$\mathsf{false}$$\beta$

De acordo com John C. Mitchell, em Foundations of Programming Languages, tanto no STLC quanto no cálculo lambda não tipado, a regra de redução pair (proj₁ P, proj₂ P) → Pquebra a confluência quando combinada com a fixredução (ou, presumo, olhando a prova), sem essas condições para o caso não tipado. Esse é o teorema 4.4.19 (página 272).