# Termination and confluence -- which goes first?

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.
• Presumably you wouldn't reduce function bodies of recursive functions by reducing the recursive calls, would you? Dec 14, 2022 at 16:01
• 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 Dec 14, 2022 at 19:11
• 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. Dec 14, 2022 at 20:20
• @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 Dec 14, 2022 at 20:52
• gist.github.com/ice1000/78405bbf65c7a16f33731414dd3703e5 here's an example I came up with. Quite artificial but reduces as I described Dec 14, 2022 at 20:59