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

[Jason Gross]

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

-Jason


On Fri, Nov 29, 2013 at 2:01 PM, Altenkirch Thorsten <
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> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131129/16db1c20/attachment.html