Mins in arrow contracts
Nathan Collins
affect our tests, or Paradox's ability to find counter-models quickly
in conjunction with --no-ptr. I had observed before (on paper) that
if
[| e ::: CF |]+ = [| e ::: CF |]- = min(e) -> CF(e),
then we should be able to drop the mins from arrow contracts, since
the arrow mins become redundant (the base case (predicate and CF)
contracts all have min premises). But it seems to still be OK to drop
the arrow mins when they aren't redundant, i.e., when CF is translated
by
[| e ::: CF |]+ = min(e) -> CF(e)
[| e ::: CF |]- = CF(e)
The idea with dropping min obligations on CFs is that knowing 'CF(e)'
doesn't help us conclude 'min(e')' (all mins are still guarded by
mins), and so it shouldn't matter.
The min *assumption* in the positive tranlation is essential: we may
need to unfold a min-guarded definition to conclude that 'e' is CF.
But does anyone know any reason to keep the mins in arrow contracts?
Charle's writeup of the original min-translation has min's on (what
corresponds to) the negative arrow contracts, but I'm assuming this
was just a conservative choice.
The other min's are necessary, so we might now have a minimal min
translation:
-- Need 'min(e)' here to unfold defs.
[| e ::: CF |]+ = min(e) -> CF(e)
[| e ::: CF |]- = CF(e)
-- Need 'min(e)' and 'min(p[e/x])' here to unfold defs.
[| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e ::: {x|p} |]
-- Need 'min(e)' here to guard 'min(p[e/x])'.
-- Need 'min(p[e/x])' here to unfold defs.
[| e ::: {x|p} |]- = min(e) -> min(p[e/x]) /\ [| e ::: {x|p} |]
[| e ::: {x|p} |] = e /= unr -> p[e/x] not-in {false, bad}
-- No auxiliary mins.
[| e ::: x:c1 -> c2 |]v = [| x ::: c1 |](dual v) -> [| e x ::: c2 |]v
Thoughts?
-nathan
Nathan Collins
<nathan....@gmail.com> wrote:
> The other min's are necessary, so we might now have a minimal min
> translation:
>
> -- Need 'min(e)' here to unfold defs.
> [| e ::: CF |]+ = min(e) -> CF(e)
> [| e ::: CF |]- = CF(e)
>
> -- Need 'min(e)' and 'min(p[e/x])' here to unfold defs.
> [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e ::: {x|p} |]
> -- Need 'min(e)' here to guard 'min(p[e/x])'.
> -- Need 'min(p[e/x])' here to unfold defs.
> [| e ::: {x|p} |]- = min(e) -> min(p[e/x]) /\ [| e ::: {x|p} |]
> [| e ::: {x|p} |] = e /= unr -> p[e/x] not-in {false, bad}
>
> -- No auxiliary mins.
> [| e ::: x:c1 -> c2 |]v = [| x ::: c1 |](dual v) -> [| e x ::: c2 |]v
A related thought, about using
[| e ::: {x|p} |] = e /= unr -> p[e/x] not-in {false, bad}
instead of
[| e ::: {x|p} |] = e /= unr -> p[e/x] in {true, unr}
I think Koen said that we use the former because it's easier to prove?
I.e.,
e in {true, unr} -> e not-in {false, bad}
but not vice versa. But, of course, we only care about "easier to
prove" when we're proving. When we're using, we'd like to use the
stronger statement, yeah? So, we could instead use
[| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) ->
(e /= unr -> p[e/x] not-in {false, bad})
[| e ::: {x|p} |]- = min(e) -> min(p[e/x]) /\
(e /= unr -> p[e/x] in {true, unr})
Now, this has the interesting consequence that erasing min's no longer
collapses the the signed translation: without mins, the + and - cases
of the predicate translation are still different. However, if we also
take types into account, then actually
not-in {false, bad} <-> in {true, unr}
Thoughts?
-nathan
Dimitrios Vytiniotis
I like this. I suspect that under the assumption that min(e) both directions
may hold (because we are probably interested in well-typed terms only) but
your idea seems to me like a good plan and independent of the min/well-typedeness.
Does it make things faster as well? I'd be curious to learn.
Thanks
d-
________________________________________
From: Dimitrios Vytiniotis
Sent: Monday, December 19, 2011 10:26 PM
To: haskellc...@googlegroups.com
Subject: RE: Mins in arrow contracts
________________________________________
From: haskellc...@googlegroups.com [haskellc...@googlegroups.com] on behalf of Nathan Collins [nathan....@gmail.com]
Sent: Monday, December 19, 2011 10:22 PM
To: Haskell Contracts
Subject: Re: Mins in arrow contracts
Dimitrios Vytiniotis
I also like this as well. I don't think we need the mins in the arrow contracts any more.
________________________________________
From: haskellc...@googlegroups.com [haskellc...@googlegroups.com] on behalf of Nathan Collins [nathan....@gmail.com]
Sent: Monday, December 19, 2011 10:13 PM
To: Haskell Contracts
Subject: Mins in arrow contracts
Dimitrios Vytiniotis
as you wrote removing them from arrow contracts did not affect anything performance-wise in Paradox/Equinox,
so it is probably a good thing to remove them.
d-
________________________________________
From: haskellc...@googlegroups.com [haskellc...@googlegroups.com] on behalf of Nathan Collins [nathan....@gmail.com]
Sent: Monday, December 19, 2011 10:13 PM
To: Haskell Contracts
Subject: Mins in arrow contracts
I noticed that removing mins from arrow contracts doesn't seem to
Nathan Collins
run-time testing is very primitive. I run the whole test-suite, and
then run paradox on a version of lem_add_symmetric which is missing a
CF lemma. The whole test suite consistently take about 2:35 right now
(Simon Marlow is compiling two copies of GHC), but 2:00 of that is
timeouts, and the remaining 35s is divided among more than 20 tests.
Maybe interestingly, if I switch to using {true,unr} and {false,bad},
but backwards (I.e. swapping the + and - cases), then all but one test
behaves as before. The changed test is eqNat where
eqNat.hs.lem_eqnat_refl.tptp becomes counter satisfiable.
-nathan
Nathan Collins
> affect our tests, or Paradox's ability to find counter-models quickly
> in conjunction with --no-ptr. I had observed before (on paper) that
> if
>
> [| e ::: CF |]+ = [| e ::: CF |]- = min(e) -> CF(e),
>
> then we should be able to drop the mins from arrow contracts, since
> the arrow mins become redundant (the base case (predicate and CF)
> contracts all have min premises). But it seems to still be OK to drop
> the arrow mins when they aren't redundant, i.e., when CF is translated
> by
>
> [| e ::: CF |]+ = min(e) -> CF(e)
> [| e ::: CF |]- = CF(e)
>
> The idea with dropping min obligations on CFs is that knowing 'CF(e)'
> doesn't help us conclude 'min(e')' (all mins are still guarded by
> mins), and so it shouldn't matter.
I seem to have a counter example to this intuitive reasoning. Can
anyone explain? The counter example is that if I remove the 'min' in
min(CF(K e1 ... en)) -> CF(K e1 ... en) -> CF e1 /\ ... /\ CF en
then 'lem_eqNat_trans's contracts appear to no longer be provable (I
waited 4 minutes, but they used to take less than 30 seconds), and
when I remove the essential
lem_eqNat_trans ::: CF^3 -> CF
contract, Paradox no longer finds small counter models to
'lem_add_symmetric' (I waited and Paradox got up to size 9 without
finding anything). Paradox used to find size 3 or 4 counter models
here.
The other very disconcerting thing here, was that none of the "quick"
tests changed. I.e., in my 20 time limited regression suite, not a
single result changes when I remove the 'min' above. So, the current
examples don't seem to be sufficient for fine tuning the axioms, and
I'm a little concerned my removal of arrow 'min's could also be a
regression, but one for which I don't yet have evidence.
> The min *assumption* in the positive tranlation is essential: we may
> need to unfold a min-guarded definition to conclude that 'e' is CF.
> But does anyone know any reason to keep the mins in arrow contracts?
> Charle's writeup of the original min-translation has min's on (what
> corresponds to) the negative arrow contracts, but I'm assuming this
> was just a conservative choice.
>
> The other min's are necessary, so we might now have a minimal min
> translation:
>
> -- Need 'min(e)' here to unfold defs.
> [| e ::: CF |]+ = min(e) -> CF(e)
> [| e ::: CF |]- = CF(e)
>
> -- Need 'min(e)' and 'min(p[e/x])' here to unfold defs.
> [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e ::: {x|p} |]
> -- Need 'min(e)' here to guard 'min(p[e/x])'.
> -- Need 'min(p[e/x])' here to unfold defs.
> [| e ::: {x|p} |]- = min(e) -> min(p[e/x]) /\ [| e ::: {x|p} |]
> [| e ::: {x|p} |] = e /= unr -> p[e/x] not-in {false, bad}
>
> -- No auxiliary mins.
> [| e ::: x:c1 -> c2 |]v = [| x ::: c1 |](dual v) -> [| e x ::: c2 |]v
>
> Thoughts?
So, I had been thinking it was nice to remove 'min's, since the theory
becomes simpler, and easier to motivate, but maybe we want the
opposite: to introduce as many 'min's as possible without losing
provability?
-nathan
Nathan Collins
<nathan....@gmail.com> wrote:
> On Mon, Dec 19, 2011 at 10:13 PM, Nathan Collins
> <nathan....@gmail.com> wrote:
>> I noticed that removing mins from arrow contracts doesn't seem to
>> affect our tests, or Paradox's ability to find counter-models quickly
>> in conjunction with --no-ptr. I had observed before (on paper) that
>> if
>>
>> [| e ::: CF |]+ = [| e ::: CF |]- = min(e) -> CF(e),
>>
>> then we should be able to drop the mins from arrow contracts, since
>> the arrow mins become redundant (the base case (predicate and CF)
>> contracts all have min premises). But it seems to still be OK to drop
>> the arrow mins when they aren't redundant, i.e., when CF is translated
>> by
>>
>> [| e ::: CF |]+ = min(e) -> CF(e)
>> [| e ::: CF |]- = CF(e)
>>
>> The idea with dropping min obligations on CFs is that knowing 'CF(e)'
>> doesn't help us conclude 'min(e')' (all mins are still guarded by
>> mins), and so it shouldn't matter.
>
> I seem to have a counter example to this intuitive reasoning. Can
> anyone explain? The counter example is that if I remove the 'min' in
>
> min(CF(K e1 ... en)) -> CF(K e1 ... en) -> CF e1 /\ ... /\ CF en
Of course, I meant
0. min(K e1 ... en) -> CF(K e1 ... en) -> CF e1 /\ ... /\ CF en
For comparison, the no-min version is
1. CF(K e1 ... en) -> CF e1 /\ ... /\ CF en
> then 'lem_eqNat_trans's contracts appear to no longer be provable (I
> waited 4 minutes, but they used to take less than 30 seconds), and
> when I remove the essential
>
> lem_eqNat_trans ::: CF^3 -> CF
>
> contract, Paradox no longer finds small counter models to
> 'lem_add_symmetric' (I waited and Paradox got up to size 9 without
> finding anything). Paradox used to find size 3 or 4 counter models
> here.
Some variations, in comparison with (1):
2. (min(CF(K e1 ... en)) -> CF(K e1 ... en)) -> CF e1 /\ ... /\ CF en
3. (min(CF(K e1 ... en)) -> CF(K e1 ... en)) -> (min e1 -> CF e1) /\
... /\ (min en -> CF en)
For (2), everything becomes provable again, but Paradox still can't
find counter models under size 9 when the lemma is missing.
For (3), everything becomes provable again, and Paradox "gets stuck"
looking for counter models of size 6 (I waited 7 minutes).
> The other very disconcerting thing here, was that none of the "quick"
> tests changed. I.e., in my 20 time limited regression suite, not a
> single result changes when I remove the 'min' above. So, the current
> examples don't seem to be sufficient for fine tuning the axioms, and
> I'm a little concerned my removal of arrow 'min's could also be a
> regression, but one for which I don't yet have evidence.
>
>> The min *assumption* in the positive tranlation is essential: we may
>> need to unfold a min-guarded definition to conclude that 'e' is CF.
>> But does anyone know any reason to keep the mins in arrow contracts?
>> Charle's writeup of the original min-translation has min's on (what
>> corresponds to) the negative arrow contracts, but I'm assuming this
>> was just a conservative choice.
>>
>> The other min's are necessary, so we might now have a minimal min
>> translation:
>>
>> -- Need 'min(e)' here to unfold defs.
>> [| e ::: CF |]+ = min(e) -> CF(e)
>> [| e ::: CF |]- = CF(e)
>>
>> -- Need 'min(e)' and 'min(p[e/x])' here to unfold defs.
>> [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e ::: {x|p} |]
>> -- Need 'min(e)' here to guard 'min(p[e/x])'.
>> -- Need 'min(p[e/x])' here to unfold defs.
>> [| e ::: {x|p} |]- = min(e) -> min(p[e/x]) /\ [| e ::: {x|p} |]
>> [| e ::: {x|p} |] = e /= unr -> p[e/x] not-in {false, bad}
Actually, we now have
>> [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) ->
>> (e /= unr -> p[e/x] not-in {false, bad})
>> [| e ::: {x|p} |]- = min(e) -> min(p[e/x]) /\
>> (e /= unr -> p[e/x] in {true, unr})
here.
>> -- No auxiliary mins.
>> [| e ::: x:c1 -> c2 |]v = [| x ::: c1 |](dual v) -> [| e x ::: c2 |]v
>>
>> Thoughts?
>
> So, I had been thinking it was nice to remove 'min's, since the theory
> becomes simpler, and easier to motivate, but maybe we want the
> opposite: to introduce as many 'min's as possible without losing
> provability?
OK, so based on this we should put back the arrow 'min's. Or, as
observed before, putting 'min's in the negative (assumption) 'CF'
translation, the arrow 'min's become redundant. I.e., we change the
'CF' translation above to
[| e ::: CF |]v = min(e) -> CF(e)
and the question about arrow 'min's becomes irrelevant, because all
base cases are guarded by 'min'.
Interestingly, we get a big performance improvement now: the full
check of 'yes/add-symmetric.hs' goes from 48s to 30s. Also, Paradox
is still able to find the size three counter models.
On the other hand, adding even more 'min's, namely using (4) instead of (0)
4. min(K e1 ... en) -> CF(K e1 ... en)
-> (min e1 -> CF e1) /\ ... /\ (min en -> CF en)
makes the 'yes/add-symmetric.hs' run time increase again, by two to four
seconds (the GHC nightly build scripts have come to life now, and
timing is less reliable). This (4) seems more consistent with
[| e ::: CF |]- = min e -> CF e,
making it preferable, except for the performance degradation?
Why should we care about fine tuning the 'min' placement, besides the
performance increase? Because we would like to describe where the
translation comes from.
-nathan