Ramana,
On 16 Oct 2014, at 17:18, Ramana Kumar <[email protected]> wrote:
> Hi all,
>
> There has been an interesting discussion on the OpenTheory mailing list
> recently regarding how to simplify the two theorems produced by a type
> definition in HOL Light and remove their free variables. The latest message
> in the thread, which shows the suggestions by Mario Carneiro can be found
> here:
> http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html.
>
> I'm cross-posting to this list because I think using Mario's suggestions
> would be an improvement to both HOL Light and Opentheory. I hope the
> respective authors of those systems might agree and implement the changes,
> and that anyone else with an interest might voice their opinion.
>
It gets even better, because it finally offers the possibility of liberating
HOL Light and OpenTheory
from those dreary abstraction and representation constants. Let me quote my
latest post to the OpenTheory list:
> In fact, you [Mario] win today’s star prize, because [your] 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 [and Mario’s neat observation], (**) 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[Mario’s] 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 [Mario’s] desiderata for naming things:
> the names of rep and abs above are whatever the user chooses.)
Regards,
Rob.
------------------------------------------------------------------------------
Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
http://p.sf.net/sfu/Zoho
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
