A state is an assignment of values to variables. More precisely, a state 
is a
family of mappings 
. Given a variable x of type s,
we write 
instead of 
. The canonical extension of to
a map from terms to values is also denoted by . (In functional programming terminology
this extension is often called eval 
.)
Given state , variable v and value M we let
denote the ``new'' state 
with 
, and 
for
every 
. Observe that for any state , terms t,r and variable v :
Unfortunately, it turns out that any sufficiently rich model of computation will allow
calculations that never terminate. We therefore include a pseudo-state 
, pronounced
``bottom'' or ``undefined''. A nonterminating computation is then said to return .