8
$\begingroup$

I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by:

  • the well-typedness of the clauses (type check)
  • the coverage of the patterns (coverage check)
  • the fact that recursive calls are structurally recursive (termination check)
  • the overlapping clauses are confluent (IApplyConfluence) -- see https://amelia.how/quick/boundaries-in-cubical-agda.html

My question: in what order does it make the best sense? Obviously type check should come first, but what about the others?

  • Since IApplyConfluence requires reduction of function bodies (for the conversion checks), we may potentially need to reduce the function being type-checked. If there is a non-termination problem, then we are in trouble (the type checker may loop). However, it makes me worried because how am I about to reduce a function that we do not yet know if it's well-defined?
  • Termination check is, in my impression, the last phase of the type checking, because there are techniques developed to do some clever reduction to make more definitions type-checked. It seems that we should definitely termination-check those who have no problem on reduction. However, if the clauses are not even confluent, we may reduce the wrong thing!
  • In case of mutually recursive functions, it's worse: the termination check of the two functions happens after both of their type checking, which means
    • if termination comes last, then both of their confluence check will happen when the other is neither known to be structurally recursive nor confluent.
    • if confluence comes last, then both of their termination check will happen when the other is neither known to be structurally recursive nor confluent.
Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Presumably you wouldn't reduce function bodies of recursive functions by reducing the recursive calls, would you? $\endgroup$
    – Andrej Bauer
    Commented Dec 14, 2022 at 16:01
  • $\begingroup$ Apart from the features mentioned in the question, I am also implementing Jesper Cockx's "overlapping and order-independent pattern matching" which requires reducing one more step in the bodies.... But you're probably right about the standard cases. I'll try to come up with a counterexample using only the features mentioned above. @AndrejBauer $\endgroup$
    – ice1000 ♦
    Commented Dec 14, 2022 at 19:11
  • $\begingroup$ Wht happens if a recursive definition $f = \Phi(f)$ is seen as $f = \mathsf{fix}\, \Phi$, whrere $\mathsf{fix}$ is a primitive fix-point operator? Then recursive calls are gone, and you could just proceed with normalizing $\Phi$ to your heart's content. $\endgroup$
    – Andrej Bauer
    Commented Dec 14, 2022 at 20:20
  • $\begingroup$ @AndrejBauer I believe pattern matching is much more general than fix. For example, pattern matching allows f (suc (suc x)) = g x for a function g while it's quite difficult to do with fix. But this is an interesting perspective $\endgroup$
    – ice1000 ♦
    Commented Dec 14, 2022 at 20:52
  • $\begingroup$ gist.github.com/ice1000/78405bbf65c7a16f33731414dd3703e5 here's an example I came up with. Quite artificial but reduces as I described $\endgroup$
    – ice1000 ♦
    Commented Dec 14, 2022 at 20:59

1 Answer 1

Reset to default
10
$\begingroup$

As you have noticed there is no "natural" way to prove confluence and termination: to prove confluence from local confluence you need termination, but proving termination often depends on typing, which becomes a lot more tricky without confluence.

In our paper on rewrite rules (The Taming of the Rew: a Type Theory with Computational Assumptions) we took one possible approach, which is to prove (global) confluence directly, i.e. without relying on termination. The basic idea is to rely on the triangle property of parallel reduction, which is a well-known trick that was first used to prove confluence of untyped lambda calculus. The main challenges here are (1) to define a proper notion of parallel reduction for your language and (2) to prove that the triangle property holds.

Alternatively, you can look into first proving termination without assuming well-typedness of your program, or at least without assuming that subject reduction holds. There are many possible directions to explore here. One example that bears mentioning is SizeChangeTool: A Termination Checker for Rewriting Dependent Types, which requires local confluence but not global confluence.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thank you very much! $\endgroup$
    – ice1000 ♦
    Commented Dec 21, 2022 at 19:34

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