Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Chris, My apologies for carrying on about this, but I care for this subject, sorry. >At some phases of the moon this sounds attractive to me too. For me too :-) The main problem is that you will get lots of extra proof obligations, so it's _not_ "efficient". You can _hope_ that the automatio

Re: [Hol-info] Undefined operations such as division by zero in HOL

On Wed, Apr 10, 2013 at 3:04 AM, Freek Wiedijk wrote: > Hi Mike, > > >Taking definedness to the level Freek is discussing would, > >I think, not let you prove that > > > > x DIV 0 = x DIV 0 > > Exactly. I think that what I want is much closer to PVS and > B than to IMPS. I also don't want any

Re: [Hol-info] Undefined operations such as division by zero in HOL

Difficult questions. Regarding any term with an undefined subterm as undefined is simplest - then you can have theorems like (A DIV B) TIMES B = A without side conditions. Problem is, though, you want to be able to write "if A NOT EQ [] THEN HD A ..." which can have an undefined subterm (HD A).

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Rob, >Given a Z specification it could generate a set of proof >obligations called domain conditions. The idea was that >if the domain conditions were true, then the specification >was insensitive to the interpretation of undefined terms. This is exactly what I was trying to describe, and the

Re: [Hol-info] Undefined operations such as division by zero in HOL

On 10 Apr 2013, at 11:04, Freek Wiedijk wrote: >> > What I just want is to have some story + infrastructure > that allows me to -- at the very very end -- prove that > the result that I have established is "meaningful", in the > sense that it doesn't depend on/refer to what functions do > outside

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Mike, >Taking definedness to the level Freek is discussing would, >I think, not let you prove that > > x DIV 0 = x DIV 0 Exactly. I think that what I want is much closer to PVS and B than to IMPS. I also don't want any change to the logic. I _hate_ partial logics. I want to be able to use

Re: [Hol-info] Undefined operations such as division by zero in HOL

On 09/04/13 14:40, Albert Y. C. Lai wrote: > This can be written in Haskell as: >do { > q0 <- x/y; > q1 <- b/c; > return (q0 + q1) >} If you have defined / to return options as Albert suggests, the above can be mimicked with HOL4's support for monad syntax. You'd need to

Re: [Hol-info] Undefined operations such as division by zero in HOL

On 10/04/13 05:46, Cris Perdue wrote: > I think this systematizes the approach that leads to using x != 0 ==> recip x > * > x = 1 as a specification for reciprocal, or Konrad's example with DIV and MOD. > Hopefully I am not missing something here. Taking definedness to the level Freek is discuss

Re: [Hol-info] Undefined operations such as division by zero in HOL

On Tue, Apr 9, 2013 at 2:22 AM, Freek Wiedijk wrote: > Hi Chris, > > Thanks for bringing up this topic, which is very > interesting question to me. It's question III in my talk > . I'm replying > here because there is an approach that I've been wanting

Re: [Hol-info] Undefined operations such as division by zero in HOL

On 13-04-05 01:50 AM, Cris Perdue wrote: > Thanks for your input on this. Are there some examples in HOL or HOL > Light where the approach you suggest with option types is used? [...] > On Thu, Apr 4, 2013 at 4:28 PM, Vincent Aravantinos > mailto:vincent.aravanti...@gmail.com>> > wrote: > > In

Re: [Hol-info] Undefined operations such as division by zero in HOL

Hi Chris, Thanks for bringing up this topic, which is very interesting question to me. It's question III in my talk . I'm replying here because there is an approach that I've been wanting to develop for a while now (but haven't really started work on).

Re: [Hol-info] Undefined operations such as division by zero in HOL

Chris, I was just considering this conceptually, but I think this is not reasonable to use in your context: this will really introduce some burden in the syntax (unless maybe the system we use has a particularly good syntactic sugar for monads, which, I believe, is not the case of HOL(Light))

Re: [Hol-info] Undefined operations such as division by zero in HOL

> I presume that the same sort of thing could be done with reciprocal of zero, and the definition without > the side condition was chosen as being easier to work with. Yes, I think I remember John Harrison discussing the issue in his thesis and concluding that working with an unconditional rewrite

Re: [Hol-info] Undefined operations such as division by zero in HOL

Vincent, Thanks for your input on this. Are there some examples in HOL or HOL Light where the approach you suggest with option types is used? (Preferably some elementary theory where I won't get too lost as a non-mathematician.) This is unfamiliar to me except of course in the programming languag

Re: [Hol-info] Undefined operations such as division by zero in HOL

Konrad, Yes, your example with MOD and DIV I think is just the right sort of thing. It's still annoying to know that the result of dividing by zero is some number, but not as bad as having a definite but unexpected result, and the issue is less obtrusive this way, too. I presume that the same so

Re: [Hol-info] Undefined operations such as division by zero in HOL

In my opinion, the best way of dealing with this is to use option types: None denoting the undefined value. This makes function composition tedious but you can use a monad to make this easier. Now, it is not standard w.r.t. usual maths. But I'm not sure whether usual maths are doing this the ri

Re: [Hol-info] Undefined operations such as division by zero in HOL

Partial functions are annoying, no matter how you approach them. One way to introduce a partial operation in HOL is with new_specification. In contrast with new_definition, this allows you to introduce a constant with only its relevant properties. Consider, for example, the so-called division algo

[Hol-info] Undefined operations such as division by zero in HOL

Dear HOL experts, I am hoping for wisdom and recommendations from you all related to a question I have. Let me start with a bit of background information, which is here largely to orient you to my understanding of the situation. I know the facts are elementary. Usually in mathematics some operat