--- Juliusz Chroboczek <[EMAIL PROTECTED]> escribi�:
> Dear Antonio,
>
> There are quire a few formalisations of patches possible; I know, for
> one, that my mental image of what Darcs is doing is very different
> from yours, and I know it's also very different of David's.
>
> The only reason why a formalisation should be preferred to others is
> that it allows one to make proofs.
>
> Thus, I believe that we should refrain from adding another formalisa-
> tion to the manual until we have one that is powerful enough to allow
> a formal proof of the correctness of the Darcs model (not necessarily
> of the algorithms used in Darcs, mind you).
Yes, of course. My formalism can be used to prove theorems 1 and 2, but it has
nasty properties:
it excludes useful patches, and all patches commute. To make an useful and
consistent theory I
have to solve two problems:
(i) How to define inverses for every patch, if needed.
(ii) I don't understand the merging algorithm yet.
For (i), I need to know if darcs really needs invertible patches and for what
it needs them. So,
for (i) and (ii) I want to look at the code. The final theory can be very
different from the
implementation, and possibly it can be found without looking at the code, but
anyway looking at
the code will be helpful, I think.
How is your mental image of darcs?
Best regards,
Antonio Regidor Garc�a
______________________________________________
Renovamos el Correo Yahoo!
Nuevos servicios, m�s seguridad
http://correo.yahoo.es
_______________________________________________
darcs-users mailing list
[email protected]
http://www.abridgegame.org/mailman/listinfo/darcs-users
