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
Ven 12 Nov 2021 06:14
Message Re: Les logiques : notes en vrac
Une distinction précédemment faite, à noter à part : il y a deux genres d’abstraction, que sont les abstractions en aval et les abstraction en amont. Ce sont les abstractions en amont, qui peuvent être source de difficultés.

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
Ven 12 Nov 2021 06:34
Message Re: Les logiques : notes en vrac
Jusqu’ici, une règle peut être dans trois cas possibles, par rapport à un terme.

Conditionnée par le terme. C’est le cas où une règle doit vérifier une base de faits, pour que la règle soit considérée comme correcte. Ce cas n’est pas nécessaire, il l’est ou pas selon l’approche du domaine.

Justifiée par le terme. C’est le cas dans la preuve de satisfiabilité. Ce cas peut être explicite ou implicite (preuve générée automatiquement) mais est toujours nécessaire pour garantir que la règle a du sens. La preuve qu’un règle admet au moins un terme ne la vérifiant pas, pourrait être considérée de la même manière.

Conditionnant le terme. C’est le cas où un terme est vérifié par une règle. C’est le cas de loin le plus fréquent. Ce cas se distingue des deux précédents, en ce qu’une non‑vérification n’est pas nécessairement une erreur.

Pour le premier et le troisième cas, la relation entre la règle et le terme, est inversée par rapport à l’autre cas (conditionnée vs conditionnante).

Le cas où une règle est considérée comme un terme, est à part, ce n’est pas une relation entre règle et terme. Il est à noter à côté des trois précédents cas quand‑même.

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
Ven 12 Nov 2021 20:47
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Le message précédent peut suggérer de remonter encore plus en amont, qu’il existe un langage plus basique que celui envisagé jusqu’ici : celui qui ne permet de poser que des interprétations sur des constantes.

Ce langage ne peut pas se définir lui‑même, justement parce qu’il ne permet que de vérifier si un terme constant fait parti d’un ensemble de faits constants déjà notés. […]

Dans cas, il faut peut‑être plus parler de notation, que de langage.

Hibou a écrit : 
[…]

La relation est ce que les choses sont pour elles‑mêmes (même si c’est plus exactement, telle qu’on les comprend), l’interprétation, c’est ce qu’elle sont pour soi ou pour un domaine. Un mot du langage courant, convenant aussi bien pour l’interprétation, c’est le role.

[…]

Parler de catégorisation, pourrait convenir parfois aussi.

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
Dim 14 Nov 2021 22:57
Message Re: Les logiques : notes en vrac
C’est l’interprétation, qui fait une variable.

Il a été dit que le langage de base initial, ne vérifiera que des termes constants. Ça peut sembler étrange : si le langage de base peut interpréter sa propre définition, qui utilise des variables, comme cela peut‑être être possible avec un langage qui né vérifie que des termes constants ?

La représentation interne précédemment décrite pour les variable, un terme de la forme (var N) ou N est l’identité de la variable, est un terme constant. En fait, toute écriture est toujours un terme constant. Il n’y a plus de mystère quand on sait que (var N) est sujet à une interprétation spécifique, et que c’est cette interprétation qui en fait une variable. Ceci dit, les requêtes ne pourront pas contenir de ces termes représentant une variable ou pas sans renvoyer une status « indéterminé ».

À noter : une écriture est toujours en elle‑même un terme constant.

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 15 Nov 2021 09:56
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

La relation est ce que les choses sont pour elles‑mêmes (même si c’est plus exactement, telle qu’on les comprend), l’interprétation, c’est ce qu’elle sont pour soi ou pour un domaine. Un mot du langage courant, convenant aussi bien pour l’interprétation, c’est le role.

[…]

Cette vision de l’interprétation par rapport à une relation, semble suggérer que l’équivalence est une forme d’interprétation. Il y aurait alors deux genres d’interprétation. L’équivalence telle qu’elle a été grossièrement définie, se réfère elle‑même à une interprétation, alors peut‑être serait‑elle une interprétation d’une interprétation. Dans ce cas, peut‑être un lien est‑il à chercher entre application d’une règle à une règle et équivalence. À moins que l’équivalence ne soit plutôt à définir sur les relations plutôt sur sur les interprétations … ou sur les deux ?

Ça fait beaucoup de questions, donc à clarifier.

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 15 Nov 2021 22:05
Message Re: Les logiques : notes en vrac
Une petite correction au message précédent, mais qui n’y change finalement rien.

