Transitive closure with quantifiers in Alloy

Question

For the setup, I have a set of theorems, each with a set of values as a premise, a label, and a value it proves.

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

I also have the following constraints:

• Labels and premises are fixed for each theorem. One theorem always belongs to label 1 and always has A /\ B as a premise, theorems C => ? and D => ? both always belong to label 2, etc. There may be distinct theorems with the same premise belonging to different labels. For example, it's possible that I could have 4. C => A, even thought we already have 2. C => D.
• All premises are of the form A /\ B /\ ... /\ N. I will never have A /\ (B \/ C) as a premise, nor will I have ~A. But I could have two theorems that share a label, one with A /\ B as a premise and one with A /\ C.
• The values each theorem proves is variable, and in fact is the only thing that varies. Each theorem may prove at most one value.
• All theorems with the same label must prove the same value. If 2. C => (does not prove anything), then I must also have 2. A =>. At most one label can prove a given value. This means it makes sense to write this example as 1. C 2. D 3. V ...
• A value is "free" if no theorem proves it. V is never free.
• A value is "provable" if it is A) free, B) belongs to a theorem where the premise is satisfiable with provable values.

A model is valid if V is provable. In this case it is, since A and B are free, which gets us C, which gets us V. However, 1. A 2. C 3. V is invalid. What I'm trying to do is figure out which additional facts are required to make all possible models valid. For example, that counterexample disappears if we add a fact that says "A proved value can't be its own premise.

Here's an alloy model representing this:

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

The problem I have is in the solvable predicate. I need it to obey the conjunctions and work for an arbitrary depth. One possible solution would be to use the transitive closure. But if I do v in free or v in free.*(Theorem.(premise.proves)), the model becomes too permissive. It would say that if C is free, then A /\ C -> A is provable. This is because Alloy does not permit sets inside sets, so it collapses {A C} -> A into A -> C and A -> A.

On the other hand, I could write it as

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']

But this is very slow and also has a maximum recursion depth of 3. Is there a way to get the speed and arbitrary depth of using a closure with the accuracy of using a quantifier? I suppose I could add a trace, where each step successively proves more values, but it seems odd to enforce an ordering on a system that doesn't need it.

Answer 1

After a lot of experimentation, I've decided that the only good way to do this is with a trace. Here's the final spec if anybody's interested: open util/ordering[Step]

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