Contracts 13 Dec 11
Simon Peyton-Jones
· Risers: check counter-example from risers :: CF -> CF
· Counter-example generation still needs work Nathan
o [Koen] When the induction hypothesis isn’t strong enough, display in a nice way
o Nathan to send model for risers with only CF -> CF
· [Nathan] More info on why GHC7 is slower.
· Equality on natural numbers is transitive: times out. Why? [Nathan will send TPTP file to Koen]
· Nested case translation; red herring. All are now equivalent, but run at very different speeds.
· D has checked out examples from other folk: Dana (3), Andrei (10ish), Neil (harder to port)
· Todo: More Neil’s examples Dimitrios
· [Koen] Still to come: reworking Equinox’s architecture, so that (eg) a theory of constructors is easy to add. But doesn’t work with MIN. Maybe Koen will add lightweight support for exclusivity.
· Theory of integers [Dimitrios]
Notes for paper: Nathan (use for qualifying exam) Aim for ICFP deadline 12 March.
· MIN stuff
· Nested case translation (conj/disj and proj/quant/mixture).
· Lemmas
· Examples: 22 yes, 7 no.
· Polymorphic CF: significantly slows down proving; explain why
· Contribution: the minimal hooks needed in the theorem prover to make it fast
Real Haskell
· Datatypes
· Classes
· GADTs
· Theories
·
Nathan Collins
Could Simon or Koen forward the Skype chat transcript as well?
Thanks,
-nathan
Simon Peyton-Jones
[12:39:00 PM] Simon Peyton Jones: Made 'risers' work; needed a stronger contract than OK
[12:39:42 PM] Koen Claessen: && is there
[12:39:52 PM] Simon Peyton Jones: Function needs two contracts
[12:46:14 PM] Koen Claessen: TODO (Koen): display function tables of abstract functions
[12:49:17 PM] Koen Claessen: ghc 70.3
[1:10:03 PM] Simon Peyton Jones: (new) ![F,X] : ( CF(F) & CF(X) & min(app(F,X)) => CF(app(F,X)) )
[1:10:55 PM] Koen Claessen: (new) ![F] : ( ~CF(F) & min(F) => ?[X] : (CF(X) & ~CF(app(F,X)) &
min(app(F,X))) )
[1:11:05 PM] Koen Claessen: (new) ![F] : ( isFun(F) & ~CF(F) & min(F) => ?[X] : (CF(X) & ~CF(app(F,X)) &
min(app(F,X))) )
[1:14:21 PM] Koen Claessen: haskell-src-exts
[1:14:33 PM] Koen Claessen: but he ignores everything he does not want to dealwith
[1:14:37 PM] Koen Claessen: e.g. type classes
[1:14:42 PM] Koen Claessen: GADTs
[1:14:43 PM] Koen Claessen: etc.
[1:15:53 PM] Koen Claessen: open questions:
[1:15:58 PM] Koen Claessen: 1. contracts + datatypes
[1:16:03 PM] Koen Claessen: 2. contracts + type classes
[1:16:26 PM] Koen Claessen: 3. theories
[1:16:33 PM] Koen Claessen: (interpreted, axiomatized)
[1:18:44 PM] Koen Claessen: theory of constructors:
[1:18:47 PM] Koen Claessen: 1. injectivity
[1:18:50 PM] Koen Claessen: 2. exclusivity
[1:24:04 PM] Koen Claessen: publish paper:
[1:24:10 PM] Koen Claessen: 1. where (ICFP?)
[1:24:25 PM] Koen Claessen: 2. who (Simon, Dimitrios, Nathan, CP, Koen)
[1:25:11 PM] Koen Claessen: ~28 March I'll be out of office for ~2 weeks
[1:25:19 PM] Simon Peyton Jones: Deadline 12 March
[1:29:09 PM] *** Call ended, duration 56:44 ***
Nathan Collins
<sim...@microsoft.com> wrote:
> · Counter-example generation still needs work Nathan
>
> o Nathan to send model for risers with only CF -> CF
Risers TPTP and counter model with only the CF -> CF contract, and not
the CF¬-null -> CF¬-null contract, is attached. The counter
model, witht the "<..>" equations removed, is also below.
This looks similar to what Dimitrios and I saw before with counter
examples: we get a counter-example that isn't really, because we don't
have 'min' for it. Below we have
a_xs = x1 : x2 : x3
for some x1, x2, x3, and we have
cf(a_xs)
and
risers(a_xs) = bad
but there is no
min(risers(a_xs)).
Interestingly, we also have
app(risers_r,app(p2_Cons,a_xs)) = c_Nil,
i.e.
risers(x2:x3) = [],
another counter-example, up to the lack of 'min'. This is the sort of
"counter example to the lemma we haven't stated yet" that we're
looking for.
Here's the model file produced by equinox:
-- a_xs = x1 : x2 : x3
--
-- "pi" means "ith projection", and "f" means "full application". A
-- non-"f" function is a "pointer". Similarly, "c" is for "full
constructor application"
-- and "k" is for "partial/pointer".
a_xs := c_Cons("f__p1_Cons(a_xs)",c_Cons("f__p1_Cons(app(p2_Cons,a_xs))","app(p2_Cons,app
(p2_Cons,a_xs))"))
f__risers(a_xs) = bad
cf(unr) = $true
cf(c_Nil) = $true
cf(c_Zero) = $true
cf(c_True) = $true
cf(c_False) = $true
cf(a_xs) = $true
cf(f__p1_Cons(a_xs)) = $true
cf(app(p2_Cons,a_xs)) = $true
cf(f__p1_Cons(app(p2_Cons,a_xs))) = $true
cf(app(p2_Cons,app(p2_Cons,a_xs))) = $true
cf(c_Cons(c_Cons(app(p1_Cons,a_xs),c_Nil),c_Nil)) =
cf(c_Cons(c_Cons(app(p1_Cons,a_xs),c_
Nil),f__risers_r(app(p2_Cons,a_xs))))
app(risers,a_xs) = bad
app(risers_r,app(p2_Cons,a_xs)) = c_Nil
app(p1_Cons,c_Nil) = app(p1_Cons,f__risers_r(app(p2_Cons,a_xs)))
app(p1_Cons,a_xs) = f__p1_Cons(a_xs)
app(p1_Cons,app(p2_Cons,a_xs)) = f__p1_Cons(app(p2_Cons,a_xs))
app(p2_Cons,c_Nil) = app(p2_Cons,f__risers_r(app(p2_Cons,a_xs)))
app(app(k_Cons,f__p1_Cons(a_xs)),app(p2_Cons,a_xs)) = a_xs
app(app(k_Cons,f__p1_Cons(app(p2_Cons,a_xs))),app(p2_Cons,app(p2_Cons,a_xs)))
= app(p2_Co
ns,a_xs)
f__risers_r(app(p2_Cons,a_xs)) = c_Nil
c_Cons(f__p1_Cons(a_xs),bad) = c_Cons(app(p1_Cons,a_xs),bad)
c_Cons(f__p1_Cons(a_xs),c_Nil) = c_Cons(app(p1_Cons,a_xs),c_Nil)
c_Cons(f__p1_Cons(a_xs),app(p2_Cons,a_xs)) = a_xs
c_Cons(f__p1_Cons(app(p2_Cons,a_xs)),app(p2_Cons,app(p2_Cons,a_xs)))
= app(p2_Cons,a_xs)
sP52_dTrans__risers_or(a_xs) = $true
sP53_dTrans__risers_or(a_xs) = $true
sP54_dTrans__risers_or(a_xs) = $true
sP55_dTrans__risers_or(a_xs) = $true
$min(bad) = $true
$min(c_Nil) = $true
$min(a_xs) = $true
$min(k_Cons) = $true
$min(risers) = $true
$min(risers_r) = $true
$min(p2_Cons) = $true
$min(app(p2_Cons,a_xs)) = $true
$min(app(k_Cons,f__p1_Cons(a_xs))) = $true
$min(app(k_Cons,f__p1_Cons(app(p2_Cons,a_xs)))) = $true
$min(c_Cons(c_Cons(app(p1_Cons,a_xs),c_Nil),c_Nil)) =
$min(c_Cons(c_Cons(app(p1_Cons,a_xs
),c_Nil),f__risers_r(app(p2_Cons,a_xs))))
f__p2_Cons(a_xs) = app(p2_Cons,a_xs)
f__p2_Cons(app(p2_Cons,a_xs)) = app(p2_Cons,app(p2_Cons,a_xs))
Koen, or anyone, can you explain where the counter example is? It
seems we need
min(risers(a_xs)) /\ cf(a_xs) /\ ~ cf(risers(a_xs)),
for
fof(cTrans_risers,
axiom,
~((($min(f__risers(a_xs))
=> ((cf(a_xs))
=> ($min(f__risers(a_xs)) => cf(f__risers(a_xs)))))))).,
but again, we don't have the 'min' part as far as I can tell.
> · Equality on natural numbers is transitive: times out. Why?
> [Nathan will send TPTP file to Koen]
Solved this: the translation was buggy for functions of three or more
arguments. I think the transitivity lemma was our first three argument
function example :P The transitivity contract now checks!
Cheers,
-nathan
Koen Claessen
> This looks similar to what Dimitrios and I saw before with counter
> examples: we get a counter-example that isn't really, because we don't
> have 'min' for it.
Yes, this is expected since we will never get a "real" counter
example; the counter example must make use of the fact that we know
too little about risers_r.
> a_xs = x1 : x2 : x3
>
> for some x1, x2, x3, and we have
>
> cf(a_xs)
>
> and
>
> risers(a_xs) = bad
Indeed, any counter example must have cf(a_xs) and nonetheless
risers(a_xs) = bad since that follows from the negation of the
conjecture.
> but there is no
>
> min(risers(a_xs)).
Yes there is, since risers(a_xs) = bad and we have $min(bad).
> Koen, or anyone, can you explain where the counter example is?
Hm... I thought you had already found the counter example? The part
where it says:
risers_r (x1:x2) = []
does obviously not correspond to what the program does, yet it is
allowed by the induction we use. Thus, a strengthening of the IH is
needed, one that excludes the fact that risers_r returns an empty list
when we give it a non-empty list.
So, to understand counter models, we should look at:
1. The definitions of the a_* arguments, which speak for themselves
2. (Only for non-standard counter models, i.e. counter examples to
induction steps that are too weak) The function tables for any
"abstract" function, i.e. recursive occurrences of the function we are
working with (in this case risers_r) or any other function for which
we use the contract rather than its definition.
Important: all other function definitions are guaranteed to hold, so
no need to study the model for those. (Unless we want to debug our
translation rather than the Haskell program with the contracts in it.)
In our case, the only information we need to look at to understand the
model is:
1. a_xs := c_Cons("f__p1_Cons(a_xs)",c_Cons("f__p1_Cons(app(p2_Cons,a_xs))","app(p2_Cons,app(p2_Cons,a_xs))"))
2. f__risers_r(app(p2_Cons,a_xs)) = c_Nil
After renaming constructor functions and selector functions to
familiar names (something we of course will do in the actual version
of the tool):
1. xs := head(xs) : head(tail(xs)) : tail(tail(xs))
2. risers_r(tail(xs)) = []
Not so difficult to interpret, but we can do better I guess. Right
now, the model printing thingy only treats constructor functions
specially. But it is clear to me now that selector functions should be
treated specially too.
What we want to print out is something like:
1. xs := x1 : x2 : ys
2. risers_r(x2:ys) = []
But the theorem prover does not have any names like x1, x2, and ys,
and therefore picks the smallest representation of them in terms of
the functions it has. In my printing out thingy, I should do something
about this.
---
BTW, I notice another issue. You are mixing partial applications using
"app" and full applications. I conjecture that for this example (and
many others) all occurrences of app occurring in the TPTP problem are
actually fully applied. In CPA's implementation, we carefully avoided
the unneccessary use of app since it lead to performance problems.
Suggestion: Implement the following optimizations:
1. Before giving the TPTP file to the theorem prover, replace any term
where app's are used to construct a full application by the actual
full application (not using the "function pointer").
2. Remove any function pointer axioms for function pointers that are
not used anymore.
My expectation is that this greatly speeds up the problems we are solving.
> It
> seems we need
>
> min(risers(a_xs)) /\ cf(a_xs) /\ ~ cf(risers(a_xs)),
> [...]
I don't understand what this question means.
>> · Equality on natural numbers is transitive: times out. Why?
>> [Nathan will send TPTP file to Koen]
>
> Solved this: the translation was buggy for functions of three or more
> arguments. I think the transitivity lemma was our first three argument
> function example :P The transitivity contract now checks!
I am happy to hear this! (And curious to know what bug could make
everything work for 0, 1, 2 arguments, but not for 3! :-)
BTW, what happens to this example if you remove the two superfluous
occurrences of case-expressions on z (those that both end in QED,
might just as well replace the whole case with QED)?
/K
Koen Claessen
Some more comments regarding risers.
When I gave an informal presentation about this stuff at Chalmers a
couple of months ago, people were confused about the fact that a
function could have two different contracts (with two different
pre-conditions). They were talking about "the" pre-condition of a
function, and thus there should be a "the" contract.
Now, this is something that we need to keep in mind when we explain
it. We have "degraded" (or "generalized") the concept of contract
(where each function at most has one contract) to the concept of "some
property of a function in the shape of a contract".
That said, I was thinking about the following contract for risers.
risers :: xs&&CF -> { ys | not (null xs) || null ys }&&CF
Does this make sense? Is it provable?
/Koen
Koen Claessen
> 1. Before giving the TPTP file to the theorem prover, replace any term
> where app's are used to construct a full application by the actual
> full application (not using the "function pointer").
>
> 2. Remove any function pointer axioms for function pointers that are
> not used anymore.
I did this by hand (well, I used sed) on the risers example, and the
total time of the new problem was 40% of the time the old problem took
(~1s vs. ~2.5s).
/Koen
Nathan Collins
> HI all,
>
>> This looks similar to what Dimitrios and I saw before with counter
>> examples: we get a counter-example that isn't really, because we don't
>> have 'min' for it.
>
> Yes, this is expected since we will never get a "real" counter
> example; the counter example must make use of the fact that we know
> too little about risers_r.
I understand the part about the non-standard counter examples, but my
confusion was about the apparent lack of 'min', which you cleared up.
I was saying the example wasn't "real" because their was no 'min'.
>> a_xs = x1 : x2 : x3
>>
>> for some x1, x2, x3, and we have
>>
>> cf(a_xs)
>>
>> and
>>
>> risers(a_xs) = bad
>
> Indeed, any counter example must have cf(a_xs) and nonetheless
> risers(a_xs) = bad since that follows from the negation of the
> conjecture.
>
>> but there is no
>>
>> min(risers(a_xs)).
>
> Yes there is, since risers(a_xs) = bad and we have $min(bad).
Ah! Great, thanks, now it makes sense.
>> Koen, or anyone, can you explain where the counter example is?
>
> Hm... I thought you had already found the counter example?
Again, I hadn't found the 'min'.
> The part
> where it says:
>
> risers_r (x1:x2) = []
>
> does obviously not correspond to what the program does, yet it is
> allowed by the induction we use. Thus, a strengthening of the IH is
> needed, one that excludes the fact that risers_r returns an empty list
> when we give it a non-empty list.
And actually we have 'min' here as well, from 'min(C_Nil)', so my
risers(x2:x3) = [],
another counter-example, up to the lack of 'min'. This is the sort of
"counter example to the lemma we haven't stated yet" that we're
looking for.
is also resolved. Great!
> So, to understand counter models, we should look at:
>
> 1. The definitions of the a_* arguments, which speak for themselves
>
> 2. (Only for non-standard counter models, i.e. counter examples to
> induction steps that are too weak) The function tables for any
> "abstract" function, i.e. recursive occurrences of the function we are
> working with (in this case risers_r) or any other function for which
> we use the contract rather than its definition.
Will these counter-examples necessarily be in terms of the recursive
occurances? The regular function is defined in terms of the recursive
function (for a single unrolling).
> Important: all other function definitions are guaranteed to hold, so
> no need to study the model for those. (Unless we want to debug our
> translation rather than the Haskell program with the contracts in it.)
So here "other function definitions" means "functions we aren't
reasoning about"?
> In our case, the only information we need to look at to understand the
> model is:
>
> 1. a_xs := c_Cons("f__p1_Cons(a_xs)",c_Cons("f__p1_Cons(app(p2_Cons,a_xs))","app(p2_Cons,app(p2_Cons,a_xs))"))
>
> 2. f__risers_r(app(p2_Cons,a_xs)) = c_Nil
>
> After renaming constructor functions and selector functions to
> familiar names (something we of course will do in the actual version
> of the tool):
>
> 1. xs := head(xs) : head(tail(xs)) : tail(tail(xs))
>
> 2. risers_r(tail(xs)) = []
>
> Not so difficult to interpret, but we can do better I guess. Right
> now, the model printing thingy only treats constructor functions
> specially. But it is clear to me now that selector functions should be
> treated specially too.
>
> What we want to print out is something like:
>
> 1. xs := x1 : x2 : ys
>
> 2. risers_r(x2:ys) = []
This would be really good.
> But the theorem prover does not have any names like x1, x2, and ys,
> and therefore picks the smallest representation of them in terms of
> the functions it has. In my printing out thingy, I should do something
> about this.
>
> ---
>
> BTW, I notice another issue. You are mixing partial applications using
> "app" and full applications. I conjecture that for this example (and
> many others) all occurrences of app occurring in the TPTP problem are
> actually fully applied. In CPA's implementation, we carefully avoided
> the unneccessary use of app since it lead to performance problems.
>
> Suggestion: Implement the following optimizations:
>
> 1. Before giving the TPTP file to the theorem prover, replace any term
> where app's are used to construct a full application by the actual
> full application (not using the "function pointer").
>
> 2. Remove any function pointer axioms for function pointers that are
> not used anymore.
>
> My expectation is that this greatly speeds up the problems we are solving.
You spotted a bug. Thanks! Your (1) is supposed to already be
implemented, but I accidentally used partial application in the case
translation. Here's the fix:
diff --git a/src/Translation.hs b/src/Translation.hs
index 973415d..c3bfc47 100644
--- a/src/Translation.hs
+++ b/src/Translation.hs
@@ -195,7 +195,7 @@ dTrans fV vs ce = do
-- equation 'x = K(pi^K_1 x)'.
conCaseProject con ((c,vs),ce) = do
-- [Pi^C_i e / v]_{(i,v) \in enumerate vs}
- let sub = [ ((Named $ Proj i c) :@: eT, v)
+ let sub = [ (F.FullApp (Proj i c) [eT], v)
| v <- vs
| i <- [1..] ]
-- C (Pi^C_1 e) ... (Pi^C_n e)
:P You'll notice there aren't actually any "pointer" axioms for the
projectors, since they're never supposed to appear partially applied.
If I remember correctly, when I tried turning off (1) (which I call
"appification", altho "unappification" would probably be more
accurate) the performance degraded significantly.
However, this bug was masked for arity-1 term constructors,
e.g. 'Succ', because my appification code was sloppy and looked up the
arity of a projection as the arity of the corresponding term
constructor. The bug you observe happens for lists because the arity
of 'Cons' is 2, whereas all projectors actually have arity 1. The
sloppy arity lookup was supposed to be OK, because there should never
be a partially applied projection, since they only appear in generated
code. I changed the arity lookup to raise an exception when given a
projection, to avoid future code generation bugs like this.
Interestingly, the 'risers' as translated used undefined terms, the
partially applied projections. But everything still worked, I guess
because the structure was still axiomatized? E.g., we had
XS = Cons(undefined1,undefined2)
instead of
XS = Cons(head(XS),tail(xs))
but all we really cared about was the structure? In any case, the
fixed translation produces a similar counter model, and checks
'risers' when the 'non-null -> non-null' contract is added back.
I would like to try (2), but not right away, since I don't know an
simple way to do it (I could add pointer functions to the dependency
graph and then ignore them if they occur in their own SCCs, and
otherwise translate them into pointer axioms, but this is not
"simple").
>> It
>> seems we need
>>
>> min(risers(a_xs)) /\ cf(a_xs) /\ ~ cf(risers(a_xs)),
>> [...]
>
> I don't understand what this question means.
That's the negation of 'risers's 'CF -> CF' contract. So the counter
model needs to satisfy it, but I thought there was no
'min(risers(a_xs))', so I was confused as to how the model really was
a model.
>>> · Equality on natural numbers is transitive: times out. Why?
>>> [Nathan will send TPTP file to Koen]
>>
>> Solved this: the translation was buggy for functions of three or more
>> arguments. I think the transitivity lemma was our first three argument
>> function example :P The transitivity contract now checks!
>
> I am happy to hear this! (And curious to know what bug could make
> everything work for 0, 1, 2 arguments, but not for 3! :-)
I was accumulating backwards in the appification code, but
'reverse = id' for length 0 and 1 lists. The first arg was not in the
accumulator, making it work up to size 2. Here's the fix:
diff --git a/src/Haskell.hs b/src/Haskell.hs
index 77a69d7..eafdaba 100644
--- a/src/Haskell.hs
+++ b/src/Haskell.hs
@@ -40,7 +40,7 @@ appifyExpr a e = go e []
where e' = go e []
args' = e':args
- go (e1 :@: e2) args = go e1 (args++[go e2 []])
+ go (e1 :@: e2) args = go e1 (go e2 [] : args)
-- There should be no enclosing applications in these case,
so no args.
go (FullApp v es) [] = FullApp v $ map (\e -> go e []) es
:P
> BTW, what happens to this example if you remove the two superfluous
> occurrences of case-expressions on z (those that both end in QED,
> might just as well replace the whole case with QED)?
Good idea. Happily it still works, although the run-time does not
improve.
-nathan
Koen Claessen
Good.
> Will these counter-examples necessarily be in terms of the recursive
> occurances? The regular function is defined in terms of the recursive
> function (for a single unrolling).
I meant that in the model, there is lots of information. Most of it
(namely the function tables of functions that have definitions) is
immediately derivable from the Haskell program (meaning the theorem
prover has no choice in the matter, it just "explored" the definitions
of the function, learning about their behavior, and then printing this
in the model).
The information in the model that is not directly derivable from the
program are (in other words, choices the theorem prover has made that
we want to see):
1. The specific values of the arguments to the function we are
checking (i.e. the a_* values)
2. The function tables of abstract functions (where no definition was
given, perhaps only a contract). The abstract functions are (a) the
recursive occurrence of the function we are checking, (b) any other
function deemed abstract by the user.
Since the theorem prover can interpret these abstract function in any
way it likes, and it is important for the model how they are
interpreted, we need to look at them to understand the counter model.
(In contrast to functions of which we have given a definition, about
which we do not need to know much.)
So, when staring at a model, we can ignore everything except the above
two cases.
>> 1. xs := x1 : x2 : ys
>> 2. risers_r(x2:ys) = []
> This would be really good.
Indeed, not sure how to do this yet though.
> You spotted a bug. Thanks! [...] Interestingly, the 'risers' as translated used undefined terms, the
> partially applied projections. But everything still worked, I guess
> because the structure was still axiomatized?
It works for the same reason existential quantification works in
pattern matches. The projection based translation says:
"xs is a cons of these specific arguments"
the quantification based translation says:
"xs is a cons of some arguments"
but since we know that cons is injective, we can derive what these
arguments are using the injectivity axioms. What your buggy
translation says is:
"xs is a cons of these specific arguments about which we know nothing"
Nothing wrong there, we still use injectivity to find out what the
arguments are.
(BTW, quantification gets translated away to skolem functions. Every
time you quantify, you get a different skolem function. If you use
projections, you get (1) the same skolem function every time (namely
the projection), (2) the skolem function has less arguments (less free
variables). This is why I believe that the projection-based
translation is superior to the quantification translation.)
> I would like to try (2), but not right away, since I don't know an
> simple way to do it (I could add pointer functions to the dependency
> graph and then ignore them if they occur in their own SCCs, and
> otherwise translate them into pointer axioms, but this is not
> "simple").
How about
1. Generate the whole problem (without pointer axioms)
2. Replace all full applications using app by the actuall full application
3. Check which ptr_* constants still appear in the file, and only add
the pointer axioms for those
>> BTW, what happens to this example if you remove the two superfluous
>> occurrences of case-expressions on z (those that both end in QED,
>> might just as well replace the whole case with QED)?
>
> Good idea. Happily it still works, although the run-time does not
> improve.
OK, good that it works.
/Koen
Nathan Collins
So, I guess what I'm asking is: should we consider defined functions
abstract, in case (2), if we are checking contracts for them?
E.g. for
add x y = case x of
Z -> y
S x' -> S (add x y)
we get
add x y = case x of
Z -> y
S x' -> S (add_r x y)
if we are checking a contract for 'add', and so conceivably the
counter model could have
add (S Z) Z = S (S (S (S (S Z))))
just as easily as it could have some other "nonsense" about 'add_r'?
Or are you saying we'd only ever see, e.g.,
add_r (S Z) Z = S (S (S (S (S Z))))
in the counter model?
>> You spotted a bug. Thanks! [...] Interestingly, the 'risers' as translated used undefined terms, the
>> partially applied projections. But everything still worked, I guess
>> because the structure was still axiomatized?
>
> It works for the same reason existential quantification works in
> pattern matches. The projection based translation says:
>
> "xs is a cons of these specific arguments"
>
> the quantification based translation says:
>
> "xs is a cons of some arguments"
>
> but since we know that cons is injective, we can derive what these
> arguments are using the injectivity axioms. What your buggy
> translation says is:
>
> "xs is a cons of these specific arguments about which we know nothing"
>
> Nothing wrong there, we still use injectivity to find out what the
> arguments are.
>
> (BTW, quantification gets translated away to skolem functions. Every
> time you quantify, you get a different skolem function. If you use
> projections, you get (1) the same skolem function every time (namely
> the projection), (2) the skolem function has less arguments (less free
> variables). This is why I believe that the projection-based
> translation is superior to the quantification translation.)
Thanks, all this makes sense.
>> I would like to try (2), but not right away, since I don't know an
>> simple way to do it (I could add pointer functions to the dependency
>> graph and then ignore them if they occur in their own SCCs, and
>> otherwise translate them into pointer axioms, but this is not
>> "simple").
>
> How about
>
> 1. Generate the whole problem (without pointer axioms)
>
> 2. Replace all full applications using app by the actuall full application
>
> 3. Check which ptr_* constants still appear in the file, and only add
> the pointer axioms for those
Yes, this should work. Also not "simple", but probably has an added
benefit: currently the appification happens in a few different places,
to avoid appifying the pointer axioms themselves. With your approach
I could probably appify once, in one place.
-nathan
Koen Claessen
>
> add x y = case x of
> Z -> y
> S x' -> S (add_r x y)
>
> if we are checking a contract for 'add', and so conceivably the
> counter model could have
>
> add (S Z) Z = S (S (S (S (S Z))))
>
> just as easily as it could have some other "nonsense" about 'add_r'?
> Or are you saying we'd only ever see, e.g.,
>
> add_r (S Z) Z = S (S (S (S (S Z))))
>
> in the counter model?
We see function tables for both add and add_r in the model of course.
But only add_r can behave strangely, since add still has a definition,
which its function table will respect. (Yes, add can behave strangely
too, but only through add_r, so we might just as well ignore it.)
/Koen
Nathan Collins
> Hi all,
>
> Some more comments regarding risers.
>
> When I gave an informal presentation about this stuff at Chalmers a
> couple of months ago, people were confused about the fact that a
> function could have two different contracts (with two different
> pre-conditions). They were talking about "the" pre-condition of a
> function, and thus there should be a "the" contract.
>
> Now, this is something that we need to keep in mind when we explain
> it. We have "degraded" (or "generalized") the concept of contract
> (where each function at most has one contract) to the concept of "some
> property of a function in the shape of a contract".
>
> That said, I was thinking about the following contract for risers.
>
> risers :: xs&&CF -> { ys | not (null xs) || null ys }&&CF
>
> Does this make sense? Is it provable?
In our current syntax it's:
{-# CONTRACT
risers ::: xs:CF -> { ys : not (null xs) `or` null ys }&&CF
#-};;
It's not strong enough, because it doesn't tell us that 'ys' is
non-null when 'xs' is. Equinox finds the corresponding theory counter
satisfiable. But, both of the following variations work
(unsatisfiable):
{-# CONTRACT
risers ::: xs:CF -> { ys : (not (null xs) `and` not (null ys)) `or`
(null xs `and` null ys) }&&CF
#-};;
{-# CONTRACT
risers ::: xs:CF -> { ys : not (null xs) `implies` not (null ys) }&&CF
#-};;
The latter includes the extra lemma in a straight-forward way.
Cheers,
-nathan
Koen Claessen
> risers ::: xs:CF -> { ys : not (null xs) `implies` not (null ys) }&&CF
> #-};;
The above is what I actually meant, good it went through!
(same as
risers ::: xs:CF -> { ys : null xs || not (null ys) }&&CF
)
So, in this case there is no real need for multiple contracts. Do we
have any examples where this is a real need? I.e. two contracts with
conflicting pre-conditions?
My guess is that in most cases, we can rewrite to one contract.
(Modularity is of course still a good reason to allow multiple
contracts.)
/Koen
Nathan Collins
I don't have a concrete example, but wouldn't we have trouble if not
all of the contracts required CF of some argument? The above trick
works, because
{x:p} -> {y:q}
is the same as
x:Any -> {y: p `implies` q}
But we can't play the same game with CF, right? For
x:CF -> {y:q}
there is no way move the CF into the predicate 'q'. So e.g.
f ::: x:CF -> {y:q1}
f ::: {x:p} -> {y:q2}
can't be combined? We could safely approximate with
f ::: x:CF -> {y: q1 `and` (p `implies` q2)}
but I don't see how to combine exactly.
-nathan