Propagation is VERY bad

[Ruben Lapauw]

Basic one-step propagation fails miserably:

vocabulary V {
    type T isa int
    Q(T, T)
}


structure S : V {
    T = {0..3}
}

structure expected : V {
    T = {0..3}
    Q<ct> = {0,0}
    Q<cf> = {0,1;0,2;0,3}
}

procedure main(){
    stdoptions.nrpropsteps = 1000
    print("Expected Result for all:")
    print(expected)
    print("T1:")
    print(propagate(T1,S))
    print("T2:")
    print(propagate(T2,S))
    print("T3:")
    print(propagate(T3,S))
    print("T4:")
    print(propagate(T4,S))
    print("T5:")
    print(propagate(T5,S))
    print("T6:")
    print(propagate(T6,S))
} 

theory T1 : V {
    !r : r = 0 <=> Q(0,r).
}

theory T2 : V {
    !r : r ~= 0 <=> ~Q(0,r).
}

theory T3: V {
    !r : r ~= 0 <=> ~Q(0,r).
    !r : r = 0 <=> Q(0,r).
}


theory T4 : V {
    !r : r=0 | ~(? x : x = 0 & Q(x, r)).
    !r : r~=0 | (? x : x = 0 & Q(x, r)).
}

theory T5 : V {
    Q(0,0).
}

theory T6 : V {
    ?r, x : r = 0 & x = 0 & Q(x, r).
}

[Bart Bogaerts]

T5 en T6 moeten zeker niet "expected" als resultaat hebben..

T4 is onleesbaar, dus daar kan ik niet over oordelen.

T3 doet hij goed.

T1 en T2 geeft hij te zwakke propagatie (propagatie samen is wel goed).

Hypothese: door slechte unnesting is de propagatie niet zo sterk als gewenst. (slechte introductie van extra variabelen).

Bigger issue. Het "unnesten" van domeinelementen voor symbolische propagatie zou misschien eens herbekeken moeten worden

[Bart Bogaerts]

In reply to Ruben's comment

T1 en T2 is inderdaad te zwak. T3: Door de combinatie van beide is het mogelijk om een volledige propagatie te doen. Dit zou toch niet mogen zijn? T4 is de herschrijving van T1, die gebeurt +- halverwege in de broncode. T5 is inderdaad niet volledig hetzelfde. Maar zelfs Q<ct> = {(0,0)} wordt niet triviaal afgeleid. T6 is dezelfde herschrijving als T4.

De propagatie is steeds approximatief, dus er worden geen garanties gegeven over wat wordt afgeleid. Maar.... Ik ben het ermee eens: het zou hier beter moeten!

Wat T2 betreft. Dat kan niet dat dat dezelfde herschrijving is gezien die volledig existentieel gequantificeerd is.

Die herschrijvingen waarover je praat, die zijn de "unnesting" waar ik naar verwijs

[Ruben Lapauw]

T1 en T2 is inderdaad te zwak.

T3: Door de combinatie van beide is het mogelijk om een volledige propagatie te doen. Dit zou toch niet mogen zijn?

T4 is de herschrijving van T1, die gebeurt +- halverwege in de broncode.

T5 is inderdaad niet volledig hetzelfde. Maar zelfs Q<ct> = {(0,0)} wordt niet triviaal afgeleid.

T6 is dezelfde herschrijving als T4. T7 heeft ook een ander gedrag dan T4. theory T7 : V { ∀r : r=0 ∨ ¬Q(0, r). ∀r : r≠0 ∨ Q(0, r). }