An indexical is a reactive functional rule of the form
`X`` in `

`R`, where `R` is a set 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. When a propagating indexical fires, `R` is
evaluated in the current store `S`, which is extended by adding the
new domain constraint `X``::`

`S(R)` to the store, where
`S(R)` denotes the value of `R` in `S`. When a checking
indexical fires, it checks if `D(X,S)` is contained in `S(R)`,
and if so, the constraint corresponding to the indexical is detected as
entailed.

Send feedback on this subject.