theory Eval imports
Extra
Kripke
ODList begin (*>*)
subsection‹Algorithmic evaluation›
text‹
label{sec:kbps-theory-eval}
evaluate a knowledge formula with respect to a few
.
: Tableau, returns the subset of X where the formula
. Could generalise that to the set of \emph{all} states where the
holds, at least for the propositional part. This is closer to
BDD interpretation. However in an explicit-state setup we want the
sets that work.
an implementation of the relations, compute the subset of @{term
X"} where @{term "X"} holds. Here we reduce space consumption by
considering the reachable states at the cost of possible
... BDDs give us some better primitives in some cases (but
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
function terminates because (recursively) either the formula
in size or it contains fewer knowledge modalities.
need to work a bit to interpret subjective formulas.
@{term "X"} to be the set of states we need to evaluate @{term
φ"} at for @{term "K a φ"} to be true.
can be treated the same as Kknows... Just deals with top-level
combinations of knowledge formulas.
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‹
'd like some generic proofs about these functions but it's simpler
to prove concrete instances.
K cases are inefficient -- we'd like to memoise them,
. However it is suggestive of the ``real'' BDD
. Compare with Halpern/Moses who do it more efficiently
time (linear?) at the cost of space. In practice the knowledge
are not deeply nested, so it is not worth trying too hard
.
general this is less efficient than the tableau approach of 🍋‹‹Proposition~3.2.1› in "FHMV:1995"›, which labels all states with all
. However it is often the case that the set of relevant worlds
much smaller than the set of all system states.
› (*<*)
end (*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
