An *indexical* is a reactive functional rule of the form

, where `X` in `R``R` is a finite domain valued *range
expression* (see below). See Syntax of Indexicals for a grammar
defining indexicals and range expressions.

Indexicals can play one of two roles: *propagating indexicals* are
used for constraint solving, and *checking indexicals* are used for
entailment checking.
Let `S(R)` denote the value of `R` in `S`.
When a propagating indexical fires, the current store `S` is
extended to `(X in S(R))(S)`. When a checking indexical fires, it
checks if `D(X,S)` is contained in `S(R)`, in which case the
constraint corresponding to the indexical is detected as entailed.

Send feedback on this subject.