Email Gateway (Aug 22 2022 at 15:17): Email Gateway (Aug 22 2022 at 15:17):From: Denis Nikiforov <denis.nikif@gmail.com>
Hi
Could someone provide an example of denotational semantics of a simple
programing language defined via HOLCF? For example, "Denotational Sematics"
by David A. Schmidt contains very good examples. I'm trying to implement
them in HOLCF and I stuck at the begining. I've read HOLCF tutorial but
it's too brief. Brian Huffman's dissertation is too complex for me. I think
that an example of application of HOLCF to simple programming languages
from D. Schmidt's book or something like this would be very helpful for
newbies like me.
Email Gateway (Aug 22 2022 at 15:17):From: Peter Gammie <peteg42@gmail.com>
Denis,
There is my PCF entry in the AFP:
https://www.isa-afp.org/entries/PCF.shtml <https://www.isa-afp.org/entries/PCF.shtml>
The language is simple, but I’m not sure anything else is. :-)
Also if you dig through the HOLCF directory in the Isabelle distribution, there are some classical examples like streams and while loops.
cheers,
peter
Email Gateway (Aug 22 2022 at 15:18):From: Denis Nikiforov <denis.nikif@gmail.com>
Peter,
Thanks for advice! I'm trying to understand your example. You can see my
simple language below.
The problem is that when I try to evaluate expressions via dval function
(see 2 last lines in the theory) I get the following error:
Wellsortedness error
(in code equation u_map ≡ Λ f. fup⋅(up oo f),
with dependency "Pure.dummy_pattern" -> "dval" -> "ValD" :: "domain" ->
"ValD" :: "predomain" -> "ValD" :: "predomain_syn" -> "liftemb [ValD]" ->
"u_map"):
Type 'b⇩⊥ not of sort {enum,pcpo}
No type arity u :: enum
Could someone explain what's the problem?
theory Arithm4
imports
HOLCF
"~~/src/HOL/HOLCF/Library/Nat_Discrete"
begin
type_synonym var = nat
type_synonym Var = var
type_synonym 'a Env = "Var → 'a"
definition env_empty :: "'a Env" where
"env_empty ≡ ⊥"
definition env_ext :: "Var → 'a → 'a Env → 'a Env" where
"env_ext ≡ Λ v x ρ v'. if v = v' then x else ρ ⋅ v'"
domain ValD = ValFF | ValTT
datatype exp = Let var ValD exp | Var var | And exp exp
type_synonym EnvD = "ValD Env"
fixrec dand :: "ValD → ValD → ValD" where
"dand ⋅ ValTT ⋅ ValTT = ValTT"
| (unchecked) "b ≠ ⊥ ⟹ dand ⋅ ValFF ⋅ b = ValFF"
| (unchecked) "a ≠ ⊥ ⟹ dand ⋅ a ⋅ ValFF = ValFF"
primrec dval :: "exp ⇒ EnvD → ValD" where
"dval (Let var val exp) = (Λ e. dval exp ⋅ (env_ext ⋅ var ⋅ val ⋅ e))"
| "dval (Var var) = (Λ e. e ⋅ var)"
| "dval (And a b) = (Λ e. dand ⋅ (dval a ⋅ e) ⋅ (dval b ⋅ e))"
value "dval (Let 1 ValFF (Let 2 ValTT (And (Var 1) (Var 2)))) ⋅ env_empty"
value "dval (Var 1)"
end
Email Gateway (Aug 22 2022 at 15:18):From: Denis Nikiforov <denis.nikif@gmail.com>
Peter
Oops, it seems that the mailing list doesn't support unicode. Here is
an ASCII version:
Thanks for advice! I'm trying to understand your example. You can see
my simple language below.
The problem is that when I try to evaluate expressions via dval
function (see 2 last lines in the theory) I get the following error:
Wellsortedness error
(in code equation u_map ≡ Λ f. fup⋅(up oo f),
with dependency "Pure.dummy_pattern" -> "dval" -> "ValD" :: "domain"
-> "ValD" :: "predomain" -> "ValD" :: "predomain_syn" -> "liftemb
[ValD]" -> "u_map"):
Type 'b⇩⊥ not of sort {enum,pcpo}
No type arity u :: enum
Could someone explain what's the problem?
theory Arithm4
imports
HOLCF
"~~/src/HOL/HOLCF/Library/Nat_Discrete"
begin
type_synonym var = nat
type_synonym Var = var
type_synonym 'a Env = "Var \<rightarrow> 'a"
definition env_empty :: "'a Env" where
"env_empty \<equiv> \<bottom>"
definition env_ext :: "Var \<rightarrow> 'a \<rightarrow> 'a Env
\<rightarrow> 'a Env" where
"env_ext \<equiv> \<Lambda> v x \<rho> v'. if v = v' then x else
\<rho> \<cdot> v'"
domain ValD = ValFF | ValTT
datatype exp = Let var ValD exp | Var var | And exp exp
type_synonym EnvD = "ValD Env"
fixrec dand :: "ValD \<rightarrow> ValD \<rightarrow> ValD" where
"dand \<cdot> ValTT \<cdot> ValTT = ValTT"
| (unchecked) "b \<noteq> \<bottom> \<Longrightarrow> dand \<cdot>
ValFF \<cdot> b = ValFF"
| (unchecked) "a \<noteq> \<bottom> \<Longrightarrow> dand \<cdot> a
\<cdot> ValFF = ValFF"
primrec dval :: "exp \<Rightarrow> EnvD \<rightarrow> ValD" where
"dval (Let var val exp) = (\<Lambda> e. dval exp \<cdot> (env_ext
\<cdot> var \<cdot> val \<cdot> e))"
| "dval (Var var) = (\<Lambda> e. e \<cdot> var)"
| "dval (And a b) = (\<Lambda> e. dand \<cdot> (dval a \<cdot> e)
\<cdot> (dval b \<cdot> e))"
value "dval (Let 1 ValFF (Let 2 ValTT (And (Var 1) (Var 2)))) \<cdot> env_empty"
value "dval (Var 1)"
end
Email Gateway (Aug 22 2022 at 15:19):From: Peter Gammie <peteg42@gmail.com>
Denis,
The ‘value’ command relies on the code generator, which isn’t set up for HOLCF.
You could instead try to use the simplifier, e.g.:
lemma "dval (Let 1 ValFF (Let 2 ValTT (And (Var 1) (Var 2)))) \<cdot> env_empty = XXX"
apply simp
HTH,
peter
—
http://peteg.org/ <http://peteg.org/>
Last updated: Apr 20 2024 at 12:26 UTC