Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2009-04-14

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
07:31 kowey joined #darcs-theory
12:57 Guest934 joined #darcs-theory
15:00 gal_bolle igloo: where have you gotten to with coq?
15:01 gal_bolle it would be nice to have a consensus on one version before/during the sprint
15:12 Igloo gal_bolle: I am stuck at two points:
15:12 Igloo Lemma NamedPatchCommutePreservesCommute
15:13 Igloo I don't think this is hard, it's just big, and I need to invert the right things and give them sensible names that match a picture so that I can follow what's going on
15:13 Igloo Lemma Foo
15:14 Igloo This I need to get the right induction pattern for
15:14 Igloo My aim for the Hackathon is to get NamedPatchCommutePreservesCommute done, and any other lemmas that I've skipped over up to now
15:15 Igloo And then to be able to describe better why Foo is true
15:15 Igloo Then hopefully you and/or Eelis (who's also said he's interested in this stuff) can tell me if/where I'm going wrong
15:16 Igloo gal_bolle: You won't be physically at the Hackathon, right?
15:19 Igloo gal_bolle: Oh, I was going to compare what we have after you modularised yours, but I completely forgot about it
15:20 gal_bolle ok, you can pull, i pushed everything
15:20 gal_bolle why does NamedPatchCommutePreservesCommute get so big?
15:21 gal_bolle ok, that's one point where having names as a construction rather than an axiom hits you
15:21 gal_bolle i think i have a middle ground for this.
15:21 Igloo http://urchin.earth.li/~ian/Named​PatchCommutePreservesCommute.png is the image
15:22 gal_bolle (note that i don't have any named patches stuff yet)
15:22 Igloo For each of those patches you have a named patch and an unnamed patch (plus various other bits and pieces), and when coq assigns them random names it's impossible to see what's going on
15:22 gal_bolle yes, that's the drawback of inversion
15:23 Igloo I was doing things like
15:23 Igloo inversion p1 as [? np ? ? ? up1].
15:23 gal_bolle you can try "rename toto into titi" to unconfuse things too
15:23 Igloo but I don't think that works, because coq doesn't consistently apply that everywhere
15:23 gal_bolle ok, so i'd like to talk about the big picture for a moment
15:23 gal_bolle is that ok with you
15:23 gal_bolle ?
15:24 gal_bolle or should i send a mail on the darcs-users list?
15:24 Igloo So I think I need to invert the p1-and-q1-invert hypothesis instead, and give names to everything that comes out of that. Maybe.
15:24 Igloo Here is fine
15:24 Igloo Mail is also fine, if you prefer that
15:24 Igloo Although the camp list might be better
15:24 gal_bolle there is a camp list?
15:25 * gal_bolle feels very stupid
15:25 Igloo http://projects.haskell.org/c​gi-bin/mailman/listinfo/camp
15:25 Igloo Don't worry, you haven't been missing much  :-)
15:25 Igloo Just some random status updates, I think
15:25 gal_bolle ok
15:26 * Igloo wonders if "Contacting us" is the wrong link text for the mailing list page
15:26 gal_bolle it's absolutely wrong
15:26 gal_bolle in my opinion
15:26 Igloo What's right, and also covers IRC?
15:27 gal_bolle forums is ugly but conveys the right message
15:27 gal_bolle (fora for additionned pedantism)
15:27 gal_bolle or discussions
15:27 Igloo Maybe there should be a "Mailing list" and "IRC" link to the same page
15:27 Igloo Anyway, big picture!
15:27 gal_bolle yes
15:28 gal_bolle so the big point of camp is names
15:28 gal_bolle do we agree?
15:28 Igloo No. The big point is correctness.
15:28 Igloo And simplicity
15:28 gal_bolle i mean the main innovation with respect to darcs
15:29 Igloo The main design choice difference is names
15:29 gal_bolle i agree about your two points wholly
15:29 gal_bolle ok, we agree
15:29 gal_bolle so my opinion is that we should introduce them as late as possible, with _one_ axiom
15:30 Igloo Would you want to do that if darcs didn't exist?
15:30 gal_bolle yes
15:30 gal_bolle it's orthogonal
15:30 gal_bolle let me explain why
15:31 gal_bolle picture yourself proving some theorem about named patches
15:31 gal_bolle you'll get a lot of patches on your sheet, which came from different part of your proof
15:32 gal_bolle and at a moment, you take p and q and say "either their names are different or they are equal"
15:32 Igloo assuming they have the same context
15:32 gal_bolle no, assuming nothing
15:32 Igloo OK, so not equal in the coq = sense then
15:33 gal_bolle no, they referred to the names
15:33 Igloo Oh, I see. Yes.
15:33 gal_bolle generally, the different-names branches will be easy, it's the case you are expected
15:34 gal_bolle that the names happen to be equal will be an "exceptional case"
15:34 gal_bolle s/expected/expecting/
15:34 gal_bolle so in the equal case, you want as much information as possible
15:35 Igloo There's a third case where the names are inverses, incidentally
15:36 gal_bolle that's why (in coqland) i'd like to have a reasonably big base of lemmas fo unnamed patches, and one axioms that says if (name p) = (name q) then R p q.
15:36 Igloo What is R?
15:36 gal_bolle yes, i consider this first case treated by "consider p^" (or "consider q^")
15:36 gal_bolle that's the point: what should R be?
15:37 Igloo You would still need to prove that (same name AND same context => some patch representation), for example
15:37 gal_bolle not necessarily
15:37 Igloo FWIW, here are the reasons I like my approach:
15:37 gal_bolle that's what my marked shuffles come from
15:37 Igloo Proving the named patch proofs is good practice for proving catch proofs
15:37 Igloo When proving catch proofs, we won't ever have to take apart named patches, so th
15:37 Igloo e fact that they are distinct from unnamed patches is irrelevant
15:37 Igloo I think that building named patches from unnamed patches and names is the right
15:37 Igloo mental model
15:38 Igloo Sigh, that pasted badly, sorry
15:38 gal_bolle it's ok
15:38 gal_bolle i agree with the premisses but not with the conclusion
15:39 gal_bolle my idea for R would be something a bit more involved like:
15:39 gal_bolle for every sequences (_:p:_) (_:p':_) such that name(p) = name(p')
15:40 gal_bolle there is a sequence (_:p'':_) from which the two above can be obtained
15:40 gal_bolle by commutation and patch deletion
15:40 gal_bolle (and maybe addition of qq^ pairs in the middle
15:40 gal_bolle )
15:40 gal_bolle with name p'' = name p
15:41 Igloo I don't think that you can make that an axiom
15:41 gal_bolle and patch addition
15:41 gal_bolle sorry
15:41 Igloo I think it's too complex
15:42 gal_bolle well, the sequence _:p'':_ is the context where (name p) was recorded
15:42 gal_bolle so it's in fact natural
15:42 gal_bolle if you look at it the other way, it says that every name was recorded once
15:43 Igloo I guess so
15:43 gal_bolle and every instance of that name comes from that record + commutation and legal addition of patches
15:43 Igloo But you might have to invent patches that have been unpulled in order to actually compute p''
15:43 Igloo In order to compute it by retracing your steps, I mean
15:44 gal_bolle yes, that's what the right part of p'' is for
15:44 gal_bolle it's also why i'm not sure about the final form of this R relation
15:44 * Igloo is unconvinced that that's going to be easier to work with
15:45 gal_bolle well, i find myself thinking «these patches come from the same record»
15:45 gal_bolle and i want a coq way to say that
15:46 Igloo I'm not sure I see why you're thinking that
15:46 Igloo Or rather, I'm not sure how that's different from "these patches have the same name" (when you're in a patch universe)
15:47 gal_bolle it's because i don't find that having "these patches have the same name" is a very good information to have
15:48 gal_bolle once you have that information, the only way to use it is to say "when the last of the two was recorded, the first existed already, so they were in fact recorded at the same time"
15:48 Igloo Do you want \start{lemma}{patch-in-univ​erse-has-minimal-context}?
15:49 gal_bolle rather patch-in-universe-has-original-context
15:49 gal_bolle but minimal would do equally well
15:49 kowey joined #darcs-theory
15:49 gal_bolle hi kowey
15:49 gal_bolle you've come at a historic moment…
15:49 kowey hi gal_bolle... ooh?
15:49 gal_bolle historical?
15:49 kowey ahistorical?
15:49 gal_bolle hysterical?
15:49 Igloo patch-in-universe-has-minimal-context is a lemma in the latex, can will be in the coq once we can prove it
15:50 gal_bolle moment
15:50 Igloo And you can prove your axiom given the properties a patch universe satisfies
15:50 gal_bolle one second (moment as a phrase is german, isn't it?)
15:50 gal_bolle igloo: it's equivalent
15:50 Igloo It's not an unheard of phrase in English
15:50 gal_bolle just like i prefer f a = f b -> a = b as a way to state injectivity
15:51 Igloo Although "one moment" is far more common
15:51 kowey erm... so I don't understand what you guys are saying, but sounds like a very good thing
15:51 gal_bolle rather than a <> b -> f a <> f b
15:52 Igloo The difference is, in that case I agree with you  :-)
15:52 Igloo I just didn't know how to use the former with coq
15:52 gal_bolle ok, then i just have to convince you that your current way of stating it is the double-negative one
15:52 gal_bolle and convince you to use my positive way
15:53 gal_bolle (new-age proof theory, eminced pepper mint…)
15:53 gal_bolle the never changing coq
15:53 gal_bolle the ever changing goal
15:53 Igloo My axioms are simpler than yours and can prove yours, so you'll have a tough job persuading me I think  :-)
15:54 gal_bolle my answers to those claims are: my axiom is _one_ axiom, hence it is simpler
15:54 gal_bolle and it can also prove yours
15:55 Igloo OK, which would you rather prove for Primitive unnamed patches, my axioms or yours?
15:55 gal_bolle they only differ on states versus sensible sequences, don't they
15:56 Igloo In fact, I don't even know how one could prove yours. You'd need something like the patch universe concept to stop me recording 2 patches with the same name
15:56 gal_bolle that's the point
15:56 gal_bolle that's exactly the point, thanks for pinning it down
15:57 gal_bolle i suppose that i have a magical way to prevent collisions
15:57 gal_bolle prove that with that magical device, everything is good
15:57 Igloo Whereas I don't need one (as far as the person providing unnamed patches is concerned)
15:57 gal_bolle sorry, i misread you
15:57 gal_bolle i don't need one either
15:58 gal_bolle we are discussing unnamed patches only
15:58 gal_bolle aren't we
15:58 * gal_bolle is getting a bit confused
15:58 Igloo Your axiom uses names
15:58 gal_bolle no, it uses states
15:58 Igloo "for every sequences (_:p:_) (_:p':_) such that name(p) = name(p'), ..."
15:58 gal_bolle yes, it's the names-elimination-axiom
15:59 gal_bolle everybody there is a named patch within a patch universe
15:59 gal_bolle i'm really getting confused
16:00 gal_bolle claim 1/ our formalisations of unnamed patches only marginally differ, with me using states and you sensible sequence, do you agree?
16:01 Igloo Yes, I have no opinions on unnamed patch representation in coq yet
16:01 gal_bolle ok
16:01 Igloo (or in the latex for that matter)
16:01 gal_bolle so my point is that current-camp is not a correct patch-universe
16:02 gal_bolle because the names are only in finite number
16:02 Igloo Do you mean the code isn't?
16:02 Igloo The set of names isn't required to be infinite
16:02 gal_bolle what i mean is that in a fully distributed system, we can't have a guaranteed way to have foolproof fresh-names generation
16:03 DanielC joined #darcs-theory
16:04 gal_bolle so you can't avoid names-clash
16:04 gal_bolle that's a fact we have to deal with
16:04 Igloo Ah, so you're saying that name clash avoidance needs to be an axiom?
16:04 gal_bolle how do you plan not to require it?
16:04 DanielC Question about patch theory: The only reason patches include context is so we know which patches to commute when we do a merge, but context does not actually affect the commutation rules at all, right?
16:05 Igloo Well, in order to use "record" in a patch universe you need to provide a name that isn't already used in that PU
16:05 gal_bolle ok, so it's an axiom of record that someone provides you with such a name
16:05 Igloo That's technically impossible in reality, of course, but we can wave our hands a bit
16:05 gal_bolle we agree on that course of axiom
16:05 gal_bolle of action sorry
16:06 Igloo It's not an axiom so much as a requirement of the operation
16:06 gal_bolle ok
16:06 Igloo record takes a mutable PU and a name not used in that PU, and mutates the PU. Or something.
16:06 gal_bolle ok
16:06 gal_bolle then i think i see where we disagree
16:06 Igloo Or you can sequence PUs like the IO monad. This is the unpleasant bit where we interact with the real world.
16:07 gal_bolle which is the first step towards agreement
16:07 Igloo :-)
16:07 gal_bolle and smiling is the second step
16:07 gal_bolle so :-) too
16:07 * Igloo picks up his shovel for step 3
16:08 gal_bolle if shovel-picking is step three, is it zeno's paradox?
16:08 gal_bolle so, i think you take a very algorithmic view of the proofs
16:08 gal_bolle you want to prove that this system with a mutable PU works
16:09 gal_bolle whereas i want something axiomatic (or descriptive, if you want)
16:09 Igloo It's PU manipulation where I think things become algorithmic
16:09 gal_bolle yes, i want to separate that algorithmic part from the logic part
16:09 gal_bolle so i have to separate two questions
16:09 Igloo Actually, maybe it doesn't have to be after all, as far as the theory is concerned
16:10 gal_bolle 1/ What's a working PU, what does it buy us?
16:10 Igloo Because we can freely copy PUs in theory
16:10 gal_bolle 2/ How do we get one
16:10 Igloo A PU is a set of repositories. It provides guarantees about the patches in these repositories
16:11 gal_bolle let me make that clearer
16:11 Igloo For example, every patch name has a unique minimal context in a PU
16:11 gal_bolle the crucial component of a PU is a Unique Name Generator
16:12 gal_bolle in fact, PUs are a tentative to encode unique name genarators, and one i'm not entirely satisfied with
16:13 gal_bolle do we agree on that (not on the satisfaction bit)
16:14 Igloo It's not really a generator as such, but OK
16:14 gal_bolle what i propose is to axiomatise this unique name generator with this R-axiom
16:14 Igloo record is something like:
16:15 Igloo If (N, repos@(repo:_), U) is a PU, n \in N, n \notin repos, u \in U, then (N, ((n, u):repo):repos, U) is a PU
16:16 Igloo where N is the set of names and U is the set of unnamed patches
16:17 Igloo And you can then prove that given you have a patch named n in two repos in that PU, that they share the same minimal context
16:17 gal_bolle ok
16:17 gal_bolle one moment
16:17 Igloo And that you can commute them directly to that context in the obvious way
16:18 gal_bolle what i don't like is the "n \notin repos" bit
16:19 gal_bolle that means that patch universes form an inductive type
16:19 gal_bolle with record, commute, merge as operations?
16:19 Igloo Yes
16:19 gal_bolle and unrecord
16:20 Igloo Yup
16:21 gal_bolle now if you have an hypothesis H: name p = name q
16:21 gal_bolle you'll need heavy inversion of the universe to find out how they are related
16:22 Igloo You'll have a lemma saying that they have the same minimal context
16:22 gal_bolle i want to see the proof of that lemma
16:22 gal_bolle it starts with "they come from the same record, and then, stuff happened"
16:23 gal_bolle and that's what i'm afraid of
16:23 gal_bolle and things i'm afraid of, i like to turn into axioms
16:24 Igloo OK, so the way I think it'll actually work is that there will be a property that is part of the inductive type that makes up a PU, and there will be a proof that record etc maintain the property
16:24 gal_bolle that's a kind of cowardness that's quite useful
16:24 gal_bolle ok, and that property will be my axiom, and the rest of the inductive construction won't see any use
16:25 Igloo Yes, but I think that we need to prove it, not axiomatise it
16:25 gal_bolle i half-agree
16:26 Igloo Incidentally, your lemma is false for darcs1 in theory and implementation, and the darcs2 implementation
16:26 Igloo Oh, I take that back, your lemma is true
16:26 Igloo But minimal contexts is false
16:26 gal_bolle aha
16:26 gal_bolle why?
16:26 Igloo And darcs can't actually use your lemma directly, because it might require patches that have been unpulled
16:27 gal_bolle of course
16:27 gal_bolle it's a lemma that should be used in proofs, not in code
16:27 Igloo s/lemma/axiom/g
16:27 gal_bolle goes without saying
16:27 Igloo See appendix B of the camp paper
16:28 Igloo I can dig up the script if you want to see the bug in action
16:28 gal_bolle oh yes, that's right
16:28 gal_bolle no it's ok
16:28 gal_bolle one moment
16:28 gal_bolle i thought that my axiom implied minimal context
16:29 gal_bolle it implies the record behaviour, doesn't it?
16:30 Igloo No, given PQR, your axiom allows a definition of commute that can give you PRQ and QRP but not RPQ
16:30 Igloo What do you mean by "the record behaviour"?
16:31 gal_bolle my axiom does not say anything about commute
16:31 Igloo http://hpaste.org/fastcgi/hpaste.fcgi/view?id=3787 is your axiom, right?
16:32 gal_bolle i keep commute-preserves-commute and commute-consistent
16:32 Igloo It says "by commutation"
16:32 gal_bolle yes
16:34 gal_bolle ok let me take it slowl
16:34 gal_bolle slowly
16:34 gal_bolle we have pqr
16:34 gal_bolle how do you apply my axiom?
16:35 Igloo If you take your axiom together with the other axioms then it will imply minimal contexts, but the other axioms imply that by themselves
16:36 Igloo But your axiom alone doesn't imply minimal contexts
16:36 gal_bolle no, that's right
16:36 gal_bolle i keep all axioms
16:36 gal_bolle and i replace the inductive definition of patch universes with my axiom
16:37 gal_bolle (the notion of patch universe goes out through the window@
16:37 Igloo So surely it's better to not have an extra axiom?
16:37 gal_bolle so surely it's better to not have an extra inductive type?
16:37 Igloo When we extent the proofs downwards, we'll have to prove it anyway
16:38 Igloo But the extra inductive type doesn't make the theorem/proof weaker
16:38 gal_bolle yes, like you'll have to prove it upward if you don't have it
16:38 Igloo Yes, but the whole goal is to prove these things
16:38 gal_bolle it's a question of where we cut through the sandwich between implementation and specification
16:39 gal_bolle my point is that
16:39 Igloo What we're currently calling axioms I'll want to prove for primitive patches at some point
16:39 gal_bolle i agre
16:39 gal_bolle agree
16:39 gal_bolle but slicing at the right place and isolating components is important
16:39 gal_bolle it can save us a lot of work
16:41 gal_bolle do you agree that either my axiom appears as a lemma in proving minimal context, or that (an implementation of) patch universes appear in proving my axiom
16:41 gal_bolle ?
16:41 gal_bolle ?
16:41 gal_bolle ?
16:41 gal_bolle sorry, that was a bit of lag
16:41 Igloo Also, the same proof that patches have minimal context will work for catches, because both of them form patch universes
16:42 Igloo I use something similar to your axiom, yes, in that I induct over a commuteRelates relation
16:43 gal_bolle ok
16:44 gal_bolle in my opinion the second alternative is better
16:45 arjanb joined #darcs-theory
16:45 gal_bolle because it allows one to use different ways to find unique names
16:45 * Igloo is lost - what's "the second alternative"?
16:46 gal_bolle maybe we could prove that some cryptographical scheme for name is cryptographically sure
16:46 gal_bolle stating my proposition as an axiom rather than a lemma
16:46 Igloo So how are you going to prove that catches have minimal contexts?
16:47 gal_bolle and having to prove that a global name dealer satisfies my axiom
16:47 gal_bolle by proving that going from patches to catches preserves my axiom
16:47 gal_bolle (that having my axioms on patches yields it as a theorem on catches)
16:47 gal_bolle i don't see how else _you_ are going to do
16:47 Igloo I think we'll have to agree to disagree  :-)
16:48 gal_bolle ok, i'll try to make that clear and in email form, i have to go
16:48 Igloo I prove that minimal contexts follows from the other axioms, so I don't need to show that catches satisfy your extra axiom
16:48 Igloo OK
16:49 gal_bolle yes, but you need an implementation of record that works in the presence of catches
16:49 gal_bolle see you
19:56 tux_rocker joined #darcs-theory
21:25 DanielC joined #darcs-theory
21:53 DanielC joined #darcs-theory

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary