Algèbre galactique, un procédé de calcul formel, relatif aux semi-fonctions, à l'inclusion et à l'égalité - Université de Lorraine Access content directly
Theses Year : 1990

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é

Abstract

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.
Fichier principal
Vignette du fichier
SCD_T_1990_0396_MEGRELIS.pdf (7.73 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

tel-01754373 , version 1 (30-03-2018)

Identifiers

  • HAL Id : tel-01754373 , version 1

Cite

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⟩
82 View
64 Download

Share

Gmail Facebook X LinkedIn More