[darcs-users] Getting ready to sprint, camp team

[Florent Becker]

Florent Becker <florent.becker at ens-lyon.org> writes:
>>> 7/ Where to introduce names?
>>> 
>>
>> I think you may have missed the idea behind patch universes.
>>
> I probably did: i don't even know what a patch universe is (i mean
> what it bourbakily is).

Maybe I have not been that clear with this: i'd like to see a formal definition
of a patch universe, and i'd like to see it used in a proof. In the current state
of things, the notion is (half) introduced, but never used.
>
>> With unnamed patches we have some axioms, say A1 and A2.
>> With named patches we prove equivalent lemmas N1, N2.
>> With catches we prove equivalent lemmas C1, C2.
>>
>> Then the patch universe says: Given a patch type P, and lemmas L1 and L2
>> on P, there is a patch universe in which L3, L4, L5 are true.
> ok
>>
>> Roughly speaking, L1 and L2 are how triples of patches are related by
>> commutation, and L3+ are things like "patches in a sequence (or, indeed,
>> theentire universe) have a minimal context".
> So why not make L3 be "patches have a minimal context?" That's what I'm
> advocating (actually something a bit weaker: that they have a common
> straight context).

This part got lost a bit in the following, what i'm advocating is making this
common context an axiom, so that we can separate proving it from names
and using it.
>>
>> So the point of patch universes is that we don't have to prove that
>> named patches /and/ catches have minimal context, we only have to prove
>> that patch-like things have minimal context.

To reiterate: i propose to make that more explicit by introducing (ie axiomatising)
the concept of "patch-like things have minimal context". I think that proving that
named patches have a minimal context is an important and difficult problem 
(at least coq-wise), so that it should be duly isolated from proving that catches
work as designed and in polynomial time. I'm just advocating cutting the proofs
into more orthogonal modules (that's what axiomatising is).

>>> My proposal is to end the madness. I propose to add an axiom that says
>>> that we can decide whether two patches are related, and draw the consequences.
>>
>> I don't want to add axioms about named patches. Apart from anything
>> else, if you need to make it an axiom for named patches then I can't see
>> how you're going to do it for catches. Or to phrase it differently: If
>> you can prove it for catches, I'm sure you could prove it for named
>> patches, so it has no business being an axiom.

Let me state it another way: there is a big *qualitative* difference between going
from unnamed patches to named patches and from named patches to catches.
The first transition requires a device, fresh names, that is going to be problematic
to formalise, but the proofs are (should be) trivial given a well-chosen formalisation.
The second is standard in terms of formalism, but has proofs with real content.
That's why i think the reasonable course of action is to tackle them separately.
>
>
> So, what do we use name for? The only thing we do with them is to compare
> them for equality. (We don't order them, or concatenate them, for instance).
> So in fact what we're manipulating is the equivalence name(p) = name(q).
>
> What is this equivalence? It's the reflexive symmetric transitive closure of
> the relation (p,p') -> exists (q,q') <<p,q>> <~> <<q',p'>>. So in fact, all
> we are using name for is to have a decision procedure for this equivalence.
> (That's not quite exact: it also gives an explicit type for the classes of that
> equivalence, but in paper terms, that's not important). So what i propose
> is to make that decision procedure the axiom¹, and prove that using stored
> names works for that procedure somewhere else. Modularity again.
>
> So what I propose is to have a function name as a parameter, plus an axiom
> that says that name(p) = name(q) <-> p ~ q for that equivalence (i use a name
> function in order to be able to manipulate equivalence classes explicitly. There
> might be a better way). Then in another module, we prove that names given at
> patch creation and preserves through commutation fit the bill. This is another
> "obvious bit" where the coq proof is going to be unnecessarily hard, because
> we are going to have to model record, the only effectful operation. There we
> might have to use patch universes, but i want to keep their use to one module,
> and do that module last (I'd even advocate doing without it, since we _can't_ and
> _won't_ have correct name generation in a fully distributed setting).

Of course i had to forget the important bit! We also need to state what happens
when p !~ q, that is that they have a common straight ancestor context (a slightly
weaker assumption than a minimal context). This corresponds to the assumption
(or rule, …) that everything happens in _one_ patch universe (or that you always have
a patch universe containing all you need), which is _not_ trivial. So i'm not adding
new axioms, just giving them a shape that will make separation of concerns easier.

Hope this helps again

Florent