L’équivalence avait été introduite sur les relations, pas sur les interprétations. Cet exemple pratique avait été posé :

Hibou a écrit : 
[…]

(equiv (cons A (cons B R)) (cons B (cons A R))) : (list R).
-- La notion de list est supposée préalablement définie.

Comment utiliser cette règle jusqu’à prouver qu’une règle peut être tentée avant une autre, malgré l’ordre dans lequel les règles sont écrites, est laissé à plus tard.

La non‑pertinence des duplications, pourrait être représentée d’une manière proche :

(equiv (cons A (cons A R)) (cons A R)) : (list R).
-- Dans un contexte où les permutations sont équivalentes.

Au lieu de cons, le constante pourrait être une autre […]


L’équivalence serait alors plus une forme d’interprétation, directement. Pourtant, sans raison pour le moment, de penser que l’équivalence ne s’applique jamais à une interprétation, les interrogations plus générales du message précédent (pas celui cité), restent les questions à se poser.

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 16 Nov 2021 23:38
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

L’égalité de deux constantes, ou plutôt de l’identité de deux constantes (même représentation pour l’identité d’une variable), se défini ainsi, avec cette représentation :

(eq () ()).
(eq (N1) (N2)) : (eq N1 N2).

La différence :

(neq (N) ()).
(neq () (N)).
(neq (N1) (N2)) : (neq N1 N2).

L’interprétation vérifiant qu’un terme est une représentation de l’identité d’une constante, ce qui correspond à ce que représente son nom :

(name ()).
(name (N)) : (name N).

[…]

Ni les règles de eq ni les règles de neq, ne mentionnent une condition du genre (name N). Les règles de name y sont implicites. Elles sont implicites dans les décompositions que font eq et neq. On pourrait alors se demander à quoi servent les deux règles de name. L’interprétation name peut être vue comme descriptive, par exemple s’il est dit quelque part, que le terme auquel s’applique eq ou neq, est un terme interprétable comme un name. Pourtant ce n’est pas dit explicitement, et même si ça l’était par une note ou un commentaire, ça resterait informelle. C’est une des raisons pour lesquelles pouvoir vérifier que des règles correspondent à des règles, pourrait être utile. Par exemple ici, une vérification serait que tout terme interprétable comme name, est unifiable à une des têtes des règles de eq et neq, c’est à dire que si (name T1) et (name T2) est vérifié, alors il doit exister une unification avec une tête de règle, pour (eq T1 T2) et (neq T1 T2), mais sans garantie de vérification. C’est cette idée qui a précédemment fait comparer certaines interprétations à des types. Ici, l’interprétation name est comme un type et autant eq que neq sont censées s’appliquer à ce type. On peut remarquer que cette notion distingue nettement interprétation et terme interne (ici aussi appelée relation), comme le terme T est comme extrait de name ou être placé dans eq ou neq.

Ça ne permet pas de rendre les choses plus vraies, mais ça peut les rendre plus dignes de confiance, une sorte de test de salubrité. Ce qui est sûr quand‑même, c’est que ça rend les choses plus lisibles, d’où l’idée de dire que name est descriptive.

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
Mer 17 Nov 2021 23:01
Message Re: Les logiques : notes en vrac
Correction d’une erreur dans le précédent message.

Si on a (name N1) et (name N2), l’unification de (eq N1 N2) n’est pas nécessairement possible, c’est celle de (eq N1 N2) ou de (neq N1 N2), qui l’est. Ce qui aurait dut être dit, serait plutôt que si on a (name N), alors (eq N ?) et (eq ? N) et (neq N ?) et (neq ? N), sont unifiables, le point d’interrogation représentant quelque chose dont on ne se préoccupe pas.

Le type ne peut pas porter sur le produit des deux arguments, comme l’unification participe à la vérification, qui peut ne pas être possible. Cela fait une différence importante avec la notion la plus courante des types, qui étant donné le type d’un argument, permettrait d’avoir un type pour le produit des deux. Ce que dit intuitivement le paragraphe précédent, c’est que ce pseudo type, s’appliquerait à chacun des deux arguments, individuellement.

Comme ça ne correspond pas tout à fait à la notion de type la plus couramment utilisée, mieux vaudrait ne pas utiliser ce mot. Parler de couverture serait approprié et moins trompeur.

Une notation fictive pour poser cette couverture à vérifier, pourrait être :

(coverage (eq name name))
(coverage (neq name name))

