[Agda] Does the order of patterns matter?

[Altenkirch Thorsten]

On 27/09/2012 11:51, "Martin Escardo" <m.escardo at cs.bham.ac.uk> 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.

I believe we would obtain this if we had strong equality of coproducts.
However, this is very inefficient. Maybe there is a weaker theory which
has this property.

>
>(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.

Yes, I agree. 

In Agda pattern matching is primitive. An alternative would be to define
pattern matching by translating it into the use of eliminators. I'd prefer
the latter for a theoretical analysis.

>
>(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.

The Berry-function shouldn't be definable by pattern matching. In my view
pattern matching is a high level notation for case analysis, I.e. it
always corresponds to splits. The Berry function shows that there are
complete covers which are not obtained by splitting.

>(4) What is there against forcing defining equations to hold
>definitionally, other than being able to compile them to
>eliminator-trees?

To me the meaning of a pattern matching program is its translation into an
eliminator tree.

>It is very disturbing that a proof ceases to type check if we reorder
>mutually exclusive, complete patterns.

Why? This is only a consequence of the misreading of a pattern matching
program as a set of equations.

This is maybe only an issue for Mathematicians who pick up functional
programming. :-)

>
>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.)

Maybe this would be a nice property but the question is what is the price
to pay. I never ran into this issue but then I never think of pattern
matching clauses as equations.

Thorsten

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.