Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Les logiques : notes en vrac
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Sam 20 Nov 2021 21:50
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

(dom (eq N1 N2)) : (name N1) & (name N2).
(dom (neq N1 N2)) : (name N1) & (name N2).

[…]

Les termes N1 et N2 sont indépendants, comme les paires (N1, N2) ne font pas toujours un terme (eq N1 N2) unifiable avec une tête de règle et idem avec neq. Il avait été dit, que c’est une conséquence du fait que l’unification avec la tête de la règle, est une partie de sa vérification et que eq et neq partitionnent l’ensemble des paires (N1, N2).

Comment représenter la même idée de domaine, mais dans l’autre sens, c’est à dire exprimer que l’ensemble des paires (N1, N2) est couvert par eq et neq, ensemble ? Une première mais mauvaise idée de notation pourrait être celle ci‑dessous, où faute d’idée de nom, le nom x est utilisé :

(x (eq N1 N2) (neq N1 N2)) : (name N1) & (name N2).

C’est une idée de domaine qui est exprimée par cette notation, pas encore l’idée de partition, comme ça ne garantirait pas que les interprétations eq et neq soient mutuellement exclusives (ça pourrait ne pas être le cas, avec d’autres exemples).

Un problème léger avec cette notation, est qu’en plus du nom manquant, il se pose un problème d’arité non‑fixe. Avec dom, précédemment proposée, l’argument est une interprétation, une seule. Avec ce x, le nombre d’arguments peut être variable (au moins un quand‑même). Mais est‑ce vraiment un problème ? Une problème plus gênant, est que l’ordre (eq N1 N2) (neq N1 N2) semble important en apparence, alors qu’il ne l’est pas. L’exemple plus haut, devrait autant pouvoir se lire comme s’il avait été écrit ainsi :

(x (neq N1 N2) (eq N1 N2)) : (name N1) & (name N2).

C’est plus un brai problème que la question de l’arité.

Un autre problème, est que cette notation rend mal l’idée que c’est la paire (N1, N2), qui est couverte par eq et neq ensemble. Cette autre notation, le rendrait mieux :

(x (name N1) (name N2)) : (eq N1 N2).
(x (name N1) (name N2)) : (neq N1 N2).

Le problème de l’arité se pose toujours (déplacé sur d’autres termes), mais il n’y a plus de problème d’ordre semblant important sans l’être. L’ordre des deux termes serait effectivement important, même si dans le cas de cet exemple en particulier, il ne le serait pas, comme (eq N1 N2) et (eq N2 N1) ont la même conclusion et idem avec neq. Comme plus haut, ça n’exprimerait pas une quelconque partition, seulement une couverture, celle de la paire (N1, N2) par deux interprétations (deux pour cette exemple, mais pas nécessairement toujours) ; l’alternative pourrait autant être un ou‑inclusif qu’un ou‑exclusif.

La première option (celle à une seule règle) n’a été présentée que pour être exclue, mais après avoir été envisagée, pas pour ne pas l’avoir été. Seule la seconde option est à retenir.

L’intérêt de cette notation serait le même qu’avec dom : une description, un test de salubrité est éventuellement un fait vérifié, pouvant être utilisé dans des démonstrations. Aussi, cette notation compléterait la précédente, celle de dom.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Lun 22 Nov 2021 17:54
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

(dom (eq N1 N2)) : (name N1) & (name N2).
(dom (neq N1 N2)) : (name N1) & (name N2).

[…]

Cette notation n’est pas correcte, quelque chose a été perdu en chemin.

N1 et N2 sont sensés être mutuellement indépendants, le sont dans la conjonction, mais pas dans la tête de la règle. Si on lit « A : B » comme « B implique A », alors il faudrait pouvoir lire « (name N1) & (name N2) implique que (eq N1 N2) est unifiable avec une tête de règle », ce qui n’est pas le cas, du moins pas toujours. C’est là qu’une chose a été perdue en chemin.

L’idée d’origine était plus proche de ceci :

