(*<*) (* * Knowledge-based programs. * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com. * License: BSD *) 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 (*>*)