Email Gateway (Aug 18 2022 at 15:55): Email Gateway (Aug 18 2022 at 15:55):From: Peter Gammie <peteg42@gmail.com>
Joachim,
Just a quick response, as it is late here. I'd suggest you read more background material before trying to prove anything. In particular, the original HOLCF paper is great, and there are some theories in the AFP that illustrate how to use HOLCF - Brian Huffman's stream fusion one is very well presented, and I hacked some things together in my worker/wrapper entry. There you will find a theory for the natural numbers that handles some of these issues.
I'd be very wary about mixing the continuous (HOLCF) and total (HOL) function spaces. It does work if you obey the design principles spelt out in the original paper.
Start with easy stuff - reasoning about lists defined using 'domain', e.g. The naturals, unless defined as a domain, are already fiddly. Sets are a long way from obvious, probably leading you to power domains if you have a non-trivial recursive definition.
Take a look at the examples in the HOLCF directory of the Isabelle distribution too.
It might help to switch on "Show sorts" in proof general and remember that if a type isn't annotated with pcpo (etc) then HOLCF doesn't know much about it.
cheers
peter
Email Gateway (Aug 18 2022 at 16:01):From: Joachim Breitner <mail@joachim-breitner.de>
Dear Brian,
thanks for your detailed response, I’m having a much clearer picture now
and also managed to define my function using HOLCF.
I had some problems with the cont2cont_Let' rule in the cont2cont rule
set. Here is a minimal example:
lemma "cont (λx. x⋅(Discr True))"
by (intro cont2cont)
works as expected. But
lemma "cont (λx. let y = True in x⋅(Discr y))"
by (intro cont2cont)
does not. The goal that it is stuck on is
"cont (λp. Discr (snd p))".
It works after I added this lemma to the cont2cont set, which works for
let expressions where the variable x does not appear in the bound
expression:
lemma cont2cont_Let_simple[simp,cont2cont]:
assumes "cont (λx. g x t)"
shows "cont (λx. let y = t in g x y)"
unfolding Let_def using assms .
I’m not sure if this is a general solution and or it would somehow
conflict with cont2cont_Let'. If it is a general solution, feel free to
add it to HOLCF.
Furthermore, I had to add these lemmas:
lemma cont2cont_list_case [simp, cont2cont]:
assumes "⋀y. cont (λx. f1 x)"
and "⋀y z. cont (λx. f2 x y z)"
shows "cont (λx. list_case (f1 x) (f2 x) l)"
using assms
by (cases l) auto
lemma cont2cont_prod_case [simp, cont2cont]:
assumes "⋀y z. cont (λx. f x y z)"
shows "cont (λx. prod_case (f x) p)"
using assms
by (cases p) auto
plus similar ones for each algebraic data types that I am using. The
form of these lemmas is very static – do you think this can be
generalized somehow? I did not yet write any ML scripts in Isabelle, but
I’m eager to learn if there is a worthwhile goal.
Thanks,
Joachim
PS: I wrote a "list :: cpo(cpo)" instance, relating lists of equal
length piecewise and not relating lists of different lengths, at
http://git.nomeata.de/?p=funcCF.git;a=blob;f=CFGraph/HOLCFList.thy;hb=HEAD
If you think this is generally useful and know where to put it I’d
happily share it (after make the proofs prettier).
signature.asc
Email Gateway (Aug 18 2022 at 16:01):From: Joachim Breitner <mail@joachim-breitner.de>
Hi Brian,
Am Freitag, den 03.09.2010, 14:25 -0700 schrieb Brian Huffman:
It works after I added this lemma to the cont2cont set, which works for
let expressions where the variable x does not appear in the bound
expression:
lemma cont2cont_Let_simple[simp,cont2cont]:
assumes "cont (λx. g x t)"
shows "cont (λx. let y = t in g x y)"
unfolding Let_def using assms .
I’m not sure if this is a general solution and or it would somehow
conflict with cont2cont_Let'. If it is a general solution, feel free to
add it to HOLCF.It would be good to add this new rule to HOLCF, but I would make a
small change to the "assumes" part:lemma cont2cont_Let_simple[simp,cont2cont]:
assumes "!!y. cont (λx. g x y)"
shows "cont (λx. let y = t in g x y)"
unfolding Let_def using assms .In case "t" is a large term, and/or "y" occurs many times in the body
of g, this might avoid a blow-up in term size.
it probably would not affect me at the moment, but are there no cases
where this would be too weak? What if "cont (λx. g x y)" does not hold
for all y, but only for y=t? But maybe such cases are only pathological
and do not occur in practice.
I guess the premise "let y = t in cont (λx. g x y)" would not allow the
other cont2cont rules to proceed.
Furthermore, I had to add these lemmas:
lemma cont2cont_list_case [simp, cont2cont]:
assumes "⋀y. cont (λx. f1 x)"
and "⋀y z. cont (λx. f2 x y z)"
shows "cont (λx. list_case (f1 x) (f2 x) l)"
using assms
by (cases l) autolemma cont2cont_prod_case [simp, cont2cont]:
assumes "⋀y z. cont (λx. f x y z)"
shows "cont (λx. prod_case (f x) p)"
using assms
by (cases p) auto
plus similar ones for each algebraic data types that I am using. The
form of these lemmas is very static – do you think this can be
generalized somehow? I did not yet write any ML scripts in Isabelle, but
I’m eager to learn if there is a worthwhile goal.I see that these lemmas assume that the variable "x" doesn't occur in
the scrutinee of the case expression; in practice it might be
necessary to create both versions of cont2cont rules for each case
combinator.
I used cont2cont_if as the template for these, and did not see a
cont2cont rule for if where x occurs in the condition. After all, it is
easy to create non-continuous functions then:
cont (λx. if x then False else True)
using the bool:pcpo instance should be false (because it is not
monotonous), even though "cont (λx. x)", "cont (λx. False)" and "cont
(λx. True)" hold. What form would a cont2cont rule about if have, if x
appears in the condition?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:07):From: Joachim Breitner <mail@joachim-breitner.de>
Hi again,
I have more questions about HOL/CF, especially about the fixrec package:
Consider again the function from my last example:
f b = {b} ∪ f b
I have this working definition:
fixrec f :: "int discr → (int ⇒ one)" where
"f⋅b = (f⋅b) (undiscr b := ONE)"
but I do not like how I have to use undiscr here (especially as in my
real example, the argument is more complex).
Shouldn’t fixrec be able to define the function having the type "int ⇒
(int ⇒ one)"? Based on my understanding, this type is also a pcpo and
therefore the operator based on the recursive definition with type
"(int ⇒ (int ⇒ one)) → (int ⇒ (int ⇒ one))" can be used to define f.
Unfortunately, this does not work:
fixrec f :: "int ⇒ int ⇒ one" where
"f b = (f b) (b := ONE)"
gives me
*** fixrec definition error:
*** unknown term
*** At command "fixrec".
while
fixrec f :: "int ⇒ int ⇒ one" where
"f = (λb. (f b) (b := ONE))"
gives
*** Continuity proof failed; please check that cont2cont rules
*** or simp rules are configured for all non-HOLCF constants.
*** The error occurred for the goal statement:
*** cont (λf b. (f b)(b := ONE))
*** At command "fixrec".
I’m also wondering why this works
fixrec g :: "(int×int) discr → ((int×int) ⇒ one)" where
"g⋅b = (case undiscr b of t ⇒ (g⋅(Discr t)) (t := ONE))"
but this does not:
fixrec g :: "(int×int) discr → ((int×int) ⇒ one)" where
"g⋅b = (case undiscr b of (a,c) ⇒ (g⋅(Discr (a,c))) ((a,c) := ONE))"
*** Continuity proof failed; please check that cont2cont rules
*** or simp rules are configured for all non-HOLCF constants.
*** The error occurred for the goal statement:
*** cont (λg. Λ a. case undiscr a of (a, c) ⇒ (g⋅(Discr (a, c)))((a, c) := ONE))
*** At command "fixrec".
Is all this a limitation of fixrec, or a limitation in my understanding
it? :-)
Thank in advance for your help,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:08):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I think I can answer one of the questions myself:
It works if I first show this lemma:
lemma cont_prod_case [simp, cont2cont]:
"[|⋀ a b. cont (f a b)|] ==> cont (λx. prod_case (λa b. f a b x) p)"
unfolding prod_case_unfold
by (induct p) simp_all
Does this mean that I have to show such a lemma for every function (or
case expression) that contains a recursive call to the function I’m
defining with fixrec? Or is there some automatism that I’m missing at
the moment?
Thanks again,
Joachim
signature.asc
Last updated: Apr 18 2024 at 16:19 UTC