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

[Joe Leslie-Hurd]

Hi Robert,

I'm afraid I may have been confusing. The OpenTheory standard library
has always had an explicit set type, and will continue to do so
(knowing what I know now, anyway). So you shouldn't need to change
anything.

Cheers,

Joe

On Thu, Jul 2, 2015 at 1:50 PM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> The HOL light fork and Holide? Or maybe I dont need to worry about it as
> long as you don't change the article files?
>
> On Jul 2, 2015 10:29 PM, "Joe Leslie-Hurd" <joe at gilith.com> wrote:
>>
>> 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