Expressions

An expression is a kind of term that ranges over the state variables. For example we might write $x > y + 1$, when $x$ and $y$ are both state variables of type $\mathbb{Z}$. Although Isabelle/HOL already allows us to write terms, these range over logical variables, and not state variables, which are modelled using lenses. In order to use state variables, we introduce some special brackets $(E)_e$, where $E$ is a term that can range over both state and logical variables. This allows us to write expressions and assertion in an intuitive way. In the remainder, we justify this notation.

We model expressions as functions of type $S \Rightarrow V$, where $S$ is the store type and $V$ is the type of the expression. Typically in a shallow embedding, we can then model expressions using $\lambda$-terms of the form $\lambda s:S.\, P(s)$, where $P$ is some term that ranges over the state. When our state variables are modelled using lenses, we can use them to query the value of variables in a particular state using the $get$ function.

For example, the expression $x > y + 1$ can be modelled as $\lambda s.\, get_x\ s > get_y\ s + 1$. However, this representation is cluttered by the insertion of the $\textit{get}$ functions. Consequently, we have developed the $e$-bracket notation, which performs this lifting automatically. Intuitively, the brackets use the type system to distinguish whether a variable mentioned in a terms is a state or logical variable, and inserts $get$ when necessary. Thus, if $x$ and $y$ are both existing lenses, then we can simply write $(x > y + 1)_e$ for our example expression.