(dom (eq N ?)) : (name N).
(dom (eq ? N)) : (name N).

Et idem pour neq.

Le point d’interrogation, à remplacer par un autre symbole, se lirait comme « on ne se préoccupe pas de ce terme ». Cette fois, la lecture est correcte : « (name N) implique que (eq N ?) est unifiable avec une tête de règle », idem pour (eq ? N).

Les deux termes étant décrits indépendamment l’un de l’autre, il y a deux domaines : celui du premier terme et celui du second terme, qui ici, se trouvent être les mêmes.

Une question laissée en suspend, était celle de trouver un symbole autre que « ? », pour signifier un terme dont ne se préoccupe pas. Il avait été noté que le symbole ISO Prolog « _ », qui aurait put correspondre, n’est pas naturel et peu lisible.

Je n’ai pas put trouver mieux que quatre symboles candidats dans Unicode. Si d’autres bons candidats existent, je les ai manqué, mais je crois que cette notion étant peu courante, surtout dans les langues naturelles, qu’il n’y en a effectivement pas d’autres, et les quatre candidats ne sont d’ailleurs pas issus de scripts pour des langues naturelles.

Les quatre, dont un seul sera conservé :

  • U+2370, nommé APL FUNCTIONAL SYMBOL QUAD QUESTION, un carré englobant un point d’interrogation.
  • U+2BD1, nommé UNCERTAINTY SIGN, un losange englobant un point d’interrogation.
  • U+FFFC, nommé OBJECT REPLACEMENT CHARACTER, un rectangle en pointillé englobant les trois lettres « OBJ ».
  • U+FFFD, nommé, REPLACEMENT CHARACTER, un losange plein, noir englobant un point d’interrogation blanc.

U+FFFC pourrait convenir, mais ce caractères semble plus être un caractère de contrôle qu’un symbole destiné à être affiché.

U+FFFD serait trop ambiguë, c’est le symbole utilisé pour représenter un caractère mal encodé dans un fichier.

U+28B1 pose deux problèmes. Son nom ne suggère pas la signification attendue. La signification attendue tourne plutôt autour de l’idée de “ placeholder ” ou de variable que de “ uncertainty ”. De plus, son aspect est trop proche du symbole U+FFFD, lui‑même inapproprié.

Seul U+2370 reste comme seul bon candidat. Comme ce symbole n’est pas courant, il sera le plus probablement non‑affiché avec la plupart des navigateurs, et alors le symbole composé [?] sera utilisé à la place dans ce sujet.

Aucun symbole convenable n’a été trouvé, correspondant à la notion de variable ou de placeholder ou de blank. Faute de mieux, un symbole reposant sur un point d’interrogation sera assez lisible, mais imparfait, comme le point d’interrogation peut suggérer quelque chose à résoudre. Un carré blanc serait‑il préférable ? Ou mieux, un x dans un carré ?

La notation serait pour l’instant, ainsi :

(dom (eq N [?])) : (name N).
(dom (eq [?] N)) : (name N).
(dom (neq N [?])) : (name N).
(dom (neq [?] N)) : (name N).

Où [?] serait en fait le symbole U+2370.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Lun 22 Nov 2021 18:23
Message Re: Les logiques : notes en vrac
Pour le choix d’un symbol posé dans le précédent message, deux autres options, en cherchant un symbole représentant un joker, une idée qui correspondrait bien au sens attendu, plus encore qu’un point d’interrogation, qui pose problème :

  • U+1F0BF, nommé PLAYING CARD RED JOKER, une carte à jouer avec une tête de joker (pas celui de Batman).
  • U+1F0CF, nommé PLAYING CARD BLACK JOKER, une carte à jouer sur laquelle figure une étoile.

Le premier est trop graphique est alors peu lisible à la taille d’un caractère ordinaire. Le second est plus sobre et assez lisible, l’étoile étant un symbole assez répandu pour représenter un joker, mais parfois aussi pour représenter un champ obligatoire. Disons que le rectangle lèvera l’ambiguïté et évoquera bien un joker.

