State formulae:
W ::= | true | p | W1 ∨ W2 |¬W |
Transition formulae:
T ::= | W | W | T1 ∨ T2 |¬T |
Fusion expressions:
E ::= | test(W) |step(T) | E1 ∨ E2 | E1 ; E2 | E∗ |
Right Fusion logic formulae:
R ::= | true | p |¬R | R1 ∨ R2 |⟨E⟩R |
Left Fusion logic formulae:
L ::= | true | fin(p) |¬L | L1 ∨ L2 | L⟨E⟩ |
Fusion logic formulae:
F ::= | L | R |
A state is a mapping State from the set of propositional variables Varb to the set of Boolean values Bool ≜{tt,ff}.
tt is the semantic ‘true’ value and ff the semantic ‘false’ value.
State : Varb → Bool
We will use σ0,σ1,σ2,… to denote states and Σ to denote the set of all possible states.
An interval σ is a finite sequence of states
σ : σ0σ1σ2…
Let Σ+ denote the set of all possible finite intervals with at least one state.
The length of an interval σ is denoted by |σ| and is the number of states minus 1.
Let σ = σ0σ1σ2… be an interval then
Example 3. Let σ = σ0σ1σ2σ3 be an interval then
σ0σ1 |
is a prefix interval of σ |
σ1σ2σ3 | is a suffix interval of σ |
σ1σ2 |
is a sub interval of σ |
Let M⟦⟧ be the “meaning” function from ‘state formulae’ × Σ+ to {tt,ff} and let σ be a finite interval (σ ∈ Σ+) then
M⟦true⟧(σ) |
= |
tt |
M⟦p⟧(σ) | = | σ0(p) |
M⟦¬W⟧(σ) | = | not M⟦W⟧(σ) |
M⟦W1 ∨ W2⟧(σ) |
= |
M⟦W1⟧(σ) or M⟦W2⟧(σ) |
Let M⟦⟧ be the “meaning” function from ‘transition formulae’ × Σ+ to {tt,ff} and let σ be a finite interval (σ ∈ Σ+) then
M⟦¬T⟧(σ) |
= |
not M⟦T⟧(σ) |
M⟦T1 ∨ T2⟧(σ) | = | M⟦T1⟧(σ) or M⟦T2⟧(σ) |
M⟦ W⟧(σ) | = | M⟦W⟧(σ
1…σ|σ|) and |σ| > 0 |
Let M⟦⟧ be the “meaning” function from ‘fusion expressions’ × Σ+ to {tt,ff} and let σ be a finite interval (σ ∈ Σ+) then
M⟦test(W)⟧(σ) |
= |
M⟦W⟧(σ0) and |σ| = 0 |
M⟦step(T)⟧(σ) |
= |
M⟦T⟧(σ0…σ1) and |σ| = 1 |
M⟦E1 ∨ E2⟧(σ) |
= |
M⟦E1⟧(σ) or M⟦E2⟧(σ) |
M⟦E0 ; E1⟧(σ) = tt | iff | exists a k, s.t. 0 ≤ k ≤|σ| and |
M⟦E0⟧(σ0…σk) = tt and M⟦E1⟧(σk…σ|σ|) = tt |
||
M⟦E∗⟧(σ) = tt |
iff |
exist l0,…,ln s.t. l0 = 0 and ln = |σ| and |
for all 0 ≤ i < n,li < li+1 and |
||
M⟦E⟧(σli…σli+1) = tt |
Let M⟦⟧ be the “meaning” function from ‘right fusion logic formulae’ × Σ+ to {tt,ff} and let σ be a finite interval (σ ∈ Σ+) then
M⟦¬R⟧(σ) = |
= |
not M⟦R⟧(σ) |
M⟦R1 ∨ R2⟧(σ) |
= |
M⟦R1⟧(σ) or M⟦R2⟧(σ) |
M⟦⟨E⟩R⟧(σ) = tt | iff | exists a k, s.t. 0 ≤ k ≤|σ| and |
M⟦E⟧(σ0…σk) = tt and |
||
M⟦R⟧(σk…σ|σ|) = tt |
Let M⟦⟧ be the “meaning” function from ‘left fusion logic formulae’ × Σ+ to {tt,ff} and let σ be a finite interval (σ ∈ Σ+) then
M⟦fin(p)⟧(σ) |
= |
σ|σ|(p) |
M⟦¬L⟧(σ) |
= |
not M⟦L⟧(σ) |
M⟦L1 ∨ L2⟧(σ) | = | M⟦L1⟧(σ) or M⟦L2⟧(σ) |
M⟦L⟨E⟩⟧(σ) = tt | iff | exists a k, s.t. 0 ≤ k ≤|σ| and |
M⟦L⟧(σ0…σk) = tt and |
||
M⟦E⟧(σk…σ|σ|) = tt |
Derived Fusion expression operators
lene(0) |
≜ |
test(true) |
lene(n + 1) |
≜ |
step(true) ; lene(n) |
truee |
≜ |
step(true)∗ |
moree | ≜ | step(true) ; truee |
eW |
≜ |
truee ; test(W) ; truee |
eW |
≜ |
step(W)∗ ; test(W) |
n : W |
≜ |
truee ; test(W) ; lene(n) |
Derived right Fusion logic operators
R1 ∧ R2 |
≜ |
¬(¬R1 ∨¬R2) |
R1 ⊃ R2 |
≜ |
¬R1 ∨ R2 |
morer |
≜ |
⟨step(true)⟩true |
emptyr |
≜ |
¬morer |
lenr(0) |
≜ |
emptyr |
lenr(n + 1) |
≜ |
⟨step(true)⟩lenr(n) |
rR | ≜ | ⟨truee⟩R |
rR |
≜ |
¬r(¬R) |
rT |
≜ |
r⟨step(T)⟩true |
rW |
≜ |
r⟨truee⟩⟨test(W)⟩true |
rW |
≜ |
¬r(¬W) |
n : rW |
≜ |
⟨truee⟩⟨test(W)⟩lenr(n) |
[E]R |
≜ |
¬(⟨E⟩¬R) |
Derived left Fusion logic operators
L1 ∧ L2 |
≜ |
¬(¬L1 ∨¬L2) |
L1 ⊃ L2 |
≜ |
¬L1 ∨ L2 |
morel |
≜ |
true⟨step(true)⟩ |
emptyl |
≜ |
¬morel |
lenl(0) |
≜ |
emptyl |
lenl(n + 1) |
≜ |
lenl(n)⟨step(true)⟩ |
lW | ≜ | true⟨test(W)⟩⟨truee⟩ |
lW |
≜ |
¬l(¬W) |
lL |
≜ |
L⟨truee⟩ |
lL |
≜ |
¬l(¬L) |
n : lW |
≜ |
true⟨test(W)⟩⟨lene(n)⟩ |
L[E] |
≜ |
¬(¬L⟨E⟩) |