|
(* Title: HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
Author: Andreas Lochbihler, ETH Zuerich
Author: Jasmin Blanchette, Inria, LORIA, MPII
Copyright 2016
A bare bones version of generative probabilistic values (GPVs).
*)
section \<open>A Bare Bones Version of Generative Probabilistic Values (GPVs)\<close>
theory GPV_Bare_Bones
imports "HOL-Library.BNF_Corec"
begin
datatype 'a pmf = return_pmf 'a
type_synonym 'a spmf = "'a option pmf"
abbreviation map_spmf :: "('a \ 'b) \ 'a spmf \ 'b spmf"
where "map_spmf f \ map_pmf (map_option f)"
abbreviation return_spmf :: "'a \ 'a spmf"
where "return_spmf x \ return_pmf (Some x)"
datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat =
Pure (result: 'a)
| IO ("output": 'b) (continuation: "'c")
codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv =
GPV (the_gpv: "('a, 'out, 'in \ ('a, 'out, 'in) gpv) generat spmf")
codatatype ('a, 'call, 'ret, 'x) gpv' =
GPV' (the_gpv': "('a, 'call, 'ret \ ('a, 'call, 'ret, 'x) gpv') generat spmf")
consts bind_gpv' :: "('a, 'call, 'ret) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'call, 'ret, 'a) gpv') \<Rightarrow> ('b, 'call, 'ret, 'a) gpv'"
definition bind_spmf :: "'a spmf \ ('a \ 'b spmf) \ 'b spmf"
where "bind_spmf x f = undefined x (\a. case a of None \ return_pmf None | Some a' \ f a')"
friend_of_corec bind_gpv'
where "bind_gpv' r f =
GPV' (map_spmf (map_generat id id ((\) (case_sum id (\r. bind_gpv' r f))))
(bind_spmf (the_gpv r)
(case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv' (f x)))
(\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
sorry
end
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
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 ist noch experimentell.
|
