Email Gateway (Aug 22 2022 at 09:15): Email Gateway (Aug 22 2022 at 09:15):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
Taking into account the discussion that follow, I would like to know if my
use of the constant "undefined" is correct
or justified. I wanted to avoid the option type at all costs and in some of
the
examples below I would not even know how to use it.
To begin with, I wanted to define a paryial recursive function such that the
following (informal) specification is satisfied:
sumR: int -> int ->_par int
-- a partial function to sum the first k integers between
-- l and u. It is not defined when l>u.
requires l <= u
ensures sumI(l,u) = \Sigma_{l<=k<=u} k
I came up with the following solution (well I did a pencil and paper
proof and have yet to check it with Isabelle/Isar):
function sumR:: "int => int => int" where
"sumR n n = n" |
"n < m ==> sumR n m = m + sumR n (m - 1)"|
"n>m ==> sumR n m = undefined"
apply atomize_elim
apply auto
done
termination sumR
apply (relation "measure (λ(i,N). nat ((N+1) - i))")
apply auto
done
Similarly, the definition of an integer division that satisfies the
following specification
div:: nat => nat => nat
requires n>0
ensures div m n = floor(m/n)
can be given by
function divV::"nat ⇒ nat ⇒ nat" where
"x < Suc y ==> divV x (Suc y) = 0"|
"x≥ Suc y ==> divV x (Suc y) = 1 + divV (x - Suc y) (Suc y)"|
"divV x 0 = undefined"
apply atomize_elim
apply auto
apply arith
done
termination by lexicographic_order
Then I remembered that primitive recursive definitions allow for non-
exaustive patterns.
So divV can be given a simpler definition like this:
fun divN:: "nat ⇒ nat ⇒ nat" where
"divN x (Suc y) = (if x < Suc y then 0 else 1 + divN (x - Suc y) (Suc y))"
In this case, Isabelle prints the following warning, which means to that it
uses "undefined" in the internal
workings of the primrec package.
constants
divN :: "nat ⇒ nat ⇒ nat"
Missing patterns in function definition:
/\ a. divN a 0 = undefined
Looking at previous discussions about this in the mailing list, I found
this enlightening explanation
from Andreas:
A long time ago (before Isabelle2009), "undefined" was called "arbitrary",
Thanks for any explanation of my use of "undefined".
Best!
Email Gateway (Aug 22 2022 at 09:15):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Alfio,
Your usage of undefined matches the usual conventions in Isabelle/HOL specification tools.
Whether it accurately models your specification depends on your understanding of the
specification. Nowadays in HOL, we are normally happy if we get a any function definition
that satisfies the specification. However, many packages internally refine the
specification. For example, you can prove that sumR evaluates to the same value for all
intervals (l,r) with r < l (but you don't know which one).
If you wanted to model say a hardware instruction of a processor with under-specified
behaviour, then this usage of undefined is probably not faithful, because the result of
executing the instructor for r < l may probably depend on l, r, the weather and whatever
else. So it really depends on what you are trying to define and do.
Andreas
Email Gateway (Aug 22 2022 at 09:15):From: David Cock <david.cock@inf.ethz.ch>
Just to reinforce this idea - there really is no getting away from the fact that HOL is a logic of total functions. If you try to define a partial function without e.g. option, you introduce unexpected relationships.
Email Gateway (Aug 22 2022 at 09:15):From: Andrew Butterfield <Andrew.Butterfield@scss.tcd.ie>
Hmmm - a little bit off topic .. is the meta-Logic of Isabelle also in effect a logic of total functions as well?
Or could you build a logic of partial functions on top of it ? … not that this would help Alfio much…
My understanding about undefinedness and/or partial functions is that there are a variety
of ways to work with them - three-valued logics, adding bottom elements to semantic domains, having definedness side-conditions (everywhere)
all with their plusses and minusses - but there is no way to avoid some pain. You have find whatever hurts leasts (which depends on what you are trying to do), and stick with that.
RAndrew
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
http://www.scss.tcd.ie/Andrew.Butterfield/
Email Gateway (Aug 22 2022 at 09:15):From: David Cock <david.cock@inf.ethz.ch>
There are people on this list better qualified to answer than me but no, the meta-logic does not require it. More general domains are possible, see HOL-CF.
Email Gateway (Aug 22 2022 at 09:15):From: Peter Lammich <lammich@in.tum.de>
On Fr, 2015-04-17 at 17:53 +0200, David Cock wrote:
There are people on this list better qualified to answer than me
The same applies to me ;)
but no, the meta-logic does not require it. More general domains are possible, see HOL-CF.
In my understanding, HOL-CF is build entirely on top of HOL,
introducing it's own function type, which is a (typedef) subtype of a=>b
In Pure, the reflexivity rule is already there, e.g., you can prove:
f x == f x
even for places x where f is undefined.
And you can use ==-equalities to prove substitutions in your theorems
(as done, e.g., by the (Pure) conversion mechanism).
Is this behaviour compatible with the goal of specifying a logic with
partial functions?
Email Gateway (Aug 22 2022 at 09:15):From: Larry Paulson <lp15@cam.ac.uk>
Yes it’s possible, e.g. a logic with a definedness predicate could be defined. LCF and HOLCF are also, in effect, logics of definedness, in that you can reason about whether or not something is the value UU (undefined), which really is treated specially, in that it induces a partial ordering on all types.
They are all a pain to use.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC