32
$\begingroup$

Are there any (functional?) programming languages where all functions have a canonical form? That is, any two functions that return the same values for all set of input is represented in the same way, e.g. if f(x) returned x + 1, and g(x) returned x + 2, then f(f(x)) and g(x) would generate indistinguishable executables when the program is compiled.

Perhaps more importantly, where/how might I find more information on canonical representation of programs (Googling "canonical representation programs" has been less than fruitful)? It seems like a natural question to ask, and I'm afraid that I just don't know the proper term for what I am looking for. I'm curious as to whether it is possible for such a language to be Turing complete, and if not, how expressive a programming language you can have, while still retaining such a property.

My background is rather limited, so I would prefer sources with fewer prerequisites, but references to more advanced sources may be cool too, as that way I'll know what I want to work towards.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
42
$\begingroup$

The extent to which this is possible is actually a major open question in the theory of the lambda calculus. Here's a quick summary of what's known:

  • The simply-typed lambda calculus with unit, products, and function space does have a simple canonical forms property. Two terms are equal if and only if they have the same beta-normal, eta-long form. Computing these normal forms is also quite straightforward.

  • The addition of sum types greatly complicates matters. The equality problem is still decidable (the keyword to search for is "coproduct equality"), but the known algorithms work for extremely tricky reasons and to my knowledge there is no totally satisfying normal form theorem. Here are the four approaches I know of:

  • The addition of unbounded types, such as natural numbers, makes the problem undecidable. Basically, you can now encode Hilbert's tenth problem.

  • The addition of recursion makes the problem undecidable, because having normal forms makes equality decidable, and that would let you solve the halting problem.

Improve this answer
$\endgroup$
3
  • $\begingroup$ This paper extends equivalence with coproducts to equivalence with sums but there is no "single" canonical form syntax, you pick a "saturation function" that is smart enough to detect when the two terms you're comparing have subterms that prove false. It is most similar to Ahmed-Licata-Harper in that they both use focusing. $\endgroup$
    – Max New
    Jul 12, 2017 at 13:09
  • $\begingroup$ With only unit, products, and functions, the cardinality of anything you can possibly write down is 1, whereas if you add sums, you suddenly get many different cardinalities (and can do "useful computation"). Are these facts related? $\endgroup$
    – glaebhoerl
    Apr 19, 2019 at 9:40
  • 1
    $\begingroup$ @glaebhoerl: I'm always reluctant to say facts are not related, but in this case I don't see an obvious connection. Most of the results I mentioned continue to hold if you add a base type $b$ to the language (without any intro- or elim-forms), but (a) that would break the cardinality fact you note, since $\lambda x:b. \lambda y:b.\; x$ and $\lambda x:b. \lambda y:b.\; y$ are different normal forms, but (b) doesn't affect any of the algorithms I know. $\endgroup$
    – Neel Krishnaswami
    Apr 19, 2019 at 21:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.