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é

Aristide Mégrelis (1, 2)

1 CRIN - Centre de Recherche en Informatique de Nancy
2 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

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.

Mots clés: Algèbre universelle; Algèbre partielle; Algèbre ordosortée; Agèbre galactique; Plasmas (gaz ionisés); Passivité (chimie); Contacts métal-semiconducteur; Diodes à barrière de Schottky

Domaines: Matière Condensée [cond-mat]

Aristide Mégrelis. Algèbre galactique, un procédé de calcul formel, relatif aux semi-fonctions, à l'inclusion et à l'égalité. Matière Condensée [cond-mat]. Université Henri Poincaré - Nancy 1, 1990. Français. ⟨NNT : 1990NAN10396⟩. ⟨tel-01754373⟩