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

29

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.

math4tots
fonte

Respostas:

38

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:

  • 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.

Neel Krishnaswami
fonte
Este artigo estende a equivalência com coprodutos a equivalência com somas, mas não existe uma sintaxe de forma canônica "única", você escolhe uma "função de saturação" que é inteligente o suficiente para detectar quando os dois termos que você está comparando têm subtermos que se provam falsos. É mais parecido com Ahmed-Licata-Harper, pois ambos usam o foco.
Max New
Com apenas unidade, produtos e funções, a cardinalidade de qualquer coisa que você possa escrever é 1, enquanto que se você adicionar somas, de repente você obtém muitas cardinalidades diferentes (e pode fazer "cálculos úteis"). Esses fatos estão relacionados?
glaebhoerl 19/04
11
bλx:b.λy:b.xλx:b.λy:b.y