undecidability issue (was: diff)

[Francois-Rene Rideau]

Codrin Nichitiu snidely remarked (:

> only a small remark about the diff utility
> (the one which would test that two representations have the
> same semantics 'up to isomorphism')...
>
> there is again a decidability problem for little tiny funny
> recursive definitions, right ? :)
>
> so a perfect diff won't really exist... how would you plan to
> go around that ?

Good question. [Tu auras un bon point]
   See my last explanatory post:
when making a diff between two objects,
an isomorphism may be *explicitly* given
up to which the diff is to be computed;
this isomorphism may be dynamically modified,
and arbitrary computer-aided tactics be used in search for it.
   And this, by definition, is reflection:
being able to dynamically define the tactics with which
the system will approximate non-computable objects.
   After all, even computable functions are only approximated
by real-world computers,
so I see no reason why non-computable functions
couldn't be approximated, too!
   The only restriction imposed by safety
is that no proof should never be trusted
that use axioms or promises of result
that were not agreed upon in the specification to be proven.
   If every object is annotated
by the axioms upon which rests its validity,
everything is fine!
   As a conclusion, nothing is ever perfectly perfect,
diff neither more nor less than anything else.

Personal P.S. long time no see. How are you doing at ENS-Lyon?
Do you know if the ens-lyon developed Coq system now allows for
Axioms not to be globally admitted?
Are they studying reflection for inclusion in their system?

== Fare' -- rideau@ens.fr -- Franc,ois-Rene' Rideau -- DDa(.ng-Vu~ Ba^n ==
Join the TUNES project for a computing system based on computing freedom !
                TUNES is a Useful, Not Expedient System
URL: "http://www.eleves.ens.fr:8080/home/rideau/Tunes/"