Auteur Message
Administrateur
Avatar de l’utilisateur
— Édit: ce que ce message exposait, s’avère être une possible mauvaise idée. Il n’est pas sans intérêt, mais à prendre avec précaution. —

Hibou a écrit : 
[…]

En parlant de syntaxe, la syntaxe des termes n’a pas besoin de faire partie des règles du langage, non‑plus. Elle serait définie, mais à côté. Par rapport au langage et au domaine client, la syntaxe des termes pourrait être tenue pour une évidence, un fait incontournable de leurs univers, de la même manière que dans le notre, la structure de la matière est un fait incontournable, on ne vérifie pas que de la matière est bien organisée comme elle doit l’être, quand on en utilise.

[…]

Oui mais non. Une représentation interne est nécessaire et elle ne se distingue pas d’une syntaxe. Ce qui a fait dire par erreur qu’aucune syntaxe n’est nécessaire parce que les constructions sont considérées comme correctes parce qu’il ne peut pas en être autrement, c’est qu’il n’y a pas par exemple, de notion d’équilibrage des parenthèses ouvrantes et fermantes.

Un processus magique est encore à l’œuvre, c’est la correspondance introduite précédemment.

L’élément central du langage, le terme, doit être défini entre autres en terme de termes. C’est une représentation dans le langage lui‑même. Pourtant c’est aussi une potentielle représentation externe, la traduction se faisant par correspondance. Si la correspondance n’existe pas, rien n’existe, il n’y a alors pas d’erreur de syntaxe possible. Les choses sont telles qu’elles ne peuvent que être ou elles ne sont pas.

Détail amusant : on peut définir une constante ou une variable, comme étant à priori n’importe quoi, à un détail prêt.

Le terme est une chose central dans le langage et le terme le plus élémentaire, est une constante. Une constante pourrait être définie comme ceci :

(letter a).
(letter b).
(letter c).
-- Etc.
(name (name1 L)) : (letter L).
(name (name2 L N)) : (letter L) & (name N).
(term (const N)) : (name N).

Ça semble aller de soi, si on veut coller aux conceptions habituelles, une constante est un mot, un mot est une suite de lettres, l’ordre des lettres est important pour l’égalité ou pas de deux suites de lettres.

Mais cette définition plus simple et même plus immédiate, est possible aussi :

(term (const C)).

Ce n’est pas tout à fait n’importe quoi, c’est C, qui peut être n’importe quoi, mais (const C) n’est pas n’importe quoi, par le fait de const, qui caractérise ce terme comme une constante, en supposant qu’aucune règle n’en fait une autre interprétation. Mais C, peut vraiment être n’importe quoi, l’égalité étant définie, c’est suffisant. C’est amusant et parfaitement abstrait.

Naturellement, il est possible de définir une variable de la même manière :

(term (var V)).

C’est aussi une chose qui peut tenter de dire que ce n’est pas une syntaxe, comme il n’y a par exemple ici pas de notion de mot commençant par une majuscule. Mais ça peut être considéré comme une syntaxe aussi, même si en pratique, la syntaxe sera mieux définie séparément, accompagnée d’une définition de la correspondance entre sa représentation et la représentation interne du langage.
Profil
Administrateur
Avatar de l’utilisateur
— Édit: ce message repose sur une précédente possible mauvaise idée. Il n’est pas sans intérêt, mais à prendre avec précaution. —

Hibou a écrit : 
[…]

Mais cette définition plus simple et même plus immédiate, est possible aussi :

(term (const C)).

Ce n’est pas tout à fait n’importe quoi, c’est C, qui peut être n’importe quoi, mais (const C) n’est pas n’importe quoi, par le fait de const, qui caractérise ce terme comme une constante, en supposant qu’aucune règle n’en fait une autre interprétation. Mais C, peut vraiment être n’importe quoi, l’égalité étant définie, c’est suffisant. C’est amusant et parfaitement abstrait.

Naturellement, il est possible de définir une variable de la même manière :

(term (var V)).

[…]

L’égalité étant supposée définie sur ce « n’importe quoi » abstrait, l’égalité doit‑elle être définie explicitement ou pas sur des constructions comme les termes ?

Ce n’est qu’une opinion personnelle, mais je crois qu’il faut définir ce qui est définissable et réduire au minimum ce qui ne l’est pas. Il ne faut invoquer la magie que quand il n’est pas possible de faire sans, une ressource si précieuse, s’utilise peu et discrètement.