Malheureusement, le symbole U+1F0CF n’est pas supporté par le forum, et alors le symbole composé [*] devrait y être utilisé à la place. Ce symbole U+1F0CF, me semble personnellement au moins, moins ambiguë qu’un symbole reposant sur un point d’interrogation :

(dom (eq N [*])) : (name N).
(dom (eq [*] N)) : (name N).
(dom (neq N [*])) : (name N).
(dom (neq [*] N)) : (name N).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Lun 22 Nov 2021 19:18
Message Re: Les logiques : notes en vrac
Le domaine d’une interprétation, est lui‑même une interprétation, comme le montre la notation du message précédent. Ça signifie qu’une interprétation pour laquelle un domaine est défini, peut elle‑même faire partie du domaine d’une autre interprétation.

Ces domaines ne correspondent pas à des types au sens courant dans les langages informatiques, ils peuvent être moins rigides, ce qui ne signifie pas qu’il soit possible de poser n’importe quoi, autant qu’ils peuvent être plus restrictifs.

Des règles sur des règles, ne sont pas des choses à résoudre, mais des choses à vérifier à priori, une seule fois à l’instantiation du langage. Comme précédemment expliqué, il y a le langage avec ses règles sémantiques, il y a les applications du langage qui définissent leurs propres règles en termes de cette sémantique, une instantiation du langage est le langage avec ses règles sémantiques et les règles d’une application du langage.

Quand « (dom (eq N [*])) : (name N). » est écrit, il faut le comprendre comme une règle devant être vérifiée, pour que l’instantiation du langage soit réalisée. Cette vérification est à comprendre comme nécessaire, elle pose un fait sur l’interprétation eq, et ce fait doit être nécessairement vérifié, parce qu’une fois posé, il devient une condition que eq doit effectivement vérifier. Dans le cas contraire, on poserait un fait qui ne serait peut‑être pas, ce qui ne serait pas correcte, parce que ce qui serait écrit, pourrait ne pas être digne de confiance.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 23 Nov 2021 00:04
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

(x (name N1) (name N2)) : (eq N1 N2).
(x (name N1) (name N2)) : (neq N1 N2).

[…]

Cette notation peut sembler convenir, mais finalement non. Si on lit encore « A : B » comme « B implique A », en notant que A peut être sans que B ne soit, c’est à dire que A couvre potentiellement plus que B, alors la notation rend bien la couverture, mais l’implication n’est pas correcte. En effet, (eq N1 N2) est sensée être compris comme un terme simplement unifiable avec une tête de règle, pas plus, alors qu’il apparaît comme une condition à vérifier, totalement, et idem pour (neq N1 N2).

Ce problème d’interprétation n’est pas absent de la notation dom, non‑plus. Avec cet exemple donné :

(dom (eq N [*])) : (name N).

La sémantique normale des règles, n’est pas respectée, comme en plus de l’unification normale avec la tête de la règle, une seconde condition implicite est sensée être vérifiée, celle que (eq N [*]) est unifiable avec une tête de règle. Mais dans le cas de cet exemple, ce n’est pas tellement un problème. En imaginant que la possible unification avec une tête de règle soit vérifiée par une interprétation spécifique, disons uni, alors cette condition implicite pourrait être rendue implicite, ainsi :

(dom (eq N [*])) : (name N) & (uni (eq N [*])).

Cette condition implicite étant censée faire partie de l’interprétation dom, il serait possible de définir dom comme posant cette condition implicite et de la laisser implicite (obliger à la noter explicitement serait difficile acceptable et n’aurait pas d’intérêt). Disons que dom ne serait pas définie comme une règle ordinaire, c’est à dire pas comme une règle définie par une application du langage, mais serait définie par le langage et il ne pourrait pas en être autrement.

