Quantifier

Statut documentaire : reference — voir Maturité et preuves.

Les quantificateurs contrôlent la portée logique des variables et participants en H-Logic. Ils relèvent de la sémantique logique, pas de données de participants ordinaires, et ne remplacent pas des boucles applicatives.

Les formes usuelles distinguent notamment intention existentielle et universelle, par exemple :

exists y:#B on .:#R(x, y);
any x:#A, exists y:#B on .:#R(x, y);

Un quantificateur modifie ce qui doit ou peut être lié pour que l'énoncé soit vrai. Une taille de collection, une construction d'itération ou un foreach du langage hôte n'exprime pas la même sémantique.

Maintenez la syntaxe des quantificateurs alignée sur les formes acceptées par le parseur H-Logic courant et validées par les tests de raisonnement. Si une nouvelle forme n'est pas couverte par la grammaire/test actuelle, documentez-la comme planifiée plutôt que d'en déduire le support à partir de la notation logique générale.