Précisément, la relation spéciale, « = » pourrait justement n’être vérifiée que sur des choses purement abstraites, absolument non‑interprétables par le langage, en tous cas pas autrement qu’à travers cette égalité. Ce n’est pas que le test de l’égalité échouerait, c’est que son usage serait invalide. Comment le représenter formellement ? Je ne sais pas.

En tous cas dans ce point de vu personnel, une règle telle que celle‑ci :

(eq (const C1) (const C2)) : C1 = C2.

… suppose que C1 et C2 sont deux de ces choses purement abstraites. Il n’est pas permis d’écrire quelque chose comme « (…) = (…) » ou « |…| = |…| », ce qui exclut l’égalité entre termes et relations et une égalité comme « X = Y », suppose que X et Y ne sont pas des variables ordinaires, mais deux variables désignant seulement deux de ces choses purement abstraites.

Ça revient à définir des règles concernant les règles du langage, ce qui est encore une colle qu’il faudrait étudier. Quoique que plus qu’une règle sur les règles du langage, c’est une règle sur l’utilisation de la relation spéciale, « = ».
Profil
Administrateur
Avatar de l’utilisateur
Hibou a écrit : 
[…]

Ce n’est qu’une opinion personnelle, mais je crois qu’il faut définir ce qui est définissable et réduire au minimum ce qui ne l’est pas. Il ne faut invoquer la magie que quand il n’est pas possible de faire sans, une ressource si précieuse, s’utilise peu et discrètement.

[…]

Il faudrait d’ailleurs définir les règles de son invocation, même si c’est informellement, parce qu’on ne fait pas sortir un lapin d’une paire de chaussons, en prononçant des paroles au hasard ou juste en faisant n’importe quoi.
Profil
Administrateur
Avatar de l’utilisateur
Une utile relation sur les règles elles‑mêmes, serait si étant donné un ensemble de règles « (r1 A) : … » et un ensemble de règles « (r2 A) : … », savoir si (r2 A) est définie pour tous les A vérifiant (r1 A). Ce serait équivalent à, considérant r1 comme un type et r2 comme une fonction, vérifier si cette fonction r2 couvre tout son domaine r1.
Profil
Administrateur
Avatar de l’utilisateur
D’après leurs variables, pour les règles, quatre propriétés indépendantes ont été distinguées jusque maintenant. Une cinquième est ajoutée plus loin, après la liste des précédentes.

Le fait qu’une variable dans la tête de la règle, n’apparaît pas dans le corps de la règle (variable inutilisée).

Le fait qu’une variable dans le corps de la règle, n’apparaît pas dans la tête de la règle (variable non‑déterminée à l’instanciation de la règle, nécessitant une résolution).

Le fait qu’un variable dans le corps de la règle, apparaît dans plusieurs termes (intrication de termes par une variable) ou dans un seul terme.

Le fait qu’une variable apparaît seule dans un terme ou avec d’autres (intrication de variables par un terme).

Une cinquième peut être ajoutée, qui est le fait qu’une variable apparaît dans la tête de la règle, une seule fois ou plusieurs fois (égalité implicite entre des entrées). L’importance de cette propriété se discute, elle s’exprime en tous cas dans la formulation du langage, de deux manières différentes possibles, c’est alors un fait sémantique implicite.
Profil
Administrateur
Avatar de l’utilisateur
Hibou a écrit : 
[…]

(r A B) : (s A) & (t A).

Dans ce cas, la variable B ne pourra pas être indéterminée, elle le sera nécessairement par l’unification. Ce cas est potentiellement douteux (à vérifier quand‑même, il existe peut‑être des exemples justifiés de tels cas), mais la variable B n’étant pas indéterminée, la règle pourrait être vérifiée.

[…]

Précision manquée : la question se pose dans le cas d’une règle dont le corps n’est pas vide.
Profil
Administrateur
Avatar de l’utilisateur
Un mot pour l’idée de terme le plus externe.

L’idée de terme le plus externe a jusque maintenant toujours été définie par sa position et par opposition aux termes internes.

Ce n’est peut‑être pas un cadeau, mais peut‑être que le mot le plus approprié pour le terme le plus externe, est l’interprétation. Ce n’est peut‑être pas un cadeau, parce que la notion d’interprétation revient tellement souvent qu’il faudrait maintenant distinguer les interprétations.

