Linguagens de programação com funções canônicas

Existem linguagens de programação (funcionais?) Nas quais todas as funções têm uma forma canônica? Ou seja, quaisquer duas funções que retornam os mesmos valores para todo o conjunto de entradas são representadas da mesma maneira, por exemplo, se f (x) retornou x + 1 eg (x) retornou x + 2, então f (f (x )) eg (x) gerariam executáveis ​​indistinguíveis quando o programa for compilado.

Talvez o mais importante seja, onde / como posso encontrar mais informações sobre representação canônica de programas (pesquisar no Google "programas de representação canônica" tem sido menos proveitoso)? Parece uma pergunta natural, e tenho medo de não saber o termo adequado para o que estou procurando. Estou curioso para saber se é possível que essa linguagem seja Turing completa e, se não for, quão expressiva você pode ter uma linguagem de programação, mantendo a propriedade.

Como meu histórico é bastante limitado, prefiro fontes com menos pré-requisitos, mas as referências a fontes mais avançadas também podem ser interessantes, pois assim saberei no que quero trabalhar.

A extensão em que isso é possível é realmente uma grande questão em aberto na teoria do cálculo lambda. Aqui está um rápido resumo do que é conhecido:

• O cálculo lambda de tipo simples com unidade, produtos e espaço de função possui uma propriedade simples de formulários canônicos. Dois termos são iguais se, e somente se, tiverem a mesma forma beta-normal e eta-longa. Computar essas formas normais também é bastante direto.

• A adição de tipos de soma complica bastante as coisas. O problema da igualdade ainda é decidível (a palavra-chave a ser pesquisada é "igualdade de coprodutos"), mas os algoritmos conhecidos funcionam por razões extremamente complicadas e, pelo que sei, não existe um teorema da forma normal totalmente satisfatório. Aqui estão as quatro abordagens que eu conheço:

  • Neil Ghani, Igualdade Beta-Eta para Coprodutos, TLCA 1995.
  • Vincent Balat, Roberto di Cosimo, Marcelo Fiore, Normalização extensional e avaliação parcial direcionada por tipo para cálculo lambda digitado com somas , POPL 2004.
  • Sam Lindley, Reescrita Extensional com Soma , TLCA 2007.
  • Arbob Ahmad, Daniel R. Licata e Robert Harper, um procedimento de decisão de prova teórica para o cálculo lambda finitário . WMM 2007.

• A adição de tipos ilimitados, como números naturais, torna o problema indecidível. Basicamente, agora você pode codificar o décimo problema de Hilbert.

• A adição de recursão torna o problema indecidível, porque ter formas normais torna a igualdade decidível e isso permitiria que você resolvesse o problema de parada.