Ce serait un exemple de règles appliqués à des règles. Cette notation nécessiterait que la constante caractérisant une interprétation soit toujours la première constante d’un terme, sinon la notation n’a pas de sens. Elle se lirait ainsi : l’interprétation eq a un premier argument couvrant name et un second argument couvrant name, idem pour neq.

La couverture ne peut pas porter sur le produit des deux arguments, parce que l’unification est une partie de la vérification de la règle. Mais les deux interprétations eq et neq, ensemble, couvrent bien le produit des deux arguments, et d’ailleurs elles partitionnent ces produits. Par rapport au produit des deux arguments, chacune des deux interprétations couvre moins que le produit et plus qu’elle ne vérifie.

Si ce message ne semble pas totalement clair, c’est normal, mais intuitivement, il peut se comprendre et c’est suffisant pour ce qu’il veut dire.

Comme dit précédemment, cette notation ne participerait pas à la définition des interprétations, seulement à leur description. Elle dirait à quoi s’applique une interprétation, d’une manière immédiatement lisible et la vérification de cette couverture serait aussi un test de salubrité, dans le sens où si elle n’est pas vérifiée, alors il y une erreur dans les règles définissant l’interprétation ou dans l’idée qu’on s’en fait. Ce qui justifie cette notation, c’est que certaines conditions qui pourraient apparaître dans les règles, mais y étant redondantes, elles n’y sont pas écrite et par là, peuvent manquer, mais seulement pour la lecture, pas pour la définition. D’où l’idée de permettre d’écrire ces conditions dans une description d’une interprétation, plutôt que dans sa définition où elle n’a pas une bonne place.

Ce concept ne ferait pas partie du langage de base.

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
Jeu 18 Nov 2021 09:50
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Une notation fictive pour poser cette couverture à vérifier, pourrait être :

(coverage (eq name name))
(coverage (neq name name))

[…] Ce qui justifie cette notation, c’est que certaines conditions qui pourraient apparaître dans les règles, mais y étant redondantes, elles n’y sont pas écrite et par là, peuvent manquer, mais seulement pour la lecture, pas pour la définition. D’où l’idée de permettre d’écrire ces conditions dans une description d’une interprétation, plutôt que dans sa définition où elle n’a pas une bonne place.

[…]

Une autre notation serait plus appropriée :

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

Elle aurait ces avantages :

Elle représente directement l’intention, qui est de rapporter dans une description, une condition qui n’est pas écrite dans les règles. C’est moins concis, mais ça reste lisible et en tous cas autant lisible que n’importe quelles autres règles.

Dans le cas où la condition implicite porte sur plusieurs termes, cette notation permet de le dire, la notation précédemment proposée ne le permettait pas.

Cette notation n’est pas plus sensible à la position de la constante caractérisant une interprétation, que ne l’est une règle ordinaire, même s’il reste préférable de toujours l’écrire au début du terme.

Cette notation ressemble simplement plus à une règle, qui faciliterait la définition de sa sémantique.

Note : la constante coverage pourrait peut‑être aussi s’appeler dom, pour domain, ce qui serait plus concis est évoquerait la même chose, surtout avec la nouvelle notation :

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

Ce serait même plus clair, l’idée de domaine évoquant mieux l’idée de couverture exacte, tandis que coverage pourrait être mal compris comme signifiant une couverture minimale, c’est à dire pouvant être plus large. C’est probablement la notation qui sera retenue ; en rappelant que ce concept ne ferait pas parti du langage de base, seulement d’une définition ultérieure.

Il a été dit que ces cas de règles sur des règles ne participeraient pas aux définitions, seraient des descriptions et des tests de salubrité. Pourtant, elles pourraient servir dans des démonstrations. En effet, cette description, si vérifiée, pourrait permettre de conclure que si N ne vérifie pas (name N), alors N ne peut pas vérifier (eq 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
Jeu 18 Nov 2021 10:24
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…] Ce qui aurait dut être dit, serait plutôt que si on a (name N), alors (eq N ?) et (eq ? N) et (neq N ?) et (neq ? N), sont unifiables, le point d’interrogation représentant quelque chose dont on ne se préoccupe pas.

[…]

Il faudrait une notation pour ça. Le point d’interrogation a déjà un usage pour les requête et son usage courant le place mal au milieu d’un terme. ISO Prolog utilise le blanc souligné, mais cette notation n’est pas naturelle et peu lisible.

Image
Hibou57

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