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

[Joe Leslie-Hurd]

Hi Michael,

It seems to me for your use-case that the simplest thing might be to
choose one of HOL4 and HOL Light as the master namespace, and then
convert all names from the other system into it.

Alternatively, you could come up with a new standard namespace and
convert everything into it. This is the OpenTheory approach, and you
can see the resulting mapping for the HOL Light standard theory
library in

https://github.com/gilith/hol-light/blob/master/opentheory/stdlib/stdlib.int

Cheers,

Joe

On Mon, Jul 6, 2015 at 10:51 PM, Michael Norrish
<Michael.Norrish at nicta.com.au> wrote:
> 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
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list