Appliquer le même principe à l’interprétation qui n’a pas encore de nom, x, n’est pas évident et expose d’autres problèmes supplémentaires, non‑exposés ici, pour ne pas endormir avec des choses inutiles.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 23 Nov 2021 00:24
Message Re: Les logiques : notes en vrac
Le nom, uni, pour une interprétation qui vérifie qu’un terme est unifiable à une tête de règle, n’est pas idéal. Ce nom est trompeur, parce qu’il peut facilement évoquer l’unification en général. Si on lit « A : B » comme « Avec B, on peut produire A », alors la règle peut se lire comme une fonction dont B est le domaine et A est le range. Le mot Anglais est utilisé, parce que la terminologie Anglaise fait une distinction utile, entre codomain et range. En Anglais, range est l’ensemble effectivement produit par une fonction, tandis que codomain est potentiellement plus large que range. On a range inclus dans ou égale à codomain. C’est là qu’est la distinction intéressante : les A effectivement produits, font partie du range de la règle vue comme une fonction, mais un terme simplement unifiable à A, qui ne vérifierait peut‑être pas la règle, ne ferait peut‑être pas partie de son range, cependant, pourrait être une définition d’un des possibles codomains.

Ceci donne l’idée d’appeler codom (abréviation de codomain), l’interprétation qui vérifie qu’un terme est unifiable à une tête de règle, et donc peut potentiellement vérifier une règle, cependant sans garantie qu’il la vérifie.

La notation (codom A) se lirait comme « A fait partie du codomain de l’ensemble des règles » et en pratique, comme « A est unifiable à au moins une tête des règles définies ».

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 23 Nov 2021 10:52
Message Re: Les logiques : notes en vrac
L’idée du précédent message est correcte, mais alambiquée et ne se lirait pas facilement. L’idée de codomaine, telle que décrite, n’est pas autant courante que l’idée de domaine, et en plus, justifier ce nom par une analogie entre règle et fonction, pourrait participer en rendre moins claire l’idée de règle, qui nécessite encore des clarifications.

Parler d’applicabilité d’un terme, serait peut‑être plus parlant. En supposant qu’il est compris qu’avant d’être vérifié par une règle, un terme doit être unifiable avec la tête de cette règle, parler de l’applicabilité d’un terme pour parler de cette condition, s’explique bien et plus directement.

En utilisant le mot app, comme abbreviation de applicable, la notation serait par exemple (app A), qui se lirait comme « le terme A est applicable », c’est à dire, « le terme A est unifiable à une tête de règle ».

La notation :

(dom (eq N [*])) : (name N).

Signifierait implicitement :

(dom (eq N [*])) : (name N) & (app (eq N [*])).

Pourtant, l’idée du nom codom, ferait apparaître une relation intéressante :

(dom (eq N [*])) : (name N) & (codom (eq N [*])).

Ce précédent choix de nom, ferait apparaître que le domaine d’une interprétation est ce qui assure qu’elle fait partie du codomaine des règles ou qu’elle a bien un codomaine.

La question a une possible seconde réponse, mais n’est toujours pas résolue. Pour dire qu’un terme est unifiable à une tête de règle, est‑il préférable de parler d’applicabilité ou de codomaine ? Le premier mot me semble plus directement compréhensible, le second mot fait ressortir une relation intéressante mais nécessite plus d’explications pour être compréhensible.

En marge, cette notion n’est pas artificielle, elle est implicite dans la sémantique du langage. Il se trouve qu’elle doit pouvoir être écrite explicitement, pour pouvoir définir explicitement ce que couvre une interprétation, une couverture appelée le domaine de l’interprétation, ce qui était l’objet des précédents messages.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 23 Nov 2021 12:06
Message Re: Les logiques : notes en vrac
Pour une explication des notions de domain, codomain et range, voir ce document : Domain, Range and Codomain (mathsisfun.com). Voir en particulier l’illustration avec l’exemple d’une fonction de x vers 2x + 1.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 23 Nov 2021 19:48
Message Re: Les logiques : notes en vrac
Que la notation (app A) ou (codom A) soit finalement choisie, ce qui suit est en supposant que le choix fait, serait celui de la notation (codom A).

