Crochet carré blanc droit mathématique

Il marque la limite droite des évaluations sémantiques et des multi-ensembles.

En sémantique formelle et en théorie des langages de programmation, la notation ⟦e⟧ représente le sens, la dénotation ou la valeur interprétée de l’expression syntaxique e. En notation Z, ⟦ ... ⟧ délimite un sac (un multi-ensemble). Ce symbole n'apparaît quasiment jamais hors du champ de la logique et de l'informatique théorique.

Typographiquement, ⟧ est un délimiteur mathématique étroit à double trait. Il se distingue nettement du signe de ponctuation large d'Asie orientale 〛 et bénéficie d'un espacement propre aux polices mathématiques.

D'où vient la convention ⟦ ⟧ ?

Les logiciens ont adopté les doubles crochets pour isoler la syntaxe du sens.

Au milieu des années 1960, le logicien Dana Scott a introduit les doubles crochets pour évaluer les formules de manière lisible lorsque celles-ci devenaient trop longues. Christopher Strachey et Scott ont ensuite ancré cet usage dans la sémantique dénotationnelle, avant qu'il ne gagne la linguistique formelle.

Cette convention sépare deux niveaux : à l'intérieur des crochets figure le texte formel brut ; l'ensemble avec crochets représente l'objet mathématique ou la valeur de vérité qui lui correspond.