Klop, van Oostrom e de Vrijer têm um artigo sobre o cálculo lambda com padrões.
http://www.sciencedirect.com/science/article/pii/S0304397508000571
Em certo sentido, um padrão é uma árvore de variáveis - embora eu esteja pensando nele como uma tupla aninhada de variáveis, por exemplo, ((x, y), z), (t, s)).
No artigo, eles mostraram que, se os padrões são lineares, no sentido de que nenhuma variável em um padrão é repetida, então a regra
(\p . m) n = m [n/p]
onde p é um padrão variável en é uma tupla de termos com a mesma forma exata de p, é confluente.
Estou curioso para saber se há desenvolvimentos semelhantes na literatura para o cálculo lambda com padrões e a regra eta adicional (expansão, redução ou apenas igualdade).
Em particular, por eta, quero dizer
m = \lambda p . m p
Mais diretamente, estou curioso para saber quais propriedades esse cálculo lambda teria. Por exemplo, é confluente?
Força a categoria de classificação a ser fechada porque força a propriedade que
m p = n p implies m = n
Usando a regra \ xi no meio. Mas talvez algo possa dar errado?
fonte
Respostas:
Esta não é uma resposta completa; é um comentário que ficou muito grande.
Se você estender o cálculo lambda digitado com produtos com eliminadores projetivos (ou seja, eliminadores de produtos
fst(e)
esnd(e)
), não haverá basicamente nenhum problema. A razão pela qual demorou tanto para descobrir isso é porque é mais natural fazer expansões eta do que reduções eta . Veja The Virtues of Eta Expansion, de Barry Jay .Se você deseja que os produtos tenham um eliminador de estilo padrão
Então as questões são mais complexas. A principal dificuldade com a correspondência de padrões são as conversões pendulares . Ou seja, esses cálculos têm a equação
e descobrir (a) qual contexto
C[-]
usar e (b) como orientar essa equação fica complicado. Na IMO, o estado da arte das abordagens no estilo de reescrita é a Extensional Rewriting with Sums, de Sam Lindley, e a Deciding Equivalence with Sums, de Gabriel Scherer, e o Empty Type , que consideram o cálculo lambda digitado com produtos e somas.fonte