[Agda] A different implementation of --without-K

[Bas Spitters]

We have a discussion on pattern matching without K in the book:

http://books.google.nl/books?id=LkDUKMv3yp0C&pg=PA163


On Sun, Dec 1, 2013 at 9:58 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

>
>
> On 29/11/13 19:01, Altenkirch Thorsten wrote:
>
>> Shouldn't the semantics simply be that you can only prove things you can
>> prove using only J but not K?
>>
>
> I like this specification. But is it complete?
>
> Let me propose a possible elaboration of this specification.
>
> In MLTT, you don't have pattern matching: everything has to be defined
> in terms of predefined combinators, which include J but not K.
>
> We can imagine pattern matching as syntax sugar for definitions with
> combinators.
>
> So an ideal Agda compiler would translate Agda into MLTT combinators
> (perhaps for MLTT with various extensions for inductive definitions).
>
> In this case, the correctness criterion is simply that Streicher's
> combinator K is not needed for this (ideal) translation.
>
> Actually, it would be very good if Agda did work like the idealized
> Agda discussed above, by compilation to combinators. This would allow
> for proof terms that can be exported to other proof assistants, for
> instance, e.g. for checking that an Agda proof is a proof, without
> having to rely on Agda to be sure.
>
> Best,
> Martin
>
>
>
>> Thorsten
>>
>> On 29/11/2013 17:36, "Andreas Abel" <andreas.abel at ifi.lmu.de> wrote:
>>
>>  On 29.11.2013 18:11, Harley D. Eades III wrote:
>>>
>>>> On Nov 29, 2013, at 5:00 AM, Nils Anders Danielsson <nad at cse.gu.se>
>>>> wrote:
>>>>
>>>>> On 2013-11-28 23:34, Andreas Abel wrote:
>>>>>
>>>>>> Yes, some of the fail test cases seem only to be there to document
>>>>>> what *is* rejected.  I do not know what purpose this serves, since I
>>>>>> would expect only stuff there that *must be* rejected.
>>>>>>
>>>>>
>>>>> The point is that the semantics of --without-K should not be changed by
>>>>> accident. These examples "must" be rejected until we make a conscious
>>>>> decision to change the semantics.
>>>>>
>>>>
>>>> Where is the semantics of --without-K formally written down?
>>>>
>>>
>>> There is not much written.  The documentation of the --without-K
>>> variants is in the respective release notes.
>>>
>>> Cheers,
>>> Andreas
>>>
>>>
>>> --
>>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>>
>>> Theoretical Computer Science, University of Munich
>>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>>
>>> andreas.abel at ifi.lmu.de
>>> http://www2.tcs.ifi.lmu.de/~abel/
>>> _______________________________________________
>>> 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.
>>
>>
>>
>>
>> _______________________________________________
>> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131202/c204d986/attachment.html