Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: Computing extensional equality

Nick Smith (Sep 28 2021 at 02:42):

Hi folks, I'm interested in the problem of computing whether two functions are extensionally equal. I don't know much type theory, so I'm trying to establish an intuition about the problem, and what is possible.

I know that the problem is undecidable for Turing-complete programming languages, but I'm not interested in those. I'm interested in suitably restricted languages. In particular, I'm interested in (purely functional) languages that include:

• first-class functions
• sum types and product types
• branching and pattern-matching
• integer arithmetic
  • Assume the standard integer operations are built-in, and that they obey all the standard laws of arithmetic.

But (perhaps unconventionally), I only want to consider languages without inductive/recursive types. (Integers are built-in, so they need not be treated as an inductive type.) I've recently been considering alternative approaches to structuring data wherein functions also fulfil the role of finite maps (a.k.a. dictionaries, associative arrays...), and I believe this can serve as an adequate alternative to inductive types for an everyday programming language. (Lookups would be statically-checked.)

As for recursive functions, they might exist in a very constrained form, or be banned entirely. (Is it reasonable to have this discussion without establishing what kind of recursion is permitted?)

So, back to our problem: determining extensional equality of functions. Thinking about this for a while, I've noticed there are actually several related problems:

• Computing a "canonical form" for a function
  • This one seems tricky: the process might need to include all kinds of elaborate manipulations, e.g. factorization and expansion of polynomial expressions.
• Computing a canonical "identifier" for a function (two functions share the identifier iff they are extensionally equal)
  • Perhaps this is an easier problem? The identifier need not contain all the information required to (efficiently) reconstruct the function definition itself.
• Testing two functions for extensional equality
  • This is an easier problem than the above problems, since equality testing is trivial if you have canonical forms/identifiers. But perhaps there are other methods to test equality that are more practical (and more decidable) than computing canonical forms/identifiers.

My questions include:

• How feasible is it to solve any of these problems in a suitably constrained language such as the one I described earlier?
• What is the most powerful language in which extensional equality is decidable? Has this been established?
• Are there some good resources for learning the basics of all this?

I've been utterly entranced by this problem lately. I've stumbled onto type-theoretic discussions about extensional equality such as the recent buzz around cubical type theory, but:

• The design of these type systems seems to be centered around inductive types, which I'm not very interested in. Perhaps all the relevant facts and motivations no longer apply in the absence of inductive types?
• From what I can tell, the idea seems to be that the programmer has to manually prove extensional equality of functions (by computing some kind of "path"). There's no built-in true/false test? That doesn't seem like the approach to equality you'd want in a general-purpose programming language.

James Wood (Sep 28 2021 at 12:44):

I guess you have to avoid being able to state all Diophantine equations, otherwise equality of open terms (i.e, polynomials) will be undecidable. Probably the most natural restriction is to linear integer arithmetic, but of course this may be a strong restriction.

Nick Smith (Sep 29 2021 at 01:51):

Let me see if I understand this problem. We can write a function $f: \Z^n \to \mathbb{B}$ that tests whether $p \in \Z^n$ is a solution to a Diophantine equation (returning a Boolean), and we can write a function $g: \Z^n \to \mathbb{B}$ that always returns false. An algorithm that told us whether $f = g$ for any such pair of functions (containing only integer addition, multiplication, and equality tests) would be solving an undecidable problem.

Is that right?

John Baez (Sep 29 2021 at 03:30):

Sounds right to me. By the way, we can take $n = 11$. That's the current smallest known value that works.

Mike Shulman (Sep 29 2021 at 03:38):

What's the largest known $n$ that doesn't work?

John Baez (Sep 29 2021 at 04:47):

It seems like most serious work has been done for natural number solutions of Diophantine equations, not integer solutions. Matiyasevich showed the best upper bound: there's no decision procedure for Diophantine equations in 9 natural number variables. Wikipedia says even 3 cannot now be excluded as a possible upper bound. I assume that means for natural numbers solutions there's a decision procedure for 2-variable Diophantine equations.

John Baez (Sep 29 2021 at 04:48):

The difficulty of settling Fermat's last theorem must have something to do with how problems kick in at n = 3.

Nick Smith (Sep 29 2021 at 08:01):

Ok, it seems I can throw extensional equality in the dustbin then. It seems utterly unrealistic even for "basic" functions :sweat_smile:.

