[opentheory-users] error loading article files (again?).

[Michael Norrish]

That’s a nice explanation; thanks.  

So here’s the next question: how should we best establish a name space for inter-operation between HOL Light and HOL4 that doesn’t use the OpenTheory library, and prefers instead to use sets as predicates?  Such a namespace would still have to figure out what to do with numerals, but hey.  

Michael


> On 3 Jul 2015, at 01:58, Joe Leslie-Hurd <joe at gilith.com> wrote:
> 
> Hi Michael,
> 
> I think your statement is correct, because both HOL Light and HOL4 use
> predicates rather than an explicit set type, so if OpenTheory also
> used predicates it would simplify translation between these two
> environments. And indeed, it complicates export if an explicit set
> type has to be reconstructed from predicates.
> 
> However, one design principle of OpenTheory is that whenever there is
> a trade-off between simplifying import or export then it's better to
> simplify importing, and in this case it's easy to drop the explicit
> set type in favour of predicates during import.
> 
> And there are other environments that do implement explicit set types,
> such as Haskell. When exporting theories as Haskell packages I want to
> export explicit sets as Haskell sets, which would be difficult if
> OpenTheory used predicates.
> 
> Cheers,
> 
> Joe
> 
> On Wed, Jul 1, 2015 at 10:38 PM, Michael Norrish
> <Michael.Norrish at nicta.com.au> wrote:
>> 
>>> On 2 Jul 2015, at 06:57, Joe Leslie-Hurd <joe at gilith.com> wrote:
>> 
>>> However, I can answer your question right now. I do want the
>>> OpenTheory fork of HOL Light to be as close as possible to the main
>>> trunk of HOL Light, but there are certain changes that are required to
>>> export a standard theory library (which is the primary purpose of this
>>> fork). For example, introducing an explicit set type (A set) rather
>>> than the predicate (A -> bool) and removing default cases (e.g., PRE 0
>>> = 0) are necessary to ensure the standard theory library can be used
>>> in as many environments as possible.
>> 
>> Is it not now our experience that providing an explicit set type actually makes it *harder* to use OpenTheory in both HOL4 and HOL Light?
>> 
>> Michael
>> 
>> ________________________________
>> 
>> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
>> 
>> _______________________________________________
>> 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