Galactic algebra. A formal calculus connected with semi-functions, inclusion and equality
Algèbre galactique, un procédé de calcul formel, relatif aux semi-fonctions, à l'inclusion et à l'égalité
Résumé
Universal algebra is one of the theoretical foundations of computer
science. Nevertheless we cannot apply it directIy to reasoning about many
mathematical objects (such as fields) or about most programs (because of
exceptions) : we cannot consider any proper semi-function (partial function); we cannot distinguish any proper subset of the carrier. So we would like a more general theory. After having re-examined partial algebra and order-sorted algebra, each one being only a part of what is wished for, I have looked for and eventually
discovered a broader calculus, G algebra, connected with equality (universal
alg.), semi-functions (partial alg.), subsets and inclusion (order-sorted alg.).
This calculus is a formallogic which has these characteristics:
each term has a meaning (no nonsense); each item of information is coded as formula (not as a "declaration"); typing is proving (not parsing).
And which has these properties: the logic is complete (completeness theorem); G algebra is a homogeneous, clean superset of universal algebra; in each class of models there are a free algebra and an initial algebra.
L'algèbre universelle est l'un des fondements théoriques de l'informatique. Cependant elle est inapplicable à l'étude de nombreux objets mathématiques (les corps par exemple) et à la modélisation de logiciel (a cause des exceptions): 1) on ne peut considérer aucune semi-fonction stricto sensu (fonction partielle); 2) on ne peut distinguer aucun sous-ensemble stricto sensu du support. Aussi aimerait-on théorie plus générale. Apres avoir examiné l'algèbre partielle et l'algèbre ordosortée (order-sorted algebra), chacune n'étant qu'une partie de ce qu'on souhaite, j'ai cherché et trouvé un procédé de calcul encore plus général, l'algèbre g. Ce procédé est une logique formelle qui a ces caractéristiques: 1) tout terme a un sens (il n'y a pas de terme absurde); 2) toute information est codée comme une formule et d'aucune autre façon; 3) typer c'est prouver (le typage n'est pas grammatical). Et qui a ces qualités: 1) elle est complète (théorème de complétude); 2) l'algèbre universelle tout entière est comprise dans l'algèbre g; 3) chaque classe de modèles comprend un magma libre et un magma initial.
Origine : Fichiers produits par l'(les) auteur(s)