[Gnu-arch-users] Re: formal foundations for the semantics of restricted mkpatch

[Tom Lord]

    > From: address@hidden

    > In this mail, I would like to set down some formal foundations for
    > discussing changesets in general and partial changesets in
    > particular.

I've gotten stuck trying to figure this out.    

    > CHANGESETS
    > ----------------------------------------------------------------------

    > A changeset C is a pair consisting of:

    >   - a tree     delta: Move(C)  : XPATHS -> XPATHS
    >   - a labeling delta: Patch(C) : XPATHS -> DATA -> DATA

    > where Move and Patch share the same domain (or co-domain, see next
    > section), and where Move is 1-to-1.  I'll write Dom(C) as short for
    > Dom(Move(C)).

This seems to be where I start to lose you.  The type of Patch(C)
makes no sense to me.

The general idea of "a labeling delta" makes sense to me, but I think
the type of such a function should be:

        labeling_delta :  Labeling <-> Labeling

in other words:

        labeling_delta :  (TREE <-> DATA) <-> (TREE <-> DATA)

I'm also a bit confused about whether DATA in your model is supposed
to be the contents of files or the id tags of paths.   It looks like
id tags but you do say at one point that its supposed to be contents.

Here's what I think is needed:

The most important thing to prove is:

----------------------------------------------------------------
* Prime Conjecture: selected mkpatch produces a sane changeset

  Given trees, ORIG and MOD, and limits, LIMITS:

  With:

        C := mkpatch_selected (ORIG, MOD, LIMITS)

        T := apply_changeset (C, ORIG)

        C2 := mkpatch (ORIG, T)

  Then:

        C = C2
----------------------------------------------------------------


That may be difficult to prove directly.

It needs to be shown that mkpatch_selected produces a valid changeset
(valid changeset needs to be defined).

It needs to be shown that the changeset C applies precisely to ORIG
(that tree T is well defined).  (apply_changeset and `applies
precisely' need to be defined.)

Given those, the prime conjecture might be easier to prove.

The prime conjecture doesn't prove that mkpatch_selected does anything
useful:  there are trivial and useless definitions of mkpatch_selected 
for which proving the prime conjecture would be very easy.  Two of
these are:

        mkpatch_selected (A,B,C) := mkpatch (A, B)

        mkpatch_selected (A, B, C) :=  "the empty changeset"

But the prime conjecture does at least show that a proposed
mkpatch_selected won't corrupt archives.

-t