<p>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:</p>

<ul>
<li><p>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.</p></li>
<li><p>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:</p>

<ul>
<li>Neil Ghani, <a href="https://personal.cis.strath.ac.uk/~ng/papers/tlca95.ps.gz"><em>Beta-Eta Equality for Coproducts</em></a>, TLCA 1995.</li>
<li>Vincent Balat, Roberto di Cosimo, Marcelo Fiore, <a href="http://dl.acm.org/citation.cfm?id=964001.964007"><em>Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums</em></a>, POPL 2004.</li>
<li>Sam Lindley, <a href="http://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf"><em>Extensional Rewriting with Sums</em></a>, TLCA 2007.</li>
<li>Arbob Ahmad, Daniel R. Licata, and Robert Harper, <a href="http://www.cis.upenn.edu/~sweirich/wmm/wmm07/programme/licata.pdf"><em>A Proof-Theoretic Decision Procedure for the Finitary Lambda-Calculus</em></a>. WMM 2007.</li>
</ul></li>
<li><p>The addition of unbounded types, such as natural numbers, makes the problem undecidable. Basically, you can now encode Hilbert's tenth problem.</p></li>
<li><p>The addition of recursion makes the problem undecidable, because having normal forms makes equality decidable, and that would let you solve the halting problem. </p></li>
</ul>

CC BY-SA 3.0
2017-07-12T13:09:31.083Z
[This paper](https://arxiv.org/pdf/1610.01213.pdf) 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.
Max New
CC BY-SA 4.0
2019-04-19T09:40:38.167Z
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?
glaebhoerl
CC BY-SA 4.0
2019-04-19T21:42:29.913Z
@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.
Neel Krishnaswami
CC BY-SA 3.0
2012-03-09T08:25:47.883Z
2012-03-09T08:33:50.293Z
2012-03-09T08:33:50.293Z
Neel Krishnaswami
<p>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.</p>

<p>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.</p>

<p>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.</p>

<computability><pl.programming-languages><functional-programming><function>
Programming languages with canonical functions
math4tots
# Programming languages with canonical functions

(Asked by: username_0 on 2012-03-09)

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.

**Tags:** computability, pl.programming-languages, functional-programming, function

---

## 1 answers

### Answer by username_1 on 2012-03-09. Score: 42 | Accepted answer

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:

  + Neil Ghani, [*Beta-Eta Equality for Coproducts*](https://personal.cis.strath.ac.uk/~ng/papers/tlca95.ps.gz), TLCA 1995.
  + Vincent Balat, Roberto di Cosimo, Marcelo Fiore, [*Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums*](http://dl.acm.org/citation.cfm?id=964001.964007), POPL 2004.
  + Sam Lindley, [*Extensional Rewriting with Sums*](http://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf), TLCA 2007.
  + Arbob Ahmad, Daniel R. Licata, and Robert Harper, [*A Proof-Theoretic Decision Procedure for the Finitary Lambda-Calculus*](http://www.cis.upenn.edu/~sweirich/wmm/wmm07/programme/licata.pdf). WMM 2007.
* 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.

> **Comments:**
> **username_2**: [This paper](https://arxiv.org/pdf/1610.01213.pdf) 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.  
> **username_3**: 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?  
> **username_1**: @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.  

---

