[opentheory-users] Troubleshooting an article reader

[Joe Leslie-Hurd]

Hi Mario,

Thanks for the suggestions: I've coloured the commands differently
according to whether they are new or changed:

http://www.gilith.com/research/opentheory/article.html#commands

Thus far defineTypeOp is the only changed command.

Instead of appending the version number to command names, the version command

http://www.gilith.com/research/opentheory/article.html#versionCommand

is used to globally specify the version of all commands in the file
(and allows for more significant future changes to the article format
than simply adding commands).

Cheers,

Joe


On Thu, Oct 16, 2014 at 2:50 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> Alternatively, if the command was named something else, like defineTypeOp6,
> then readers could be backwards-compatible without you having to select the
> article format (which I don't think is written anywhere in the file, so
> you'd have to supply this externally or else try to process and wait for an
> error before switching standards).
>
> On Thu, Oct 16, 2014 at 5:47 PM, Mario Carneiro <di.gama at gmail.com> wrote:
>>
>> By the way, would it be possible to highlight breaking changes differently
>> from non-breaking changes in v6? For example, a v5 reader will still work if
>> it implements hdTl, because any file using that will not be valid under the
>> spec so that code would just be dormant assuming the article file is valid.
>> Are there any other commands whose behavior is different other than
>> defineTypeOp?
>>
>> On Thu, Oct 16, 2014 at 4:43 PM, Rob Arthan <rda at lemma-one.com> wrote:
>>>
>>> Joe,
>>>
>>> I am certainly happy with the new way of formulating defineTypeOp.
>>>
>>> Regards,
>>>
>>> Rob.
>>>
>>> On 16 Oct 2014, at 19:06, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>> Hi Rob,
>>>
>>> That is a very nice idea for a new_type_specification that is
>>> compatible with the HOL Light and OpenTheory kernels: I like that it
>>> doesn't define new constants with the new type operator, which always
>>> seemed a bit inelegant to me.
>>>
>>> In the immediate term, I wonder if we can now agree that the benefits
>>> of Mario's new formulation of defineTypeOp are significant enough to
>>> change the OpenTheory article spec as follows?
>>>
>>>
>>> http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand
>>>
>>> I very much like the removal of hard-coded free variables (as opposed
>>> to providing additional arguments to specify their name), and the
>>> formulation simplifies the explanation of a future
>>> new_type_specification article command. As before, the cost is that
>>> readers have to implement both the old and new behaviors.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Thu, Oct 16, 2014 at 9:22 AM, Rob Arthan <rda at lemma-one.com> wrote:
>>>
>>> Mario,
>>>
>>> On 16 Oct 2014, at 08:36, Mario Carneiro <di.gama at gmail.com> wrote:
>>>
>>>
>>> \a. (abs (rep a)) = \a. a
>>>
>>> and similarly for the other:
>>>
>>> P = \r. ((rep (abs r)) = r
>>>
>>>
>>> In fact, you win today's star prize, because the above characterisations
>>> give a workable way of formulating using only the typed lambda calculus
>>> the type specification principle that is discussed in the HOL4
>>> documentation,
>>> but has never actually been implemented (despite having some really nice
>>> properties).
>>>
>>> As described in the HOL4 logic manual, the type specification principle
>>> would not be acceptable in the HOL Light or OpenTheory kernels because
>>> it depends on various non-primitive constants. The problem is to
>>> express using only the typed lambda-calculus something equiprovable with
>>> the following sequent, (*) say;
>>>
>>> Gamma |- (?f. TypeDefn P f) => Q
>>>
>>> where P and Q are closed terms satisfying certain conditions.
>>> From this (and another theorem that is easy to express without
>>> the logical connectives), you get a new type operator (alpha1, ...
>>> alphaN) op
>>> whose defining property is q[alpha1, ... alphaN) op/alpha].
>>> This generalises new_type_definition, which is the special case when
>>> Gamma is empty and Q is ?f.TypeDefn P f.
>>>
>>> Now ?f. TypeDefn p f is equivalent to ?abs.?rep. R P abs rep,
>>> where R P abs rep asserts that abs is left-inverse to rep and that
>>> rep is left-inverse to abs precisely where P holds (i.e., the properties
>>> that new_type_definition gives you of the abstraction and
>>> representation functions that HOL Light insists on defining for you).
>>> So (*) is equivalent to (**):
>>>
>>> Gamma |- (?abs.?rep. R P abs rep) => Q
>>>
>>> By first-order logic, (**) is equiprovable with:
>>>
>>> Gamma, P = (\r.rep(abs r) = r), (\a.abs(rep a)) = (\a.a) |- Q
>>>
>>> I had been fiddling around with various not very nice
>>> approximations to the above. With your improvements you get
>>> something that is relatively easy to understand and is
>>> simple enough to propose for serious consideration
>>> as a more general replacement for new_type_definition.
>>> (Note that it also satisfies you desiderata for naming things:
>>> the names of rep and abs above are whatever the user chooses.)
>>>
>>> Regards,
>>>
>>> Rob.
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>>
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>