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

[Joe Leslie-Hurd]

Hi Robert,

That depends - into which system are you planning on importing
OpenTheory theories?

Cheers,

Joe

On Thu, Jul 2, 2015 at 9:39 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Oh no. So does that mean the import function would have to be updated then.
>
> On Jul 2, 2015 5:58 PM, "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