4
$\begingroup$

I have been learning MLTT and working on implementing its type checker referencing Coq's core language specification. Currently, I am at the stage of implementing its termination checker. I find it somewhat dissatisfying that I need to implement a separate termination checker in addition to the type checker.

I suspect the need for a separate termination checker arises from the presence of lambda abstractions, which allow for recursive definitions. This requires us to distinguish valid recursive definitions from invalid ones, and the implementation of a termination checker doesn't look that simple.

Is there a version of MLTT that is fully combinatorial and does not include lambda abstraction? In such a system, recursion schemas like induction over natural numbers would be primitives, eliminating the need for a separate termination checker. Are there any papers or implementations of such a system?

If no such system exists, I am curious to know why. One potential issue I can foresee is that a fully combinatorial language might be less convenient for dealing with recursive definitions without lambda abstraction. However, it seems feasible to support lambda abstraction in the surface language and then desugar and elaborate it into a fully combinatorial core language.

What other challenges might arise with this approach? Or would a combinatorial system without lambda abstraction inherently be weaker than one with it?

$\endgroup$
1
  • 1
    $\begingroup$ If we define judgemental equality by first interpreting the combinators into ordinary MLTT and then comparing maybe it's not that hard. The hard part is correctly listing all the equations purely in terms of combinators. Untyped SK calculus has some pretty wacky equations to make it equivalent to lambda calculus... the usual two are not remotely enough $\endgroup$
    – Trebor
    Commented Jun 14 at 5:07

1 Answer 1

5
$\begingroup$

You need a termination checker to translate recursive pattern-matching definitions into corresponding uses of eliminators (recursion/induction principles). This has nothing to do with $\lambda$-abstraction. You can implement MLTT without a termination checker by using eliminators instead of pattern matching. MLTT itself is defined in terms of eliminators, not pattern matching.

$\endgroup$
7
  • $\begingroup$ I was referencing the core languages of Coq and Agda. Is their core language different from MLTT? I supposed there can be some language-specific details in implementation but they follow the core mechanism. $\endgroup$
    – 12412316
    Commented Jun 13 at 15:33
  • 1
    $\begingroup$ Coq's core language is based on the calculus of inductive constructions and uses eliminators instead of termination checking. Agda does not have a core language, but if it did it would probably do something similar. You really don't want to muck about with termination checking in your core theory. $\endgroup$ Commented Jun 13 at 15:43
  • 1
    $\begingroup$ @NaïmFavier Coq doesn't use eliminators internally. The section of the manual you link, at the bottom, says that they are annoying to use and therefore Coq is defined differently. Coq instead has match ... with ... end and fix f args := ... as primitive expressions for destructing data and recursion, with the eliminators automatically emitted as definitions in terms of these constructs. E.g. you'll notice that the eliminators produced for mutual inductive types are strictly less powerful than match and fix. Checking guardedness of fix expressions is in the kernel. $\endgroup$
    – HTNW
    Commented Jun 14 at 2:29
  • 1
    $\begingroup$ @12412316 That fixes are guarded can probably be formulated as a side condition to their type-checking, so your question isn't strictly well-defined. Pedantry aside: yes, (fix f (n : nat) : False {struct n} := f (S n)) Z is well-typed-minus-guardedness and reduces forever. As to my other statement, feed Coq Inductive tree : Set := node (n : nat) (cs : forest) with forest : Set := nil | cons (t : tree) (ts : tree). Print tree_rect. The "eliminator" doesn't recurse! Coq's logic for generating eliminators in this case is deficient; it doesn't matter since eliminators are not fundamental. $\endgroup$
    – HTNW
    Commented Jun 14 at 3:34
  • 1
    $\begingroup$ Bit of rooting around shows that Coq actually straight up has a flag for disabling the termination checker (Unset Guard Checking.). Under that, Check ((fix f (n : nat) : False := f (S n)) O). succeeds and Eval compute in ((fix f (n : nat) : False := f (S n)) O). loops! $\endgroup$
    – HTNW
    Commented Jun 14 at 3:47

Your Answer

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

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