用传递闭包代替递归（非终端的可达性和生产力）

Question

有时，当我想在 Alloy 中使用递归时，我发现我可以使用传递闭包或序列。

例如，在上下文无关文法模型中：

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)
}

可达非终端的一个可能定义是"the start symbol, and any non-terminal appearing on the right-hand side of a rule for a reachable symbol."一个简单的翻译是

// 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])
}

不出所料，这会破坏堆栈。但是如果我们简单地取Grammar.Start在refers关系下的传递闭包（或者，严格来说，由refers谓词形成的关系），我们可以定义可达性：

// 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

原则上，生产性符号的定义同样是递归的：一个符号是生产性的，当且仅当它是一个终结符号，或者它至少有一个规则，其中右侧的每个符号都是生产性的。简单的写法是

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

就像可达性的直接定义一样，这会破坏堆栈。但是我还没有找到我可以在符号上定义的关系，它会通过传递闭包给我想要的结果。我有没有发现传递闭包不能代替递归的情况？还是我只是想得不够仔细，没有找到合适的关系？

有一个明显但费力的 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]
}

只要不忘记添加足够的谓词来处理尽可能长的非终端引用链（如果扩大范围），这就可以正常工作。

具体来说，我好像有几个问题；欢迎回答其中任何一个问题：

1 有没有一种方法可以在 Alloy 中定义一组高效的非终端而不求助于 p0、p1、p2... hack？

2 如果必须求助于 hack，是否有更好的定义方式？

3 作为一个理论问题：是否可以表征可以使用传递闭包或原子序列而不是递归来定义的递归谓词集？

Answer 1

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

是的，是这样的。更准确地说，您发现了一个不能用一阶传递闭包（在 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?

在 Alloy 中没有办法做到这一点。但是，在支持高阶量化的 Alloy* 中可能有一种方法可以做到这一点。（想法是用 "productiveness" 关系上的闭包来描述生产性元素集，这将对生产性符号集使用二阶量化，并将该集约束为最小值。类似的想法是Alloy 书中的 "A.1.9 Axiomatizing Transitive Closure" 中有描述。）

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?

这是一个有趣的问题。 wiki文章中提到了添加传递闭包和定点运算符后二阶逻辑的相对表达能力（后者可以表达递归形式）。

用传递闭包代替递归（非终端的可达性和生产力）

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

alloy