合金中量词的传递闭包

Question

对于设置，我有一组定理，每个定理都有一组值作为前提，一个标签和一个它证明的值。

1. A / B => C
2. C => D
2. A => D // note same label as C => D
3. B / C => V
4. ...

我还有以下约束：

• 每个定理的标签和前提都是固定的。一个定理总是属于标签 1，并且总是以A / B为前提，定理C => ?和D => ?总是属于标签 2，依此类推。可能存在具有相同前提的不同定理，属于不同的标签。例如，我有可能4. C => A，甚至认为我们已经有了2. C => D。
• 所有房舍均为A / B / ... / N形式。我永远不会有A / (B / C)作为前提，也不会有~A.但是我可以有两个共享标签的定理，一个以A / B为前提，一个以A / C为前提。
• 每个定理证明的值是可变的，实际上是唯一变化的东西。每个定理最多可以证明一个值。
• 具有相同标签的所有定理必须证明相同的值。如果2. C =>(不能证明什么)，那么我也必须有2. A =>.最多一个标签可以证明给定的值。这意味着将此示例编写为1. C 2. D 3. V ...
• 如果没有定理证明，则值是"自由的"。V从来都不是免费的。
• 如果一个值是"可证明的"，如果它是A)自由的，B)属于一个定理，其中前提可以用可证明的值来满足。

如果 V 可证明，则模型有效。在这种情况下，由于 A 和 B 是免费的，因此我们得到 C，得到我们 V。但是，1. A 2. C 3. V无效。我试图做的是弄清楚需要哪些额外的事实才能使所有可能的模型有效。例如，如果我们添加一个事实，即"一个被证明的价值不能是它自己的前提。

这是一个代表这一点的合金模型：

abstract sig Label { 
proves: disj lone Value
}
one sig L1, L2, LV extends Label{}
abstract sig Value{}
one sig A, B, C, D, V extends Value {}
sig Theorem {
premise: Value set -> Label
}
fun free: set Value {
Value - Label.proves
}
pred solvable(v: Value) {
v in free or // ???    
}
pred Valid {
solvable[V]
}

pred DefaultTheorems {
one disj T1, T2, T3, T4: Theorem | {
#Theorem = 4
T1.premise = (A + B) -> L1
T2.premise = C -> L2
T3.premise = A -> L2
T4.premise = (B + C) -> LV  
}
LV.proves = V
}
check { DefaultTheorems => Valid } for 7

我的问题出在solvable谓词中。我需要它服从连词并为任意深度工作。一种可能的解决方案是使用传递闭包。但是如果我这样做v in free or v in free.*(Theorem.(premise.proves))，模型就会变得过于宽松。它会说，如果C是免费的，那么A / C -> A是可以证明的。这是因为合金不允许集合内的集合，因此它会{A C} -> A折叠成A -> C并A -> A。

另一方面，我可以把它写成

pred solvable(v: Value) {
v in free or some t: Theorem |
let premise' = (t.premise).(proves.v) |
some v' and all v': premise' | solvable[v']

但这非常慢，并且最大递归深度为 3。有没有办法获得使用闭包的速度和任意深度，以及使用量词的准确性？我想我可以添加一个跟踪，其中每个步骤都连续证明更多的值，但是在不需要它的系统上强制执行排序似乎很奇怪。

Answer 1

经过大量的实验，我决定这样做的唯一好方法是使用痕迹。如果有人感兴趣，这是最终规格： 打开使用/订购[步骤]

sig Step {}
abstract sig Label { 
proves: disj lone Value
}
one sig L1, L2, LV extends Label{}
abstract sig Value {
proven_at: set Step
}
one sig A, B, C, D, V extends Value {}
sig Theorem {
premise: Value set -> Label
}
fun free: set Value {
Value - Label.proves
}
pred solvable(v: Value, s: Step) {
v in proven_at.s or
some t: Theorem |
let premise' = (t.premise).(proves.v) |
some premise' and all v': premise' |
v' in proven_at.s
}
pred Valid {
solvable[V, last]
}
fact Trace {
free = proven_at.first
all s: Step - last | 
let s' = s.next |
proven_at.s' = proven_at.s + {v: Value | solvable[v, s]}
}
pred DefaultTheorems {
one disj T1, T2, T3, T4: Theorem | {
#Theorem = 4
T1.premise = (A + B) -> L1
T2.premise = C -> L2
T3.premise = A -> L2
T4.premise = (B + C) -> LV  
}
LV.proves = V
}
check { DefaultTheorems => Valid } for 8 but 4 Step