Replacing recursion with transitive closure (reachability and productivity of non-terminals)

Question

Sometimes, when I would like to use recursion in Alloy, I find I can get by with transitive closure, or sequences.

For example, in a model of context-free grammars:

abstract sig Symbol {}
sig NT, T extends Symbol {}

// A grammar is a tuple(V, Sigma, Rules, Start) 
one sig Grammar {
  V : set NT,
  Sigma : set T,
  Rules : set Prod,
  Start : one V
}

// A production rule has a left-hand side
// and a right-hand side
sig Prod {
  lhs : NT,
  rhs : seq Symbol
}

fact tidy_world {
  // Don't fill the model with irrelevancies
  Prod in Grammar.Rules
  Symbol in (Grammar.V + Grammar.Sigma)
}

One possible definition of reachable non-terminals would be "the start symbol, and any non-terminal appearing on the right-hand side of a rule for a reachable symbol." A straightforward translation would be

// A non-terminal 'refers' to non-terminals
// in the right-hand sides of its rules
pred refers[n1, n2 : NT] {
  let r = (Grammar.Rules & lhs.n1) |
  n2 in r.rhs.elems
}

pred reachable[n : NT] {
  n in Grammar.Start
  or some n2 : NT 
    | (reachable[n2] and refers[n2,n])
}

Predictably, this blows the stack. But if we simply take the transitive closure of Grammar.Start under the refers relation (or, strictly speaking, a relation formed from the refers predicate), we can define reachability:

// A non-terminal is 'reachable' if it's the
// start symbol or if it is referred to by
// (rules for) a reachable symbol.
pred Reachable[n : NT] {
  n in Grammar.Start.*(
    {n1, n2 : NT | refers[n1,n2]}
  )
}

pred some_unreachable {
  some n : (NT - Grammar.Start) 
    | not Reachable[n]
}
run some_unreachable for 4

In principle, the definition of productive symbols is similarly recursive: a symbol is productive iff it is a terminal symbol, or it has at least one rule in which every symbol in the right-hand side is productive. The simple-minded way to write this is

pred productive[s : Symbol] {
  s in T 
  or some p : (lhs.s) | 
      all r : (p.rhs.elems) | productive[r]
}

Like the straightforward definition of reachability, this blows the stack. But I have not yet found a relation I can define on symbols which will give me, via transitive closure, the result I want. Have I found a case where transitive closure cannot substitute for recursion? Or have I just not thought hard enough to find the right relation?

There is an obvious, if laborious, hack:

pred p0[s : Symbol] { s in T }
pred p1[s : Symbol] { p0[s] 
  or some p : (lhs.s) 
  | all e : p.rhs.elems 
  | p0[e]}
pred p2[s : Symbol] { p1[s] 
  or some p : (lhs.s) 
  | all e : p.rhs.elems 
  | p1[e]}
pred p3[s : Symbol] { p2[s] 
  or some p : (lhs.s) 
  | all e : p.rhs.elems 
  | p2[e]}
... etc ...
pred productive[n : NT] {
  p5[n]
}

This works OK as long as one doesn't forget to add enough predicates to handle the longest possible chain of non-terminal references, if one raises the scope.

Concretely, I seem to have several questions; answers to any of them would be welcome:

1 Is there a way to define the set of productive non-terminals in Alloy without resorting to the p0, p1, p2, ... hack?

2 If one does have to resort to the hack, is there a better way to define it?

3 As a theoretical question: is it possible to characterize the set of recursive predicates that can be defined using transitive closure, or sequences of atoms, instead of recursion?

Answer 1

Have I found a case where transitive closure cannot substitute for recursion?

Yes, that is the case. More precisely, you found a recursive relation that cannot be expressed with the first-order transitive closure (that is supported in Alloy).

Is there a way to define the set of productive non-terminals in Alloy without resorting to the p0, p1, p2, ... hack? If one does have to resort to the hack, is there a better way to define it?

There is no a way to do this in Alloy. However, there might be a way to do this in Alloy* which supports higher-order quantification. (The idea would be to describe the set of productive elements with a closure over the relation of "productiveness", which would use second-order quantification over the set of productive symbols, and constraining this set to be minimal. Similar idea is described in "A.1.9 Axiomatizing Transitive Closure" in the Alloy book.)

As a theoretical question: is it possible to characterize the set of recursive predicates that can be defined using transitive closure, or sequences of atoms, instead of recursion?

This is an interesting question. The wiki article mentions relative expressiveness of second order logic when transitive closure and fixed point operator are added (the later being able to express forms of recursion).