SSL Eval.thy

Sprache: Isabelle

(*<*)
(*
* 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}

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

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‹

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.2 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.