Re: [isabelle] making use of star



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
> 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
> 
> 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.

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:

1. You need to say

code_pred start .

in order to generate code for star (or any inductive predicate).

2. 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.

3. 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}"

4. This does still not quite work because "succ" is not defined in a manner that
the second argument can be computed from the first. It needs to be an inductive
definition

inductive succ :: "State => State => bool"
where "y = x(|index := Suc(index x)|) ==> succ x y"

code_pred succ .

5. Now the above values command does not terminate because there are infinitely
many successor states. You can look at the first 3 states like this:

values 3 "{y. star succ state_0 y}"

Happy?

6. The way you have written star makes it unsuitable for computing predecessors
from successors: values 3 "{x. star succ x state_2}" will not terminate because
star will call itself recursively forever without getting to a call of succ.

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
> 
>  
> 
>  
> 
>  
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.