I'd say one of the stronger ways to get "undefined" is to add an element to
your type representing undefinedness, e.g., make it (/) : real option ->
real option -> real option, where NONE represents "undefined". But then you
will have a lot of bookkeeping to deal with...
I don't suggest this
Well, as the purpose of optionTheory is to augment any type with one more
value, for (at least) extreals, it would be equivalent to have that “undefined”
thing defined as part of the datatype definition:
val extreal_def = Datatype
`extreal = NegInf | PosInf | Normal real | Undefined`;
> So I think the key is to make sure that “undefined” thing really
undefined, such that whenever it appears, the proof cannot proceed any more
I think this is exactly what is impossible to do in HOL: it is a logic of
total functions.
On Wed, 20 Feb 2019 at 15:26, Chun Tian (binghe)
wrote:
>
Very nice paper. Thanks Umair and Freek for the correction and link.
On Wed, 20 Feb 2019 21:08 Umair Siddique
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101=rep1=pdf
>
> http://www.gilith.com/talks/tphols2001-subtypes.pdf
>
>
> - Umair
>
> On Wed, Feb 20, 2019 at 4:02 PM
*We apologize if you received this email several times. To be removed from our
mailing list, please respond to this message with UNSUBSCRIBE in the subject
line.*
WORDS 2019
12th International Conference
Loughborough, September 9–13, 2019
Thanks for the paper links.
Actually I was long wondering what was under HOL’s "examples/miller/subtypes/“
folder, now I realized it’s the implementation of the idea in this paper.
There’re some example code at the end of subtypeTools.sml in that folder:
tt prove
(``~3 IN nzreal``,
Rather than subtyping, I believe the approach in HOL Light is to use the finite
cartesian products framework to write things analogous to
!x : real[‘a] y : real [‘b]. …
The same sort of thing is possible in HOL if you inherit from fcpTheory.
The HOL4 uses of fcp have been very focused on the
[Apologies if you receive multiple copies of this email. Please distribute to
any and all interested parties.]
Deadlines extended!
Register your papers by February 26, and submit them by March 25.
---
Apologies for cross-posting
ICLP 2019 Sister Conferences and Journal Presentation Track - Call for Papers
The program committee of the 35th International Conference on Logic Programming
(ICLP) invites submissions of published journal papers and papers presented at
related conferences for the
Apologies for cross-posting
** CALL FOR PAPERS **
The 35th International Conference on Logic Programming (ICLP 2019)
Applications Track
September 21-25, 2019
Las Cruces, New Mexico (USA)
https://www.cs.nmsu.edu/ALP/iclp2019/
Apologies for the small typo I forwarded to Gregory (and the additional
email). The submission is by March 05.
All the best,
Mario
Il giorno gio 14 feb 2019, 04:39 Gregory Gelfond ha
scritto:
> [Apologies if you receive multiple copies of this email. Please distribute
> to
> any and all
The 27th International Conference on Automated Deduction (CADE-27)
Natal, Brazil
25-30 August 2019
http://www.cade-27.info
CALL FOR PAPERS
CADE is the major international forum for presenting research on all aspects
of automated deduction. High-quality submissions on the general topic of
[ Apologize for Multiple Copies ]
***
iFM 2019 - Call for Workshops and Tutorials
15th International Conference on integrated Formal Methods (iFM)
2-6 December 2019
Bergen, Norway
Web:
13 matches
Mail list logo
