[opentheory-users] Troubleshooting an article reader

[Joe Leslie-Hurd]

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
>