[Agda] A different implementation of --without-K
jasongross9 at gmail.com
Fri Nov 29 20:40:57 CET 2013
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?)
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?
> 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>
> >>> 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.
> >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
> >Agda mailing list
> >Agda at lists.chalmers.se
> 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
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda