Theory Eval
theory Eval
imports
Extra
Kripke
ODList
begin
subsection‹Algorithmic evaluation›
text‹
\label{sec:kbps-theory-eval}
Generically evaluate a knowledge formula with respect to a few
operations.
Intuition: Tableau, returns the subset of X where the formula
holds. Could generalise that to the set of \emph{all} states where the
formula holds, at least for the propositional part. This is closer to
the BDD interpretation. However in an explicit-state setup we want the
smallest sets that work.
Given an implementation of the relations, compute the subset of @{term
"X"} where @{term "X"} holds. Here we reduce space consumption by
only considering the reachable states at the cost of possible
reevaluation... BDDs give us some better primitives in some cases (but
not all). Something to ponder.
›
function
eval_rec :: "(('rep :: linorder) odlist ⇒ 'p ⇒ 'rep odlist)
⇒ ('a ⇒ 'rep ⇒ 'rep odlist)
⇒ ('a list ⇒ 'rep ⇒ 'rep odlist)
⇒ 'rep odlist
⇒ ('a, 'p) Kform
⇒ 'rep odlist"
where
"eval_rec val R CR X (Kprop p) = val X p"
| "eval_rec val R CR X (Knot φ) = ODList.difference X (eval_rec val R CR X φ)"
| "eval_rec val R CR X (Kand φ ψ) = ODList.intersect (eval_rec val R CR X φ) (eval_rec val R CR X ψ)"
| "eval_rec val R CR X (Kknows a φ) = ODList.filter (λs. eval_rec val R CR (R a s) (Knot φ) = ODList.empty) X"
| "eval_rec val R CR X (Kcknows as φ) = (if as = [] then X else ODList.filter (λs. eval_rec val R CR (CR as s) (Knot φ) = ODList.empty) X)"
by pat_completeness auto
fun
kf_k_measure :: "('a, 'p) Kform ⇒ nat"
where
"kf_k_measure (Kprop p) = 0"
| "kf_k_measure (Knot φ) = kf_k_measure φ"
| "kf_k_measure (Kand φ ψ) = kf_k_measure φ + kf_k_measure ψ"
| "kf_k_measure (Kknows a φ) = 1 + kf_k_measure φ"
| "kf_k_measure (Kcknows as φ) = 1 + kf_k_measure φ"
termination eval_rec
apply (relation "measures [λ(_, _, _, _, φ). size φ, λ(_, _, _, _, φ). kf_k_measure φ]")
apply auto
done
text‹
This function terminates because (recursively) either the formula
decreases in size or it contains fewer knowledge modalities.
We need to work a bit to interpret subjective formulas.
Expect @{term "X"} to be the set of states we need to evaluate @{term
"φ"} at for @{term "K a φ"} to be true.
Kcknows can be treated the same as Kknows... Just deals with top-level
boolean combinations of knowledge formulas.
The K cases are terrible. For CK we actually show @{term "K (CK
φ)"}. might be easier to futz that here.
›
fun
evalS :: "(('rep :: linorder) odlist ⇒ 'p ⇒ 'rep odlist)
⇒ ('a ⇒ 'rep ⇒ 'rep odlist)
⇒ ('a list ⇒ 'rep ⇒ 'rep odlist)
⇒ 'rep odlist
⇒ ('a, 'p) Kform ⇒ bool"
where
"evalS val R CR X (Kprop p) = undefined"
| "evalS val R CR X (Knot φ) = (¬evalS val R CR X φ)"
| "evalS val R CR X (Kand φ ψ) = (evalS val R CR X φ ∧ evalS val R CR X ψ)"
| "evalS val R CR X (Kknows a φ) = (eval_rec val R CR X (Knot φ) = ODList.empty)"
| "evalS val R CR X (Kcknows as φ) = (eval_rec val R CR (ODList.big_union (CR as) (toList X)) (Knot φ) = ODList.empty)"
text‹
We'd like some generic proofs about these functions but it's simpler
just to prove concrete instances.
The K cases are inefficient -- we'd like to memoise them,
etc. However it is suggestive of the ``real'' BDD
implementations. Compare with Halpern/Moses who do it more efficiently
in time (linear?) at the cost of space. In practice the knowledge
formulas are not deeply nested, so it is not worth trying too hard
here.
In general this is less efficient than the tableau approach of
\<^citet>‹‹Proposition~3.2.1› in "FHMV:1995"›, which labels all states with all
formulas. However it is often the case that the set of relevant worlds
is much smaller than the set of all system states.
›
end