Email Gateway (Aug 19 2022 at 12:20): Email Gateway (Aug 19 2022 at 12:20):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
I (kind of) wanted to star playing a bit with fixpoint operators in
Isabelle, which is motivated by experiments in denotational
semantics of imperative languages.
I have noticed that the theories available in the Isabelle
distribution (concerning the IMP language) follow Winskel´s
relational approach. That is to say, the denotation of a command
is a set of pair of states, and then one can easily define
the semantics of while by the least fixpoint of the appropriate
functional using Isabelle´s lfp fixpoint operator.
In general, the fix point operator fix has type
(D->D)->D where D must be a chain complete cpo with
a least element (according to Winskel´s Lecture Notes on
Denotational Semantics). In Isabelle, the operator
lfp has type ('a ->'a)->'a, and it is defined in the
theory Complete Lattice. So, what is the minimal requirement
in Isabelle
On the other hand, in section 6.5 of the Isabelle/HOL tutorial
the type of 'a is also a set of pairs and in the discussion
it is implied that 'a must always be a set.
The book "Concrete Semantics"
by Nipkow and Klein also uses a relational semantics
So my main questions are:
1) How to use the fixpoint operator on functionals that
are not based on sets of pairs? ?
2) Do I need complete lattices or cpo´s with least elements
suffice?
3) Can I use functionals where D is a function space
(for instance, using partial maps provided by Isabelle).
4) Do I have to use type classes to make the appropriate
instantiations? (If yes I have no idea how)
Thanks for any help. This will be a long journey!
Email Gateway (Aug 19 2022 at 12:21):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Alfio,
Have you already looked at HOLCF? It formalises domain theory and denotational semantics.
If not, that's where you should go first. Brian Huffman's PhD thesis describes what is in
there and how to use it.
lfp has type "('a => 'a) => 'a" where 'a must be of sort complete_lattice. _ set
instantiates complete_lattice, so lfp can in particular be used for functionals on all
sets. But you can also use other types that instantiate complete_lattice. For example, if
'a is a complete lattice, then so is _ => 'a, i.e., you can also use functions.
If you only have a chain-complete partial order with a least element, you cannot use lfp,
but instead fixp from the theory Complete_Partial_Order, but you have to deal with
admissibility yourself. This is where HOLCF greatly helps you.
All of the above solutions are based on type classes, and this is what makes them
convenient. The package partial_function provides some front-end to fixp that does not
rely on type classes, but I recommend that you use the type classes, because they make
definitions and proofs much simpler.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 12:21):From: Brian Huffman <huffman.brian.c@gmail.com>
On Tue, Oct 8, 2013 at 7:32 AM, Andreas Lochbihler
<andreas.lochbihler@inf.ethz.ch> wrote:
Hi Alfio,
Have you already looked at HOLCF? It formalises domain theory and
denotational semantics. If not, that's where you should go first. Brian
Huffman's PhD thesis describes what is in there and how to use it.
[...]
If you only have a chain-complete partial order with a least element, you
cannot use lfp, but instead fixp from the theory Complete_Partial_Order, but
you have to deal with admissibility yourself. This is where HOLCF greatly
helps you.
Hi Alfio,
I should point out a few differences between the HOLCF and
Complete_Partial_Order formalizations of fixpoints:
Class ccpo from Complete_Partial_Order uses a slightly stronger
completeness condition than HOLCF uses; ccpo requires lubs of
arbitrary chains, while HOLCF requires lubs only for countable chains.
On the other hand, class ccpo has fixpoints for all monotone
functions, whereas HOLCF additionally requires functions to be
continuous.
The other major consideration is that HOLCF uses a continuous function
space type "'a -> 'b" almost everywhere, rather than using ordinary
functions "'a => 'b" with a continuity predicate. One consequence is
that you are locked in to using type classes for cpos (type 'a -> 'b
is only defined for cpo types); Complete_Partial_Order is a bit more
flexible in this regard.
That said, if you are willing to commit to using type classes and the
continuous function space type, HOLCF provides highly tuned automation
for proving continuity and admissibility.
Whichever library you decide to use, I'd welcome any questions,
comments, or suggestions for improvements to either library.
Email Gateway (Aug 19 2022 at 12:21):From: Alfio Martini <alfio.martini@acm.org>
Many Thanks Brian and Andreas!
I have already downloaded Brian´s PhD thesis and it seems
highly readable!
All The Best!
Email Gateway (Aug 19 2022 at 12:22):From: Viorel Preoteasaa <viorel.preoteasa@abo.fi>
Hi Alfio,
Another approach of using least fix points for semantics of programs
is when using a predicate transformer semantics. As compared to
programs as relations which can be used for modelling partial correctness,
predicate transformers allows modelling total correctness.
If S is the set of computation states, programs are modelled as monotonic
functions from power set of S (Pred.S = S->bool) to Pred.S. In this model a
program P applied to a set X of final states returns the initial states from
which P terminates, and it terminates in a state from X.
Iteration can be defined in this model as a least fix point of a monotonic
function from (Pred.S)->(Pred.S) to (Pred.S)->(Pred.S). This least fix point
exists in the complete lattice of monotonic predicate transformers
((Pred.S)->(pred.S))
You can find formalizations of these concepts in the AFP entries:
[1] Semantics and Data Refinement of Invariant Based Programs
(sections 3 and 4)
[2] Algebra of Monotonic Boolean Transformers (Section 3)
and corresponding papers:
[3] Preoteasa, Viorel and Back, Ralph-Johan.
Invariant Diagrams with Data Refinement. Formal Aspect of Computing.
Vol: 24, Num: 1, Pages 67-95. Springer London.
http://dx.doi.org/10.1007/s00165-011-0195-2. 2012.
[4] Preoteasa, Viorel. Refinement algebra with dual operator.
Science of Computer Programming.
http://dx.doi.org/10.1016/j.scico.2013.07.002. 2013.
[2] and [4] introduces an algebra for modelling programs. The
basic model for this algebra is set of monotonic predicate
transformers with their operations, so everything that is
done in the algebra is true in the model. Actually you will
find the definition of the while statement and its properties
the algebra part of the paper. The model contains just the
the results needed to show that it is indeed a model for the algebra.
[2] and [4] uses an arbitrary Boolean algebra B instead of Pred.S
The algebra is more abstract than the model. In the algebra
only fixed points of certain functions are axiomatised. These
are the functions needed for defining the while statements.
Best regards,
Viorel Preoteasa
Email Gateway (Aug 19 2022 at 12:22):From: Alfio Martini <alfio.martini@acm.org>
Thank you Viorel for the very detailed reply and the great references.
I was not aware of them!
All the Best!
Last updated: Apr 19 2024 at 04:17 UTC