Ça se lit bien : « (nat z). » dit que z est interprétable comme un nat. Interprétable comme, et non‑pas interprété comme, ce qui suggérerait que c’est sa seule interprétation possible. Potentiellement, une autre interprétation est toujours possible, mais en se plaçant dans un ensemble donné de règles, on peut éventuellement dire qu’il n’a qu’une interprétation.

Ça se lit bien récursivement aussi. Quand il a été dit que ce qui est une règle du point de vu du domaine client est un terme du point de vue du domaine du langage et que ce terme est incorporé dans un terme spécifique au domaine du langage. Ce terme dans lequel il est incorporé, désigne l’interprétation comme une règle, en même temps que du point de vue du domaine client, la tête d’une règle est une interprétation.

Une interprétation peut elle‑même être interprétée. En plus de l’exemple plus haut, un exemple précédent a déjà suggéré, celui de définir une règle sur des règles, pour vérifier si elles sont dans une relation qui a été comparée à un typage. Un autre exemple, mais plus délicat, est celui de la négation qui a été décrite comme sélectionnant une interprétation d’un terme.

Quand il a été dit que la composition verticale est comme une imbrication ou le placement dans un contexte, on peut alors dire qu’elle permet aussi de placer un terme dans une interprétation.

Le terme le plus externe étant appelé l’interprétation, il n’y a plus de raison d’hésiter à appeler la composition horizontale, une relation. Une interprétation est alors aussi une relation, ce qui se lit assez bien.
Profil
Administrateur
Avatar de l’utilisateur
Pour comprendre l’idée étrange d’interprétation d’une interprétation.

Quand une interprétation I1 est interprétée par une interprétation I2, I1 devient un terme, n’est plus interprétation. C’est d’ailleurs le fait qu’une interprétation soit représentée par un terme, et que l’interprétation s’applique à un terme, qui fait qu’une interprétation peut elle‑même être interprétée, mais devient alors un terme comme les autres.

Une règle du domaine client, définie une interprétation. Cette règle est un terme du domaine du langage. Si le domaine du langage établit une propriété de ce terme, par là, est établie une propriété de l’interprétation correspondante dans le domaine client. L’établissement d’une propriété, se comprend là, comme le fait qu’un terme vérifie une interprétation.
Profil
Administrateur
Avatar de l’utilisateur
Hibou a écrit : 
[…]

(letter a).
(letter b).
(letter c).
-- Etc.
(name (name1 L)) : (letter L).
(name (name2 L N)) : (letter L) & (name N).
(term (const N)) : (name N).

Ça semble aller de soi, si on veut coller aux conceptions habituelles, une constante est un mot, un mot est une suite de lettres, l’ordre des lettres est important pour l’égalité ou pas de deux suites de lettres.

Mais cette définition plus simple et même plus immédiate, est possible aussi :

(term (const C)).

Ce n’est pas tout à fait n’importe quoi, c’est C, qui peut être n’importe quoi, mais (const C) n’est pas n’importe quoi, par le fait de const, qui caractérise ce terme comme une constante, en supposant qu’aucune règle n’en fait une autre interprétation. Mais C, peut vraiment être n’importe quoi, l’égalité étant définie, c’est suffisant. C’est amusant et parfaitement abstrait.

[…]

Cette abstraction était une possible mauvaise idée.

Quand on un problème ne semble pas avoir de solution, on ne sait jamais si c’est qu’on manque d’imagination. Sans certitude, mais un argument semble convaincant : l’abstraction est une omission et ce qui est omis peut finir par manquer.
Profil
Administrateur
Avatar de l’utilisateur
Hibou a écrit : 
[…]

Le fait qu’un variable dans le corps de la règle, apparaît dans plusieurs termes (intrication de termes par une variable) ou dans un seul terme.

Le fait qu’une variable apparaît seule dans un terme ou avec d’autres (intrication de variables par un terme).

[…]

Il existe au moins une possibilité d’éliminer des intrications :

(r A A)
(r A B) & (eq A B).

Il n’y a pas d’intrication dans la première ligne, les deux variables et les deux termes sont intriqués dans la seconde ligne, qui est pourtant équivalente à la première. C’est peut‑être le seul cas de base à partir duquel il est possible de les éliminer ou il y en a peut‑être d’autres, aucune idée pour le moment.
Profil