[Agda] Does the order of patterns matter?

[Martin Escardo]

Another question, related to the questions below.

Is there any guarantee (hoped or proved) that any recursive definition 
that the termination checker accepts, by pattern matching, can be 
compiled to Martin-Loef combinators (including K if you don't disable 
K), for a suitable fragment of Agda?

Martin

On 27/09/12 11:51, Martin Escardo wrote:
> Nils' message tells us where to find a full explanation of what is going
> on.
>
> On 27/09/12 11:27, Altenkirch Thorsten wrote:
>> The bug is rather that we use the = sign here -
>> Epigram avoided this by using |-> and it also kept track of the
>> splittings.
>
> But "|->" would also be wrong, because e.g. in Achim's example, there is
> a situation f lhs = rhs where there is no reduction f lhs |-> rhs. But
> this is just a notational discussion
>
>
> Here are some questions/conjectures.
>
> (1) It would be possible to implement Agda so that each equation in a
> pattern holds definitionally, if we wished, I believe. Of course, you
> would get new definitional equalities not present in Martin-Loef type
> theory. But does that matter? Conjecture: no new propositional
> equalities arise.
>
> (2) Every equation in a definition by pattern matching should hold
> propositionally (we know that this is not the case definitionally).
> This should be a meta-theorem.
>
> (3) Is there a nice characterization of pattern-matching definitions
> such that every "definining equation" does hold definitionally? The
> Berry-function in Nils' response indicates that this may be hard. Such
> pattern-system should be invariant under permuting equations, in
> suitable sense.
>
> (4) What is there against forcing defining equations to hold
> definitionally, other than being able to compile them to
> eliminator-trees? Already in definitions by pattern matching on natural
> numbers there is a departure from Martin-Lof type theory, because in
> MLTT you need an inductive definition to even compute the predecessor
> function. So why not go a bit further, provide (1) and (2) make sense?
>
> It is very disturbing that a proof ceases to type check if we reorder
> mutually exclusive, complete patterns.
>
> Such an extension should be conservative in the sense of allowing more
> proofs, but no new theorems. (Which the eta-rule doesn't satisfy, but
> nevertheless we seem to be happy to add.)
>
> Best,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda