[opentheory-users] Troubleshooting an article reader

[Rob Arthan]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141016/7c76b100/attachment-0001.html>