todays skype transcript
Dimitrios Vytiniotis
[13:34:21] *** Simon Peyton Jones added Dimitrios Vytiniotis, Koen Claessen ***
[13:34:27] Simon Peyton Jones: hi
[13:34:40] Simon Peyton Jones: Something popped up saying you were calling...?
[13:34:42] Koen Claessen: hi smon
[13:34:46] Koen Claessen: yes
[13:34:48] Koen Claessen: we have a meeting
[13:34:49] Dimitrios Vytiniotis: we have a phone meeting
[13:34:57] Koen Claessen: wondered if you could / wanted to join
[13:35:01] Koen Claessen: if not, that's OK
[13:35:18] Simon Peyton Jones: ok call me
[13:35:47] Koen Claessen: storm!
[13:36:23] Dimitrios Vytiniotis: Satus report:
[13:36:37] Dimitrios Vytiniotis: 1) Nathan continued impl the lemmas (now in)
[13:36:46] Dimitrios Vytiniotis: 2) I implemented a Coq back end
[13:36:53] Dimitrios Vytiniotis: 3) Nathan on-demand unrolling
[13:37:21] Dimitrios Vytiniotis: 4) We added back the projection-based translation of case expressions
[13:37:31] Dimitrios Vytiniotis: (strangely not performing any better)
[13:37:55] Koen Claessen: good idea
[13:37:58] Koen Claessen: examples?
[13:38:19] Dimitrios Vytiniotis: OPTIONS="-e Coq" run-tests.sh all
[13:38:50] Dimitrios Vytiniotis: egs/yes/add-symmetric.hs
[13:40:37] Koen Claessen: more info about eqNat
[13:41:43] Koen Claessen: have you looked at the model?
[13:41:53] Koen Claessen: it produces models anyway
[13:42:23] Dimitrios Vytiniotis: TODO:
[13:42:43] Dimitrios Vytiniotis: 1) Examine models for the problematic examples
[13:43:21] Dimitrios Vytiniotis: 2) Skolemize the final formula to get coutnerxamples with a_ terms
[13:43:27] Koen Claessen: OK
[13:43:32] Koen Claessen: needed for understanding models
[13:44:05] Koen Claessen: number (2) above leads to that
[13:45:18] Koen Claessen: Nathan: please send me those 2 TPTP files
[13:45:27] Koen Claessen: have not installed it
[13:45:29] Koen Claessen: yet
[13:48:21] Koen Claessen: $symbol
[13:48:25] Koen Claessen: means something special
[13:48:30] Koen Claessen: tool-specific
[13:48:30] Dimitrios Vytiniotis: thats the only change
[13:48:43] Dimitrios Vytiniotis: ==========================================
[13:48:51] Dimitrios Vytiniotis: DVs visit in Munich:
[13:49:48] Dimitrios Vytiniotis: 1) min() vs trigger's ?
[13:49:57] Koen Claessen: have not realized it is similar
[13:50:21] Koen Claessen: Jasmin made a finite model finder for Isabelle
[13:50:37] Koen Claessen: $min is like his trick
[13:50:54] Dimitrios Vytiniotis: 2) Andrey Rybalchenko and Ruslan Le....
[13:51:11] Dimitrios Vytiniotis: tool for checking properties of ocaml programs
[13:53:15] Koen Claessen: theory of list
[13:53:20] Koen Claessen: cons, nil append, =
[13:53:30] Koen Claessen: more functions: everything explodes
[13:54:07] Koen Claessen: already: careful with adding a theory for integers
[13:54:12] Koen Claessen: because of botto
[13:54:13] Koen Claessen: m
[13:54:40] Dimitrios Vytiniotis: #+ --->> the theory's +
[13:54:40] Simon Peyton Jones: data Int = I# Int#
[13:56:19] Koen Claessen: examples?
[13:56:21] Simon Peyton Jones: ask for examples
[13:56:52] Dimitrios Vytiniotis: 3) Dana's paper?
[14:06:41] Dimitrios Vytiniotis: ------------------ TASKS --------------------------
[14:06:52] Dimitrios Vytiniotis: A) Dimitrios queries people for tests and continues debugging
[14:07:09] Dimitrios Vytiniotis: B) Nathan implements skolemization and starts looking at the models for coutnerexamnples
[14:07:17] Dimitrios Vytiniotis: C) Koen tries to debug the TPTP files
[14:07:21] Dimitrios Vytiniotis: and build the tool
[14:08:35] Koen Claessen: x = Cons (head x) (tail x)
[14:08:41] Koen Claessen: exists a b . x = Cons a b
[14:09:07] Koen Claessen: x = Cons (somefun1 x) (somefun2 x)
[14:09:36] Simon Peyton Jones: So the first should be better.
[14:10:56] Dimitrios Vytiniotis: D) Dimitrios and Nathan tidy up the paper and their thoughts
[14:11:43] Dimitrios Vytiniotis: --------------------------------------------------- TASKS END -----------
[14:12:14] Dimitrios Vytiniotis: forall x. sel_1 (K_1 x) = x
[14:12:25] Dimitrios Vytiniotis: Question: where should the min's go?
[14:12:33] Dimitrios Vytiniotis: min(K_1 x)
[14:12:33] Koen Claessen: $min(K_1 x) =>
[14:12:59] Koen Claessen: we want K_1 injective
[14:13:25] Koen Claessen: adding $min is something you may do
[14:13:28] Koen Claessen: not must or need to
[14:13:33] Dimitrios Vytiniotis: i use
[14:13:52] Dimitrios Vytiniotis: min(K_1 x) \/ min(sel_1 (K_`1 x))
[14:14:32] Dimitrios Vytiniotis: [14:08] Koen Claessen:
<<< Cons (head x) (tail x)
[14:15:23] Koen Claessen: min(K_1 x) =>
[14:15:27] Koen Claessen: min(sel(K_1 x)) =>
[14:16:01] Dimitrios Vytiniotis: if x = (Cons x1 x2) and i'm trying to check that x = Cons (head x) (tail x), then don't i need to unfold (head (Cons x1 x2))?
[14:16:17] Koen Claessen: we know min(x)
[14:17:33] Koen Claessen: infinite models:
[14:17:42] Koen Claessen: (1) an injective function, (2) not surjective
[14:17:55] Koen Claessen: all x . f(x) != 0
[14:18:01] Koen Claessen: sel(f(x)) = x
[14:18:37] Koen Claessen: my student Ann Lillieström
[14:18:40] Koen Claessen: tool Infinox
[14:19:34] Dimitrios Vytiniotis: for ordinary function:
[14:19:38] Dimitrios Vytiniotis: f (S x) = x
[14:19:40] Dimitrios Vytiniotis: we produce:
[14:20:00] Dimitrios Vytiniotis: forall y, min (f y) /\ y = S x ==> f y = x
[14:20:21] Dimitrios Vytiniotis: sel (S x) = x
[14:20:47] Koen Claessen: definition:
[14:20:53] Koen Claessen: f (C x) = x
[14:20:57] Koen Claessen: two choices:
[14:21:04] Koen Claessen: min(C x) => f(C x) = x
[14:21:12] Koen Claessen: min(f(C x)) => f(C x) = x
[14:21:27] Koen Claessen: choice (1) is for when f is sel
[14:21:32] Koen Claessen: the second is weaker
[14:22:41] Dimitrios Vytiniotis: IF we could we would always pick the second
[14:22:54] Dimitrios Vytiniotis: But the second is too weak for injectivity
[14:23:05] Dimitrios Vytiniotis: it's injectivity only for the applied selectors in your "active term" set
[14:23:24] Dimitrios Vytiniotis: E) Nathan puts this discussion in the document
[14:23:32] Koen Claessen: have to go
Nathan Collins
Can you clarify what you said about infinite models when using
i. phi_project := forall x. min(pred (S x)) \/ min(S x) -> pred (S x) = x
vs
ii. phi_project := forall x. min(S x) -> pred (S x) = x
? Specifically, are you saying that we will *only* have infinite
models when using (i), or just that infinite models will be at least
as likely with (i) as with (ii)? If the latter, than I think I
understand: (i) implies (ii), so everything else being equal any model
for (i) is a model for (ii), but (ii) could have more models. But if
you are saying that we will *only* have infinite models with (i), then
I don't follow.
I understand the part about D is infinite if
exists f : D -> D, injective f /\ ~ surjective f,
I just don't understand why (i) and
phi_disjoint := forall x. min(S x) \/ min (Z) -> S x /= Z
allows us to prove the existence of such an f (yes, I understand we
can take f := S if there are no mins).
Thanks,
-nathan