The only way forward (apart from having no concept of function equality whatsoever) seems to be treating functions as pieces of syntax, and comparing them for syntactic equality. I think type theorists call this "definitional equality". I suppose that must suffice!

Mike Shulman (Sep 29 2021 at 08:08):

Yes, that's the reason why, as you said, a programmer or mathematician has to manually prove extensional equality of functions. The only kind of equality check for functions that we can expect a computer to do is intensional.

Nick Smith (Sep 29 2021 at 09:12):

Does the quick appearance of undecidability have something to do with (non-)continuity? If my language hypothetically had only rational arithmetic (no $\Z$ or $\N$ types, or any inductive type), can we have more expressive languages whilst retaining decidable equality?

Nick Smith (Sep 29 2021 at 09:13):

Or are there other simple counter-examples...

James Deikun (Sep 29 2021 at 11:10):

Having only real arithmetic would work, rational not so much. The theory of a real closed field is decidable. You can't have trigonometric functions though.

John Baez (Sep 29 2021 at 12:16):

That result about real closed fields is due to Tarski; it's good to read this to see what he did.

John Baez (Sep 29 2021 at 12:24):

It seems that while it's decidable, the best decision procedure is very slow. I don't know how slow! But if I had to wildly guess, I'd say double exponential time, something like $2^{2^{cn}}$. So this raises the question: is decidability useful if you have to wait billions of years to decide the equality of two functions?

James Deikun (Sep 29 2021 at 13:17):

The really bad slowdown is in quantifier alternation depth, making results like this quite practical for many purposes though...

Jacques Carette (Sep 29 2021 at 15:04):

If you stick to the world of arithmetic, indeed things go sideways quite quickly. But if you instead look at holonomic functions (functions that satisfy a linear ode with polynomial coefficients, which almost all special functions do), then things look bright again. See for example this paper from Joris van der Hoeven.

Nick Smith (Sep 30 2021 at 00:55):

I don't understand... how are holonomic functions not "sticking to the world of arithmetic"? It seems like they're still defined in terms of addition, multiplication, etc.

Nick Smith (Sep 30 2021 at 00:57):

Perhaps I'm missing the "big picture" of how holonomic functions are different to traditional functions.

Jacques Carette (Sep 30 2021 at 01:13):

They are 'different' because they are defined by a finite amount of data that has a very large amount of regularity properties, even though they are 'infinite' objects defined over continuous spaces. The resulting solutions are analytic with well-behaved, locatable singularities.

One thing to remember is that these are defined implicitly, as the solution of an LODE. So they really live in the world of analysis, not arithmetic.

Nick Smith (Sep 30 2021 at 01:40):

They do seem to be pretty exciting, from what I can comprehend. It's a shame that there is not a drop of introductory material about them. Every resource I can find assumes you are a mathematician. It's hard for me to discern whether they are a useful construct for more than just niche applications.

Nick Smith (Sep 30 2021 at 01:43):

From what I can tell, some operations on holonomic functions might also be computationally intractable...

Nick Smith (Sep 30 2021 at 01:46):

For example, it seems like you need to compute Gröbner bases, which is doubly exponential:

The complexity of Gröbner bases has been the object of extensive studies. It is well-known that in the worst-case, the complexity is doubly exponential in the number of variables.

Jacques Carette (Sep 30 2021 at 12:52):

Most operations on holonomic functions don't need Gröbner bases, in fact they can mostly be done via straightforward linear algebra. Furthermore, Gröbner bases are quite remarkable in that their running time is often nowhere near the worst case (we do know that in degenerate cases, Gröbner bases exactly correspond to Gaussian Elimination and to the Euclidean algorithm). The work on understanding when Gröbner bases are fast and when they are not is still ongoing, and appears to be extremely deep.

I find Bruno Salvy's talk that goes along with the paper Linear Differential Equations as a Data Structure to be a really good entry point. The audience were mathematically-oriented computer scientists.

Manuel Kauer's The Holonomic Toolkit is rather good, but was written for an audience of people who do Symbolic Computation. YMMV.

Nick Smith (Oct 01 2021 at 02:50):

Thank you for these references! I'll see if they help me :smile:. I am very much on board with treating equations as data structures. It's an approach I've been investigating for a while now...