predicates in Essence

[ott2]

Essence is a fragment of relational second-order logic. All logics have a syntax for defining predicates, so that more complex expressions can be expressed succinctly in terms of predicates, with arbitrarily deep nesting of predicate expressions. A predicate is simply a macro, and the syntax usually supports substitution via some restricted form of pattern matching.

I propose an initial syntax along the following lines:

letting between(a,b,c) be predicate(
   (a < b) /\ (b < c)
)
letting noIsolatedVertices(x,y) be predicate(
   forAll u : x .
      exists v : x .
         (u != v) /\ ({u,v} in y)
)
letting hom(V,E,W,F) be predicate(
   exists f : function V --> W .
      forAll {u,v} in E .
         {f(u),f(v)} in F
)

Here the parameters are substituted in with parentheses added when the substitution is made, to avoid unexpected changes in operator precedence.

My initial thoughts are to require predicates to be formulas in which the only free variables are the parameters. This may not be a necessary restriction, but it does become difficult to provide precise semantics and error messages for a more general macro mechanism that does things like reference domains that it expects have been defined. For instance, the following would be nice to have, but is not strictly necessary for a first version:

given n : int(1..)
letting vertices be domain int(1..n)
given G : set of set (size 2) of vertices
letting triangleFree(E) be predicate(
   forAll u,v,w : vertices .
      !(({u,v} in E) /\ ({v,w} in E) /\ ({w,u} in E))
)
find q : bool such that q = triangleFree(E)