[Agda] Does the order of patterns matter?

[Altenkirch Thorsten]

Hi,

I was just about to compose an answer but forgot about this paper. A lot
of stuff is already in Conor's PhD, btw. And it is (partially ?)
implemented in OLEG and Epigram 1.

Indeed, it would be good if somebody could show that a program which
passes the syntactic conditions for --without-K can be translated into
combinators but K. I had some discussions with Pierre Boutellier in Paris
about this recently but I don't think there is a definitive answer.

Mutual inductive definitions and mutual recursion can be easily
incorporated as syntactic sugar due to the power of dependent types. Still
somebody should spell out the details.

However, there are many features of Agda which are not covered:
- coinductive definitions and in particular mixed inductive-coinductive
definitions
- so called induction-induction which means you mutually define inductive
types one depending on the other.
- induction-recursion, I.e. defining an inductive type mutually with a
recursive definition. This covers the
  definition of universes.

In these cases we don't even have an accepted set of combinators.

Thorsten


On 27/09/2012 17:07, "Dan Doel" <dan.doel at gmail.com> wrote:

>Yes, see Eliminating Dependent Pattern Matching:
>
>  
>http://www.cs.st-andrews.ac.uk/~james/RESEARCH/pattern-elimination-final.p
>df
>
>The --without-K part is more dicey; I don't think anyone's proved that
>bit (i.e. that it doesn't require/imply K).
>
>On Thu, Sep 27, 2012 at 11:48 AM, Martin Escardo
><m.escardo at cs.bham.ac.uk> wrote:
>> 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
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda

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.