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

[Joe Leslie-Hurd]

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