Could someone send the Skype transcript for today's meeting?
1 view
Skip to first unread message
Nathan Collins
Dec 20, 2011, 9:37:53 AM12/20/11
to Haskell Contracts
Thanks!
Koen Claessen
Dec 20, 2011, 10:06:58 AM12/20/11
to haskellc...@googlegroups.com
Tuesday, December 20, 2011[1:35:29 PM CEST] Simon Peyton Jones: no
sound[1:35:33 PM CEST] Simon Peyton Jones: lots of hiss
thought[1:36:11 PM CEST] Simon Peyton Jones: He's looking
puzzled[1:36:15 PM CEST] Simon Peyton Jones: Waving fingers[1:36:21 PM
CEST] Simon Peyton Jones: Now puzzled again[1:37:22 PM CEST] Simon
Peyton Jones: Sound briefly then went[1:37:34 PM CEST] Simon Peyton
Jones: Tapping nose[1:37:53 PM CEST] Koen Claessen: no sound?[1:37:56
PM CEST] Simon Peyton Jones: No[1:38:16 PM CEST] Simon Peyton Jones:
You call me[1:38:17 PM CEST] Koen Claessen: let me restart
skype[1:38:29 PM CEST] Simon Peyton Jones: ok and I'll restart
too[1:38:31 PM CEST] Simon Peyton Jones: then you call[1:38:53 PM
CEST] Simon Peyton Jones: hello[1:39:56 PM CEST] Simon Peyton Jones:
What is the reasoning for when min is needed[1:40:00 PM CEST] Simon
Peyton Jones: and when it isn't[1:40:23 PM CEST] Koen Claessen: when
we say [| e ::: CF |]- = CF(e)[1:40:31 PM CEST] Koen Claessen: or [| e
::: CF |]- = min(e) & CF(e)[1:42:12 PM CEST] Simon Peyton Jones: What
does it mean to say "this is a minimal min translation"?[1:42:13 PM
CEST] Koen Claessen: [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [|
e ::: {x|p} |][1:42:19 PM CEST] Simon Peyton Jones: What
precisely?[1:43:28 PM CEST] Simon Peyton Jones: Formal claim: anything
we can prove without mins, we can prove with mins[1:43:47 PM CEST]
Simon Peyton Jones: "Minimal" means as few mins as poss, subject to
the above[1:44:04 PM CEST] Koen Claessen: we know: anything we can
prove with mins, we can prove without mins[1:44:34 PM CEST] Simon
Peyton Jones: [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e :::
{x|p} |][1:45:01 PM CEST] Koen Claessen: I had e ::: C and e :/:
C[1:45:45 PM CEST] Simon Peyton Jones: - is ::: ; + is :/:[1:46:29 PM
CEST] Simon Peyton Jones: - is ::: ; + is not :/:[1:49:13 PM CEST]
Koen Claessen: either say p[e/x] not-in {false, bad}[1:49:22 PM CEST]
Koen Claessen: or we say p[e/x] in {true, unr}[1:51:22 PM CEST] Koen
Claessen: [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e :::
{x|p} |][1:51:29 PM CEST] Koen Claessen: why is min(e) there?[1:51:57
PM CEST] Simon Peyton Jones: [| e ::: {x|p} |]+ = min(e) /\
min(p[e/x]) -> (e /= unr -> p[e/x] not-in
{false, bad})[1:52:19 PM CEST] Simon Peyton Jones: [| e ::: {x|p} |]-
= min(e) -> min(p[e/x]) /\ (e /= unr -> p[e/x]
in {true, unr})[1:53:05 PM CEST] Simon Peyton Jones: [| e ::: {x|p}
|]+ = min(e) /\ min(p[e/x]) -> (e /= unr ->
p[e/x] not-in {false, bad})[1:53:33 PM CEST] Simon Peyton Jones: a +
is something we provea - is something we assume[1:54:21 PM CEST] Simon
Peyton Jones: Assume: min(e) /\ min(p[e/x]) /\ e /= unr[1:54:28 PM
CEST] Simon Peyton Jones: Prove p[e/x] not-in {false, bad})[1:55:36 PM
CEST] Simon Peyton Jones: We need min(e) so that we can make use of
e/=unr[1:55:50 PM CEST] Simon Peyton Jones: We need min(p[e/x]) wo
that we can prove things about p[e/x][1:57:25 PM CEST] Simon Peyton
Jones: Koen's idea: [| e ::: C |] are the assumptions you get if you
assume e satisfies C[1:57:52 PM CEST] Simon Peyton Jones: [| e :/: C
|] are the assumptions you get if you know e does not satisfy
C[2:00:29 PM CEST] Simon Peyton Jones: [| e ::: x:c1 -> c2 |]+ = [| x
::: c1 |]- -> [| e x ::: c2 |]+[2:00:31 PM CEST] Simon Peyton Jones:
and dually[2:00:55 PM CEST] Simon Peyton Jones: [| e ::: CF |]+ =
min(e) -> CF(e)[2:01:13 PM CEST] Simon Peyton Jones: [| e ::: CF |]- =
CF(e)[2:04:23 PM CEST] Simon Peyton Jones: min( app(f,) ) ->
min(f)[2:05:29 PM CEST] Simon Peyton Jones: -- 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[2:07:07 PM CEST] Simon Peyton Jones: If there
exists a counter-model without mins, then there exists on with
mins[2:07:11 PM CEST] Simon Peyton Jones: And vice verat[2:10:06 PM
CEST] Simon Peyton Jones: Commutativity of addition, as a test case
for use of lemmas.Eventually worked by removing apps; then Paradox
could find counter-models[2:10:20 PM CEST] Simon Peyton Jones: Equinox
can diverge on things that are not true; Paradox does not[2:10:42 PM
CEST] Koen Claessen: counter example is circular?[2:10:48 PM CEST]
Koen Claessen: meaning infinite[2:11:05 PM CEST] Koen Claessen:
Equinox won't find infinite counter examples, Paradox can if they have
a finite representation[2:11:32 PM CEST] Simon Peyton Jones: Equinox
can diverge on things that are not *provable* (even if they are
true)[2:12:28 PM CEST] Simon Peyton Jones: Equinox can only find
finite counter-examples[2:12:38 PM CEST] Simon Peyton Jones: (unless
you are lucky)[2:13:41 PM CEST] Simon Peyton Jones: In the end it went
through only by stating that the lemma itself is CF[2:14:05 PM CEST]
Simon Peyton Jones: Moreover the statement of CF-ness needed to hold
even if lemma's argument were not validi[2:15:24 PM CEST] Simon Peyton
Jones: We'd like to understand this phenomenon more clearly[2:17:20 PM
CEST] Simon Peyton Jones: How can it take more time? Really![2:17:36
PM CEST] Simon Peyton Jones: if f x = e, and e has not BADs, then f
is cF[2:17:43 PM CEST] Simon Peyton Jones: (If it doesn't call
anythign else)[2:19:13 PM CEST] Simon Peyton Jones: f x = Cons x
[][2:19:46 PM CEST] Simon Peyton Jones: f x = case x of p1 -> Cons x
[] p2 -> [][2:22:34 PM CEST] Koen Claessen: f x = Cons x
[][2:22:39 PM CEST] Koen Claessen: f x = Nil[2:23:08 PM CEST] Simon
Peyton Jones: min(f x)[2:23:15 PM CEST] Simon Peyton Jones: now it'll
expand both defns[2:25:01 PM CEST] Simon Peyton Jones: I think we
agree: proving CF should be linear in the size of the program[2:25:21
PM CEST] Simon Peyton Jones: The constant factor willl be worse than a
syntactic tree traversal[2:25:53 PM CEST] Simon Peyton Jones: But if
the constant factor is grotesquely worse, the we probably are in
trouble anyway[2:31:47 PM CEST] Simon Peyton Jones: Problem: it's Too
Hard to know exactly which lemmas you need[2:32:25 PM CEST] Koen
Claessen: a flag called --split[2:32:45 PM CEST] Koen Claessen:
fof(monkey, conjecture, A & B & C).[2:34:22 PM CEST] Simon Peyton
Jones: forall x. ...[2:34:36 PM CEST] Simon Peyton Jones: negate it
and skolemize x to a_x[2:34:59 PM CEST] Koen Claessen: instead of
conjecture(forall x . P(x))[2:35:06 PM CEST] Koen Claessen: add
conjecture(P(a_x))[2:36:45 PM CEST] Simon Peyton Jones: add_symmetric
is a tough case!so we should not be discouraged[2:37:20 PM CEST] Simon
Peyton Jones: Park it, and return to real programs[2:38:18 PM CEST]
Simon Peyton Jones: Next priorities:a) Write paperb) Real programs
sound[1:35:33 PM CEST] Simon Peyton Jones: lots of hiss
thought[1:36:11 PM CEST] Simon Peyton Jones: He's looking
puzzled[1:36:15 PM CEST] Simon Peyton Jones: Waving fingers[1:36:21 PM
CEST] Simon Peyton Jones: Now puzzled again[1:37:22 PM CEST] Simon
Peyton Jones: Sound briefly then went[1:37:34 PM CEST] Simon Peyton
Jones: Tapping nose[1:37:53 PM CEST] Koen Claessen: no sound?[1:37:56
PM CEST] Simon Peyton Jones: No[1:38:16 PM CEST] Simon Peyton Jones:
You call me[1:38:17 PM CEST] Koen Claessen: let me restart
skype[1:38:29 PM CEST] Simon Peyton Jones: ok and I'll restart
too[1:38:31 PM CEST] Simon Peyton Jones: then you call[1:38:53 PM
CEST] Simon Peyton Jones: hello[1:39:56 PM CEST] Simon Peyton Jones:
What is the reasoning for when min is needed[1:40:00 PM CEST] Simon
Peyton Jones: and when it isn't[1:40:23 PM CEST] Koen Claessen: when
we say [| e ::: CF |]- = CF(e)[1:40:31 PM CEST] Koen Claessen: or [| e
::: CF |]- = min(e) & CF(e)[1:42:12 PM CEST] Simon Peyton Jones: What
does it mean to say "this is a minimal min translation"?[1:42:13 PM
CEST] Koen Claessen: [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [|
e ::: {x|p} |][1:42:19 PM CEST] Simon Peyton Jones: What
precisely?[1:43:28 PM CEST] Simon Peyton Jones: Formal claim: anything
we can prove without mins, we can prove with mins[1:43:47 PM CEST]
Simon Peyton Jones: "Minimal" means as few mins as poss, subject to
the above[1:44:04 PM CEST] Koen Claessen: we know: anything we can
prove with mins, we can prove without mins[1:44:34 PM CEST] Simon
Peyton Jones: [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e :::
{x|p} |][1:45:01 PM CEST] Koen Claessen: I had e ::: C and e :/:
C[1:45:45 PM CEST] Simon Peyton Jones: - is ::: ; + is :/:[1:46:29 PM
CEST] Simon Peyton Jones: - is ::: ; + is not :/:[1:49:13 PM CEST]
Koen Claessen: either say p[e/x] not-in {false, bad}[1:49:22 PM CEST]
Koen Claessen: or we say p[e/x] in {true, unr}[1:51:22 PM CEST] Koen
Claessen: [| e ::: {x|p} |]+ = min(e) /\ min(p[e/x]) -> [| e :::
{x|p} |][1:51:29 PM CEST] Koen Claessen: why is min(e) there?[1:51:57
PM CEST] Simon Peyton Jones: [| e ::: {x|p} |]+ = min(e) /\
min(p[e/x]) -> (e /= unr -> p[e/x] not-in
{false, bad})[1:52:19 PM CEST] Simon Peyton Jones: [| e ::: {x|p} |]-
= min(e) -> min(p[e/x]) /\ (e /= unr -> p[e/x]
in {true, unr})[1:53:05 PM CEST] Simon Peyton Jones: [| e ::: {x|p}
|]+ = min(e) /\ min(p[e/x]) -> (e /= unr ->
p[e/x] not-in {false, bad})[1:53:33 PM CEST] Simon Peyton Jones: a +
is something we provea - is something we assume[1:54:21 PM CEST] Simon
Peyton Jones: Assume: min(e) /\ min(p[e/x]) /\ e /= unr[1:54:28 PM
CEST] Simon Peyton Jones: Prove p[e/x] not-in {false, bad})[1:55:36 PM
CEST] Simon Peyton Jones: We need min(e) so that we can make use of
e/=unr[1:55:50 PM CEST] Simon Peyton Jones: We need min(p[e/x]) wo
that we can prove things about p[e/x][1:57:25 PM CEST] Simon Peyton
Jones: Koen's idea: [| e ::: C |] are the assumptions you get if you
assume e satisfies C[1:57:52 PM CEST] Simon Peyton Jones: [| e :/: C
|] are the assumptions you get if you know e does not satisfy
C[2:00:29 PM CEST] Simon Peyton Jones: [| e ::: x:c1 -> c2 |]+ = [| x
::: c1 |]- -> [| e x ::: c2 |]+[2:00:31 PM CEST] Simon Peyton Jones:
and dually[2:00:55 PM CEST] Simon Peyton Jones: [| e ::: CF |]+ =
min(e) -> CF(e)[2:01:13 PM CEST] Simon Peyton Jones: [| e ::: CF |]- =
CF(e)[2:04:23 PM CEST] Simon Peyton Jones: min( app(f,) ) ->
min(f)[2:05:29 PM CEST] Simon Peyton Jones: -- 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[2:07:07 PM CEST] Simon Peyton Jones: If there
exists a counter-model without mins, then there exists on with
mins[2:07:11 PM CEST] Simon Peyton Jones: And vice verat[2:10:06 PM
CEST] Simon Peyton Jones: Commutativity of addition, as a test case
for use of lemmas.Eventually worked by removing apps; then Paradox
could find counter-models[2:10:20 PM CEST] Simon Peyton Jones: Equinox
can diverge on things that are not true; Paradox does not[2:10:42 PM
CEST] Koen Claessen: counter example is circular?[2:10:48 PM CEST]
Koen Claessen: meaning infinite[2:11:05 PM CEST] Koen Claessen:
Equinox won't find infinite counter examples, Paradox can if they have
a finite representation[2:11:32 PM CEST] Simon Peyton Jones: Equinox
can diverge on things that are not *provable* (even if they are
true)[2:12:28 PM CEST] Simon Peyton Jones: Equinox can only find
finite counter-examples[2:12:38 PM CEST] Simon Peyton Jones: (unless
you are lucky)[2:13:41 PM CEST] Simon Peyton Jones: In the end it went
through only by stating that the lemma itself is CF[2:14:05 PM CEST]
Simon Peyton Jones: Moreover the statement of CF-ness needed to hold
even if lemma's argument were not validi[2:15:24 PM CEST] Simon Peyton
Jones: We'd like to understand this phenomenon more clearly[2:17:20 PM
CEST] Simon Peyton Jones: How can it take more time? Really![2:17:36
PM CEST] Simon Peyton Jones: if f x = e, and e has not BADs, then f
is cF[2:17:43 PM CEST] Simon Peyton Jones: (If it doesn't call
anythign else)[2:19:13 PM CEST] Simon Peyton Jones: f x = Cons x
[][2:19:46 PM CEST] Simon Peyton Jones: f x = case x of p1 -> Cons x
[] p2 -> [][2:22:34 PM CEST] Koen Claessen: f x = Cons x
[][2:22:39 PM CEST] Koen Claessen: f x = Nil[2:23:08 PM CEST] Simon
Peyton Jones: min(f x)[2:23:15 PM CEST] Simon Peyton Jones: now it'll
expand both defns[2:25:01 PM CEST] Simon Peyton Jones: I think we
agree: proving CF should be linear in the size of the program[2:25:21
PM CEST] Simon Peyton Jones: The constant factor willl be worse than a
syntactic tree traversal[2:25:53 PM CEST] Simon Peyton Jones: But if
the constant factor is grotesquely worse, the we probably are in
trouble anyway[2:31:47 PM CEST] Simon Peyton Jones: Problem: it's Too
Hard to know exactly which lemmas you need[2:32:25 PM CEST] Koen
Claessen: a flag called --split[2:32:45 PM CEST] Koen Claessen:
fof(monkey, conjecture, A & B & C).[2:34:22 PM CEST] Simon Peyton
Jones: forall x. ...[2:34:36 PM CEST] Simon Peyton Jones: negate it
and skolemize x to a_x[2:34:59 PM CEST] Koen Claessen: instead of
conjecture(forall x . P(x))[2:35:06 PM CEST] Koen Claessen: add
conjecture(P(a_x))[2:36:45 PM CEST] Simon Peyton Jones: add_symmetric
is a tough case!so we should not be discouraged[2:37:20 PM CEST] Simon
Peyton Jones: Park it, and return to real programs[2:38:18 PM CEST]
Simon Peyton Jones: Next priorities:a) Write paperb) Real programs
On Tue, Dec 20, 2011 at 3:37 PM, Nathan Collins
<nathan....@gmail.com> wrote:
> Thanks!
Reply all
Reply to author
Forward
0 new messages