Calculus of Constructions: compress expression to its smallest form

Question

I'm aware that the Calculus of Constructions is strongly normalizing, meaning every expression has a normal for that cannot be beta,eta-reduced further. So in fact this is the most efficient expression that calculates the same value as the original expression.

But in certain cases, normalization may reduce a small expression to a huge expression (in terms of size).

Is there a smallest-form of expressions? A form that calculates the same value with the smallest size.

In other words, instead of a time-efficient normal-form, a space-efficient one.

Answer 1

There's a bit of freedom in what we considre "the same value". Let me show that there is no such algorithm if "the same value" means "observationally equivalent". I will use a fragment of the Calculus of constructions, namely Gödel's System T (simply typed $\lambda$-calculus, natural numbers, and primitive recursion on them), so the argument applies to a much weaker calculus already.

Given a number $n$, let $\overline{n}$ be the corresponding numeral representing it, i.e., $n$ applications of $\mathtt{succ}$ to $0$. Given a Turing mahcine $M$, let $\lceil M \rceil$ be the numeral encoding $M$ in some reasonable way.

Say that two closed terms $t, u : \mathtt{nat} \to \mathtt{nat}$ are equivalent, written $t \simeq u$, when for all $n \in \mathbb{N}$, $t \, \overline{n}$ and $s \, \overline{n}$ both normalize to the same numeral (they normalize to a numeral because we're in a strongly normalizing claculus).

Suppose we had an algorithm, which given any closed term of type $\mathtt{nat} \to \mathtt{nat}$ calculates a minimal equivalent term. Then we can solve the Halting oracle as follows.

There is a term $S : \mathtt{nat} \times \mathtt{nat} \to \mathtt{nat}$ such that, for all $n \in \mathbb{N}$ and all Turing machines $M$, $S (\lceil M \rceil, \overline{n})$ normalizes to $\overline{1}$ if $T$ halts within $n$ steps, and it normalizes to $\overline{0}$ otherwise. This is well known, since simulation of a Turing machine for a fixed number of steps $n$ is primitive recursive.

There are finitely many closed terms $Z_1, \ldots, Z_k$ which are minimal terms equivalent to $\lambda x : \mathtt{nat} .\, 0$. Our minimization algorithm returns one of them when we give it $\lambda x : \mathtt{nat} .\, 0$, and it may even be the case that $\lambda x : \mathtt{nat} .\, 0$ is in fact the only such minimal term. All this does not matter, the only thing that matters is that there are finitely many minimal terms that are equivalent to $\lambda x : \mathtt{nat} .\, 0$.

Now, given any machine $M$, consider the term $$u \mathbin{{:}{=}} \lambda x : \mathtt{nat} .\, S (\lceil M \rceil, x)$$ If $M$ runs forever then $u \overline{n}$ normalizes to $\overline{0}$ for every $n$ and is equivalent to $\lambda x : \mathtt{nat} .\, 0$. To decide whether $M$ runs forever, we feed $u$ into our minimzation algorithm and check whether the algorithm returned one of $Z_1, \ldots, Z_k$. If it did, then $M$ runs forever. If it did not, then it halts. (Note: the algorithm need not calculate the $Z_1, \ldots, Z_k$ by itself, these can be hard-coded into the algorithm.)

It would be nice to know an argument that works with a weaker notion of equivalence, for instance just $\beta$-reducibility.

Answer 2

As Andrej has said, the problem is undecidable if you allow replacing one term by another, extensionally equal one. However, you might be interested in optimal sharing of expressions, in the following sense: given the reduction $$(\lambda x:T.C\ x\ x)\ u\rightarrow_\beta C\ u\ u $$ it is clear that the occurrences of the term $u$ can be shared in memory, and every reduction applied to the one can be applied to the other.

In this sense, it is known how to reduce untyped terms in an optimal manner, reducing sharing as much as possible. This is explained here: https://stackoverflow.com/a/41737550/2059388 and the relevant citation is J. Lamping's An algorithm for optimal lambda calculus reduction. There is little doubt that the theorem for the untyped calculus can be extended to the CIC.

An other relevant question is the amount of type information that can be erased when performing type conversion, or indeed how to perform efficient conversion, which is an active field of research, see e.g. Mishra-Linger's thesis.

Answer 3

Let me insist on the viewpoint touched upon by cody's answer.

As far a see it, the question of finding a smallest $\lambda$-term equivalent to another $\lambda$-term is not really interesting, even if it there were an algorithm computing it. In fact, most programs you write in the $\lambda$-calculus (or whatever calculus of the $\lambda$-cube) are already in normal form, or at least head normal form, so they are already at their "smallest" in the sense you describe. Besides, being "small" doesn't mean being more efficient as discussed in this question.

So the issue you point out (that normalizing blows up the size) is a real problem only when you want to apply a function to an argument, and reduce to normal form to get the result. For instance, suppose you have a term $M$ computing a function $f$ on binary strings. Then you have $$M\,\overline{x}\to^{l(|x|)}\overline{f(x)}$$ where $l(|x|)$ is the number of reduction steps using leftmost-outermost reduction, which is guaranteed to find a normal form if it exists (in CoC, it always exists, but what I am saying applies to the untyped case as well). Now suppose, furthermore, that $l(n)=O(n^k)$ for some constant $k$. Can you conclude that $f$ is polynomial-time computable?

It is very easy to construct examples of $\lambda$-terms whose size increases exponentially with (leftmost-outermost) reduction, i.e., in $\Theta(n)$ steps you get a term of size $\Theta(2^n)$. This may make us seriously doubtful in regard to a positive answer to the above question: it seems that the $\lambda$-calculus is able to perform an exponential amount of work in linear time. In other words, it seems that the $\lambda$-calculus is not a reasonable model of computation in terms of complexity.

Although legitimate, the above doubt comes from a misguided assumption, namely that $\lambda$-terms are efficient representations of themselves. They are not! Less jokingly, $\lambda$-terms are very inefficient representations of the states that a machine executing them actually needs to go through.

It turns out that there is a syntax, called $\lambda$-calculus with linear explicit substitutions and introduced by Beniamino Accattoli, which is very good at representing the phenomenon of sharing alluded to in cody's answer. In particular, this syntax may be used to provide extremely faithful term representations of abstract machines of all sorts (see Beniamino's ICFP 2014 paper "Distilling Abstract Machines", of which I am co-author. I apologize for self-promotion but it seems relevant here).

This same syntax may be used to prove that, contrarily to the naive intuition, the answer to the above question is yes, indeed: the number of leftmost-outermost steps to normal form is a reasonable cost measure, even if the size explodes, because there is in fact another way of representing the same computation (using linear explicit substitutions) in which:

1. the size does not explode;
2. given two terms in the linear explicit substitution syntax, there is a polynomial-time algorithm that tests whether they represent the same $\lambda$-term, i.e., there is a clever way of comparing terms which does not need to "unfold" the sharing (just "unfolding" and then comparing would not work because the "unshared" term may be exponentially big).

This is all explained in Accattoli and Dal Lago's paper "Beta Reduction is Invariant, Indeed" (LICS 2014 and then I think there is a more recent journal version).

I think point 2 goes very much in the direction of your question about "space efficient" representations of $\lambda$-terms: the linear substitution calculus provides such representations, although they are not "normal" in any way, i.e., they are not the normal form of some rewriting procedure.