These structures are intended to allow one to talk about ‘all such objects as may be represented in a picture by arrows’, (Venema).
An arrow frame is a frame, , such that is a ternary relation, (so ), is a binary relation, and a unary one, so .
The interpretation intended for these relations is similar to the structure of a groupoid, but from a relational point of view.
For think , ‘the’ composite of and , but, of course, need not be uniquely defined by this;
For , think is a ‘reverse’ arrow for ;
For i.e. , think is an ‘identity arrow’.
This defines a frame by a relational signature. It does not specify any formulae to be satisfied, nor is there a valuation around to give some ‘meaning’ to the structure.
The arrow language follows the general form of the modal languages, but note that there are several ‘arities’ of relation in the structure, so we need several different types of modal operators.
The arrow language is defined by the rule
where the are the propositional variables, as usual, and in addition
is ‘identity’ and is a nullary modality or modal constant;
(an unfortunate notation, but which seems fairly standard in the sources used for this) is the ‘converse’ operator and is a ‘diamond’, i.e. a unary operator, and
is the ‘composition operator’ and is a dyadic operator.
The possible interpretations or readings of these include
is SKIP;
is conversely; and
is ‘first then ’.
The usual rules for modal semantics apply. An arrow model, , consists of an arrow frame, , (and a valuation , which plays a somewhat behind the scenes role in this general situation). In what follows, ,
if and only if ;
if and only if for some with ;
if and only if and for some with .
A general treatment of these ideas can be found in
whilst a short introduction is
Last revised on December 24, 2010 at 07:47:12. See the history of this page for a list of all contributions to it.