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

[Andreas Abel]

On 29.11.2013 20:40, Jason Gross wrote:
> Is there a computable/decidable/syntactic (and also complete)
> characterization of what's provable with J but not K?  (Alternatively,
> is there an algorithm for transforming proofs using K into proofs using
> only J whenever they exist?)

Not that I know of.  [Maybe there is one in one of the drawers of 
Conor's desk...]  I guess this is what Jesper Cockx and Pierre 
Boutillier are working on.

Cheers,
Andreas

> On Fri, Nov 29, 2013 at 2:01 PM, Altenkirch Thorsten
> <psztxa at exmail.nottingham.ac.uk <mailto:psztxa at exmail.nottingham.ac.uk>>
> wrote:
>
>     Shouldn't the semantics simply be that you can only prove things you can
>     prove using only J but not K?
>
>     Thorsten
>
>     On 29/11/2013 17:36, "Andreas Abel" <andreas.abel at ifi.lmu.de
>     <mailto: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 <mailto: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 <mailto:andreas.abel at ifi.lmu.de>
>      >http://www2.tcs.ifi.lmu.de/~abel/
>      >_______________________________________________
>      >Agda mailing list
>      >Agda at lists.chalmers.se <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>