À sa lecture, le nom codom serait inévitablement mis en rapport avec le nom dom et il faudrait alors s’assurer que la relation entre les deux est bien celle qui pourrait être implicitement supposée. Elle semble l’être et ce message l’explique.

Il a été dit que « A : B. » peut être lue comme une fonction où B est le domain, l’ensemble des solutions A, le range et les termes unifiables avec A, un codomain (il peut y en avoir plusieurs, en principe) de la règle, et même le seul, puisqu’aucun autre n’est prévu pour le moment au moins.

Si un terme T est unifiable avec A, on le note (codom T). Si un terme U vérifie « A : B. », il fait parti du range de la règle vu comme une fonction. Comme la vérification de la règle par le terme U, nécessite que U soit unifiable avec A, on peut noter que si U est vérifié, alors cela implique (codom U) (l’implication réciproque n’est pas valide, parce que pas toujours valide).

Il a été dit que cette notation, avec une condition implicite :

(dom (eq N [*])) : (name N).

Se comprendrait comme celle‑ci, avec une condition explicite :

(dom (eq N [*])) : (name N) & (codom (eq N [*])).

(name N) est un terme qu’on suppose vérifié, comme la règle est supposée être vérifiée. D’après les explications plus haut, on peut comprendre que (name N), vérifié, implique (codom (name N)). Cette remarque rend moins surprenante le présence de (codom (eq N [*])) dans la notation avec une condition explicite.

Il a été dit que le domaine d’une interprétation est lui‑même défini par une interprétation, que alors l’interprétation dont le domaine est défini, peut elle même participer à la définition du domaine d’une autre interprétation. Si cette relation est comprise, alors la présence de termes représentant un codomain, dans une conjonction représentant un domain, ne surprend pas excessivement, comme ça explique que la chaîne soit possible.

Ça ne surprend pas trop, ça peut aussi s’expliquer plus explicitement. Comme dit précédemment, la conjonction du corps d’une règle, peut être vue comme un domain ; ors, pour vérifier cette conjonction, il faut vérifier tous ses termes, et chaque terme, pour être vérifié, nécessite d’être au minimum dans le codomain de l’ensemble des règles, c’est à dire dans celui d’au moins une règle.

Précédemment, il a été dit qu’une interprétation peut être le domaine d’une autre interprétation. Une interprétation vérifiée, est un terme vérifié, ce qui signifie là aussi, que le terme qui la représente est un codomain.

En résumé : le domaine d’une interprétation, est défini par une ou des interprétations, et ce même domaine d’une interprétation implique un ou plusieurs codomain(s) implicites, impliqués par la vérification des termes qui définissent le domaine. Interprétation, domain et codomain, sont liés. La notion de range se cache dans le langage aussi, mais sans être nommée (parce que ça n’aurait pas d’utilité), elle existe comme l’ensemble des solutions à un terme.

Dans la notation discutée, il existe une seconde lecture de la notion de domaine. En reprenant cette notation :

(dom (eq N [*])) : (name N).

Dans cet exemple, (name N) est le domaine de (eq N [*]) (ce qui n’est pas le domaine de (eq N1 N2)) autant qu’une définition du domaine du premier terme de eq, désigné par N. Le domaine du terme se comprenant comme l’ensemble des termes pouvant se trouver à cette place. Parler du domaine d’une interprétation, c’est aussi parler du domaine des termes qui la constituent.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 23 Nov 2021 20:04
Message Re: Les logiques : notes en vrac
Il faudrait trouver un autre nom que dom. Le domaine dont il est question dans le précédent message et d’autres précédents, est plus large que le domaine au sens strict. Ce qu’il faudrait, c’est un mot qui soit à domain, ce que codomain est à range.

La raison pour laquelle le domaine dont il est question, est plus large que le domaine au sens stricte, est celle‑ci : il s’agit de conditions assurant l’unification avec des têtes de règles, ce qui est une condition en général plus faible que la vérification de ces règles.

Un tel mot pourrait‑il être corange ? Ce mot est imaginé par analogie, par symétrie.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
cron