# Term and Attribute Language

Summary. This note focuses on some of the design elements of the term language, and acts as a precursor to adding typing capability to terms and attributes of the core policy language. It explores some of the dimensions in which terms and conditions are extensible, e.g. to facilitate the addition of more domain-specific operations.

For concrete examples of attributed terms in the intermediate format, see the separate test vectors document.

## Extending conditions

Recall the grammar up to the language of conditions

data Const = Subj | Obj | Act
data Term = Entity String | Attr Term String | Keyword Const
data BinPred = Equ | Lt | Lte | Gte -- add more as required
data Cond = BinRel BinPred Term Term | T | Not Cond
| And Cond Cond | Or Cond Cond

Presently, our intermediate language of conditions Cond supports binary relations, which is a binary predicate symbol followed by its two terms – for now, we have the (in)equality predicate symbols captured by the data type BinPred. Of course, this can be extended with more binary predicate symbols as the need arises, by extending BinPred.

To motivate the rest of the discussion, recall the $\mathtt{grant\:if}$ rule policy from the yellow paper, which consists of a conjunction of the following conditions

\begin{align} \mathbf{object} &= vehicle \\ \mathbf{subject} &= vehicle.owner.daughter \\ \mathbf{action} &= drive\text{-}vehicle \\ true &= owner.daughter.is\text{-}insured \\ 0900 &\leq local\text{-}time(vehicle.location) \\ 2000 &\geq local\text{-}time(vehicle.location) \end{align}

Note that the last two conditions take a slight departure from the paper example, in that $local\text{-}time$ appears to be a function taking a “location” as parameter.

Using the syntactic sugar defined in the revisions document (in particular, =*= for BinRel Equ, <@> for Attr and respectively subject, object, action for Keyword Subj, Keyword Obj, Keyword Act), we can express the first three conditions in the abstract syntax

object  =*= Entity "vehicle"
subject =*= Entity "vehicle" <@> "owner" <@> "daughter"
action  =*= Entity "drive-vehicle"

The others are worth some discussion. The fourth condition may again be expressed as an equality =*= of terms, at least if we presuppose $true$ as e.g. a constant term – but perhaps it would be tidier to reserve Const for key-words (i.e. $\mathbf{subject}$, $\mathbf{object}$, $\mathbf{action}$), and instead enrich the language of conditions to support relations of other arities. Assuming this is possible, we can introduce a predicate symbol $\mathtt{isTrue}$, so that the fourth condition can be equivalently written

$$\mathtt{isTrue}(owner.daughter.is\text{-}insured)$$

To this end, we add a constructor UnRel of unary relations in our language of conditions.

data Cond = ... -- as above
| UnRel UnPred Term

A unary relation is a unary predicate symbol UnPred followed by its term. Examples include IsTrue as in the above example.

data UnPred = IsTrue | IsNull -- etc.

In the abstract syntax, the fourth condition thus becomes

UnRel IsTrue (Entity "owner" <@> "daughter" <@> "is-insured")

For the last two conditions involving $local\text{-}time$, see the next section for one approach.

Following a similar approach, one can just as easily add support for ternary (or higher arity) relations as required. As mentioned above, we postpone the discussion of how one should type (and interpret) such operation symbols to later. The intention now is simply to lay the groundwork.

## Composite terms

It also appears important for our language to be flexible enough to support function symbols on terms (this was also proposed by Michael in a much earlier draft of the core language). For example, given two (numerical) terms $t_1$ and $t_2$, we may want to express their “sum” $t_1 + t_2$ as a term. Or given a term we may want to express its SHA-hash. For this we can adopt a similar approach to the above, adding operation symbols over terms, e.g.

data UnOp = Negative | Length | Hash | LocalTime -- ...
data BinOp = Add -- ...

Again, higher arity operations can be added in the same way. Now we introduce a data type for composite terms, which are terms built from these operations.

data CompTerm = Simple Term
| UnTerm UnOp CompTerm
| BinTerm BinOp CompTerm CompTerm

The existing terms we have above (i.e. values of type Term) are also considered composite – we deem these Simple. Unary and binary composite terms are respectively labelled UnTerm and BinTerm. Notice we could have added these directly to the Term data type, but then it would be syntactically valid to take attributes of composite terms, e.g. $(t_1 + t_2).attr$ – which we would probably like to rule out.

Taking CompTerm as our new type for terms then requires the appropriate modification to Cond

data Cond = UnRel UnPred CompTerm
| BinRel BinPred CompTerm CompTerm
| ...

### Back to the example

Let us return to the example conditions above. With the suggested revision to the Cond type, The first four conditions can be re-expressed in the abstract syntax with little change if we make the appropriate adjustments to the syntactic sugar operators and helpers (namely subject, object, action, =*= and <@> – which is given below) to work with CompTerms. We also take this opportunity to introduce a further “smart constructor” ent to lift an Entity term into a CompTerm, thereby abstracting away excessive use of Simple wrappers.

ent :: String -> CompTerm
ent = Simple . Entity

(<@>) :: CompTerm -> String -> CompTerm
Simple t <@> a = Simple (Attr t a)

Thus lines 1-4 become

object  =*= ent "vehicle"
subject =*= ent "vehicle" <@> "owner" <@> "daughter"
action  =*= ent "drive-vehicle"
UnRel IsTrue (ent "owner" <@> "daughter" <@> "is-insured")

The intuitive interpretation of $local\text{-}time$ suggests that it ought to be a unary operation, taking a “location” term as parameter. As such, it would be appropriate to express the last two conditions as follows

ent "0900" <*= UnTerm LocalTime (ent "vehicle" <@> "location")
ent "2000" >*= UnTerm LocalTime (ent "vehicle" <@> "location")