Relating Domain Concepts Intensionally by Ordering Connections - Formal Methods and Hybrid Real-Time Systems - page 212

value
valid_plans: B WrkIdx ∼

× PrcIdx × → PP-infset

valid_plans(b,prcidx,wrkidx) ≡

{ |

pp:PP • φ (b,pp)(prcidx,wrkidx)

}

pp

∧ ∧

pre consistent(b,wrkidx) consistent(pp,wrkidx) consistent(pp,prcidx)

Similarly, we can define the set of applicable budgets begin the budgets which
apply financially, given a project plan; assuming the mediating ties:

value
appl_budgets: PP WrkIdx ∼

× PrcIdx × → B-infset

appl_budgets(pp,prcidx,wrkidx) ≡

{ b | b:B • φ (b,pp)(prcidx,wrkidx) }

pre consistent(b,wrkidx) ∧ consistent(pp,wrkidx) ∧ consistent(pp,prcidx)

) between
the power set of budgets and the power set of project plans; hence, between the
two concepts.

Generalising these two functions, gives a pair of dual functions ( F , G

value
F WrkIdx) ∼

:B-set → (PrcIdx × → PP-infset

F (bs)(prcidx,wrkidx) ≡

{ pp | pp:PP • ( ∀ b:B • b ∈ bs ⇒ φ (b,pp)(prcidx,wrkidx)) }

pre consistent(b,wrkidx) ∧ consistent(pp,wrkidx) ∧ consistent(pp,prcidx),

WrkIdx) →

G :PP-set → (PrcIdx × B-infset

G (pps)(prcidx,wrkidx) ≡

{ b | b:B • ( ∀ pp:PP • pp ∈ pps ⇒ φ (b,pp)(prcidx,wrkidx)) }

pre consistent(b,wrkidx) ∧ consistent(pp,wrkidx) ∧ consistent(pp,prcidx)

Theorem 2. The mapping pair ( F , G ) is a Galois connection.

Proof. The proof is by inspection using Theorem 1. The functions F and G cor-

respond to ϕ R and ψ R , respectively. The binary relation R N is the binary

relation between budget values (b:B) and project plan values (pp:PP). The binary
relation is defined by the predicate φ fp ; assuming

⊆ M ×

-quantification over the me-
diating ties (prcidx:PrcIdx) and (wrkidx:WrkIdx). X and Y correspond to finite
sets of values having type B and type PP, respectively; x and y are values in
these sets.

∀

The above shows that any predicate indicating a relation between objects of
two concepts, may be utilized in a definition of a Galois connection. What gives
substance to the Galois connection in this paper (and in the proposed method),
is expressed by the formal models of the two concepts.