[Agda] A different implementation of --without-K
abela at chalmers.se
Sat Nov 30 10:34:23 CET 2013
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.
> On Fri, Nov 29, 2013 at 2:01 PM, Altenkirch Thorsten
> <psztxa at exmail.nottingham.ac.uk <mailto:psztxa at exmail.nottingham.ac.uk>>
> 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
> <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>>
> >>> 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
> >>> 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 <mailto:andreas.abel at ifi.lmu.de>
> >Agda mailing list
> >Agda at lists.chalmers.se <mailto: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
> 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>
More information about the Agda