<p>At least the problem of whether 2 terms are equal modulo the theory of Cartesian Closed Categories (or $\beta\eta$ conversion) is decidable, because (in part) of the normalization property.</p>

<p>Another, more categorical way to see this is by extracting a conversion algorithm through <strong>normalization by evaluation</strong> which gives decision procedures for equality in categories which can naturally be embedded in the presheaf or sheaf category over sets.</p>

<p>See e.g. Altenkirch, Dybjer, Hoffmann &amp; Scott, <em>Normalization by Evaluation for Typed Lambda Calculus with Coproducts</em></p>

<p>for the version with products and coproducts (the version for just CCCs without coproducts can be found in the references).</p>

<p>An account which gives examples of implementations can be found <a href="https://www21.in.tum.de/~nipkow/pubs/tphols08.pdf" rel="noreferrer">here</a>.</p>

<p>Solving more complex questions than conversion, or solving conversion questions in the presence of datatypes like the natural numbers becomes undecidable rather quickly. I'm not aware of much work on algorithms for such systems, which I would be interested in as well. One could try simply encoding the equational theory into a first-order logic prover like <a href="http://www.vprover.org/" rel="noreferrer">Vampire</a>, but I don't know how well that would work. It would be an interesting experiment!</p>

CC BY-SA 3.0
2017-05-21T19:23:32.830Z
2017-05-21T19:23:32.830Z
cody
<p>I'd like to do automated inference, say solving word problems or reducing to normal form, in an equational theory of the typed lambda calculus (with product and unit types). Equivalently, in category-theoretic language: I'd like to do inference in a cartesian closed category presented by a finite set of generators and relations. I would be interested in any references on this topic.</p>

<p>I understand that inference in this setting is generally undecidable. However, I wonder whether there is any literature that either gives useful conditions under which exact inference is possible or proposes heuristic algorithms for approximate inference.</p>

CC BY-SA 3.0
2017-05-20T10:48:57.140Z
[The Seven Virtues of Simple Type Theory](http://imps.mcmaster.ca/doc/seven-virtues.pdf) by William M. Farmer is a very good introduction, if you haven't read it or something similar yet. The issue of undecidability is handled there by using "general models" (Henkin semantics) instead of "standard models". Section 6 "Provability" gives a proof system for SST (which has the same consistency strength as bounded Zermelo set theory aka Mac Lane set theory).
Thomas Klimpel
<reference-request><lambda-calculus><typed-lambda-calculus>
Inference in typed lambda calculus theories
Evan Patterson
# Inference in typed lambda calculus theories

(Asked by: username_0 on 2017-05-20)

I'd like to do automated inference, say solving word problems or reducing to normal form, in an equational theory of the typed lambda calculus (with product and unit types). Equivalently, in category-theoretic language: I'd like to do inference in a cartesian closed category presented by a finite set of generators and relations. I would be interested in any references on this topic.

I understand that inference in this setting is generally undecidable. However, I wonder whether there is any literature that either gives useful conditions under which exact inference is possible or proposes heuristic algorithms for approximate inference.

**Tags:** reference-request, lambda-calculus, typed-lambda-calculus
> **Comments:**
> **username_1**: [The Seven Virtues of Simple Type Theory](http://imps.mcmaster.ca/doc/seven-virtues.pdf) by William M. Farmer is a very good introduction, if you haven't read it or something similar yet. The issue of undecidability is handled there by using "general models" (Henkin semantics) instead of "standard models". Section 6 "Provability" gives a proof system for SST (which has the same consistency strength as bounded Zermelo set theory aka Mac Lane set theory).  

---

## 1 answers

### Answer by username_2 on 2017-05-21. Score: 4 | Accepted answer

At least the problem of whether 2 terms are equal modulo the theory of Cartesian Closed Categories (or $\beta\eta$ conversion) is decidable, because (in part) of the normalization property.

Another, more categorical way to see this is by extracting a conversion algorithm through **normalization by evaluation** which gives decision procedures for equality in categories which can naturally be embedded in the presheaf or sheaf category over sets.

See e.g. Altenkirch, Dybjer, Hoffmann & Scott, *Normalization by Evaluation for Typed Lambda Calculus with Coproducts*

for the version with products and coproducts (the version for just CCCs without coproducts can be found in the references).

An account which gives examples of implementations can be found [here](https://www21.in.tum.de/~nipkow/pubs/tphols08.pdf).

Solving more complex questions than conversion, or solving conversion questions in the presence of datatypes like the natural numbers becomes undecidable rather quickly. I'm not aware of much work on algorithms for such systems, which I would be interested in as well. One could try simply encoding the equational theory into a first-order logic prover like [Vampire](http://www.vprover.org/), but I don't know how well that would work. It would be an interesting experiment!


---

