Email Gateway (Aug 18 2022 at 20:09): Email Gateway (Aug 18 2022 at 20:09):From: James Smith <jecs@imperial.ac.uk>
Good afternoon,
this is the first of several neophyte questions I suspect...
I've defined reflexive transitive closure...
theory rtc
imports Main
begin
inductive star :: "('a => 'a => bool) => ('a => 'a => bool)" for r where
base: "star r x x" |
step: "r x y ==> ( star r y z ==> star r x z )"
end
...and now want to apply this to a successor function I have on states...
definition succ :: "State => State => bool"
where "( succ x y ) \<equiv> ( index x = Suc(index y) )"
...where states are just records with an index field and other non
interfering fields:
record State =
index :: nat
...
My successor function works fine. If I instantiate a few states with the
obvious indeces I get, for example...
value "succ state_1 state_0"
...returning true, whereas
value "succ state_2 state_0"
returns false.
I (somewhat naively, it turns out) expected that...
value "star succ state_2 state_0"
..would return true, but it returns:
"star (\<lambda> u ua. Index = Suc( index ua)) (| index = Suc( Suc 0), ...\)
(| index = 0, ...|)"
My Coq colleagues in the room aren't suprised and tell me that my definition
of star is just that, and doesn't provide a way to actually compute the
transitive closure. Also, I note that if I do...
value "succ"
...I get "_", which I take to mean "some value", whereas if I do...
value "star"
...I just get "star", which I suspect has something to do with it.
Can anyone tell me what is going wrong and how to fix it?
Many thanks,
James
Email Gateway (Aug 18 2022 at 20:10):From: Tobias Nipkow <nipkow@in.tum.de>
Am 21/06/2012 14:31, schrieb James Smith:
Good afternoon,
this is the first of several neophyte questions I suspect...
I've defined reflexive transitive closure...theory rtc
imports Main
begininductive star :: "('a => 'a => bool) => ('a => 'a => bool)" for r where
base: "star r x x" |
step: "r x y ==> ( star r y z ==> star r x z )"end
...and now want to apply this to a successor function I have on states...
definition succ :: "State => State => bool"
where "( succ x y ) \<equiv> ( index x = Suc(index y) )"
...where states are just records with an index field and other non
interfering fields:record State =
index :: natI (somewhat naively, it turns out) expected that...
value "star succ state_2 state_0"
..would return true, but it returns:
"star (\<lambda> u ua. Index = Suc( index ua)) (| index = Suc( Suc 0), ...\)
(| index = 0, ...|)"My Coq colleagues in the room aren't suprised and tell me that my definition
of star is just that, and doesn't provide a way to actually compute the
transitive closure.
They are wrong. Isabelle (in contrast to Coq) can often execute inductive
definitions. Hence your expectation makes sense. However, there are several
difficulties with the way you have phrased your definitions:
code_pred start .
in order to generate code for star (or any inductive predicate).
star is higher order. This complicates code generation to the point that it
does not work for the situation where all arguments of "star r" are inputs. If
you fix r in the defn of star, it works better. But let's assume we stick with
your star.
What your defn of star will still allow us to do is to translate it into a
Prolog-like enumeration of all y such that "star r x y" for some given r and x.
This means not a single value but a set of values will be computed. The syntax is
values "{y. star succ state_0 y}"
inductive succ :: "State => State => bool"
where "y = x(|index := Suc(index x)|) ==> succ x y"
code_pred succ .
values 3 "{y. star succ state_0 y}"
Happy?
For an impressive example of what code generation for inductive predicates can
do see A. Lochbihler, L. Bulwahn : Animating the Formalised Semantics of a
Java-like Language. ITP 2011
http://pp.info.uni-karlsruhe.de/personhp/andreas_lochbihler.php
Also, I note that if I do...
value "succ"
...I get "_", which I take to mean "some value", whereas if I do...
value "star"
...I just get "star", which I suspect has something to do with it.
This is the result of the fact that "normal" definitions and inductive ones are
executed by different mechanisms.
Tobias
PS I have take the liberty to remove most of the blank lines from your email.
Many thanks,
James
Email Gateway (Aug 18 2022 at 20:10):From: James Smith <jecs@imperial.ac.uk>
Tobias, hi,
many thanks for your reply. I understand now that you don't need to execute
definitions in order to prove things about them. So, for example, the proof
that star' is indeed transitive doesn't require code_pred star', but
computing with it does. I find it fascinating that you can compute with
Isabelle in this way nonetheless.
More fundamentally, I do not want to create executable code, although I am
giving the impression that I do. I am just adjusting to the use of a theorem
prover after using a model checker. I should be proving things about the
types that I think up, rather than instantiating them. Creating instances of
State' to confirm that succ star' appears to be transitive is stupid when
I already have a proof that `star' is transitive without needing to execute
or indeed instantiate anything.
As an interesting aside, working with Isabelle in a room full of Coq users
seems to be working out fine. Those around me get an introduction to basic
Isabelle syntax amongst other things and I get valuable conversations about
theorem proving and types in general.
Kind regards,
James
Email Gateway (Aug 18 2022 at 20:10):From: Tobias Nipkow <nipkow@in.tum.de>
Of course, if you have a proof, there is no need to run test cases to check the
property. But with larger definitions, proofs become expensive enough that a bit
of rapid prototyping to weed out the most glaring bugs can be quite beneficial.
Tobias
Email Gateway (Aug 18 2022 at 20:12):From: Makarius <makarius@sketis.net>
Exchange of Isabelle and Coq users can indeed be quite interesting to
learn more about the specifc strengths and weaknesses of either system,
although there is a substantial overlap.
BTW, when a Coq user says "type" he means "proposition" in a more common
sense, which is also the way Isabelle uses term. So
theorem a: A <proof>
is just a theorem called "a" with proposition "A", which is proven by the
included proof. A Coq user would call "a" constant and "A" type here.
Anyway, Isabelle also has some terminology that first needs some
interpretation to be understandable to other people out there.
Makarius
Email Gateway (Aug 18 2022 at 20:18):From: James Smith <jecs@imperial.ac.uk>
Tobias, hi,
back with Isabelle today...
Hmm, I've just looked at this again. I think I haven't explained myself well
and so have been misunderstood. I have my definition of State:
record State =
index :: nat
cookies :: "Cookie set"
A cookie is just a string for the time being, and I instantiate one:
type_synonym Cookie = string
definition c :: Cookie where "counter=[CHR ''c'']"
I also instantiate a few states:
definition state_0 :: State where "state_0\<equiv>(|index=0,cookies={}|)"
definition state_1 :: State where "state_1\<equiv>(|index=1,cookies={c}|)"
definition state_2 :: State where "state_2\<equiv>(|index=2,cookies={c}|)"
Now with the succ predicate defined about the following...
value "succ state_0 state_1"
...returns false and it took me a while to work out why. If I delete the
cookie from state_1, or, alternatively, add a cookie to state_0, it works.
This is because the inductive predicate, as you rightly point out,
calculates the second argument from the first, taking x and changing its
index to get y. Therefore y is only the successor to x if y agrees in all
its other fields. But this isn't the required behaviour, y should be the
successor if its index is one greater, that's all.
I understand inductive definitions a little better now so I have, for
example:
Inductive succ :: "nat => nat => bool" where
"succ 1 0" |
"succ n m ==> succ (Suc n) (Suc m)
But how can I get this with states? I have a signature...
Inductive succ :: "nat => nat => bool" where
...
...but it's not obvious to me how I create a base step without instantiating
states, which I don't want to do except for ``testing''. I mean with nat you
already have an inductive set to work with, to do induction over, so
defining succ n m is easy from there. But with my states I don't have a
structure already in place so I can't do induction over it.
It seems to me I should just use "State list", in which case, if I take the
time to understand the functionality available with lists, I won't need to
define succ at all.
Regards,
James
Email Gateway (Aug 18 2022 at 20:18):From: Tobias Nipkow <nipkow@in.tum.de>
Hi James,
the relation you want is truly relational, you cannot compute one argument from
the other. Prolog can deal with such relations with the help of logical
variables and backtracking. Isabelle's execution mechanism does not support
logical variables but only backtracking. Thus you would need to enumerate all
the possible values of all the other fields, which is infeasible in general.
Tobias
Email Gateway (Aug 18 2022 at 20:18):From: James Smith <jecs@imperial.ac.uk>
Hi,
exactly. My point was that my bad explanation in the first place probably
led to a belief that computing states was what was required.
I realised this morning that I'd have to provide my own ``universe'' of all
instances of states in order for such calculations to work.
With type nat you get all the natural numbers to work with. With my type
State you get the type definition and nothing else.
Many thanks for all the help. I'll move on to lists now, thankfully!
Kind regards,
James
Last updated: Apr 18 2024 at 16:19 UTC