I like the big-step normalization approach in terms of OPE's (order
and environment closures used in James Chapman's thesis:
Chantal and Thorsten's Agda version of using hereditary substitution via a
term syntax is also great, but it is more difficult to scale to additional
I'm also fond of some work I did extending James' work to define weak-head
normal forms independently of expressions (by embedding other weak-head
forms in closures, rather than expressions, and then defining the semantics
version of a hereditary substituiton-based environment machine).
Here is the code, which uses a normalization function as the semantics:
And a technical report explaining it:
I also made a more serious version, closer to what appears in James' thesis,
where the semantics is presented relationally + logical relations proofs,
here is the code but I haven't had a chance to write about it:
There is also a more efficient version that lazily computes conversion of
normal forms by only expanding closures when necessary:
The nice thing about this approach is that you can define weak-head normal
forms to be your "core" language, and then expose all the primitives in
of a much simpler LF-like expression "surface" language with only the
type intro + elim rules (then you expose the intro + elim rules of other
via an initial environment, which may use your core language constructs).
Post by Philip Wadler
Thanks very much, Nils!
No favourites from anyone else? That doesn't seem much like this list!
Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
Post by Nils Anders Danielsson Post by Philip Wadler
It defines values as closures, a syntactic approach.
This definition is similar to a standard big-step operational semantics,
and it is not defined compositionally (i.e. using recursion on the
structure of terms). Hence I see this as an operational, rather than
denotational, semantics. I made this argument in "Operational Semantics
Post by Philip Wadler
data value where
fun : (value -> Delay value) -> value
But this does not work because value appears in a negative position.
Is there a way to model a denotational description of values in Agda,
perhaps by mimicking one of the constructions of domain theory?
In a typed setting you could perhaps define value by recursion on the
structure of the types.
Benton, Kennedy and Varming used the delay monad to define the lifting
construction on Ï-CPOs, and they used this to define a denotational
Some Domain Theory and Denotational Semantics in Coq
There is also preliminary work in this direction that uses higher
inductive types to define, roughly speaking, the delay monad quotiented
Domain Theory in Type Theory via QIITs
Altenkirch, Capriotti and Reus
Note that higher inductive types are not (yet?) supported directly by
A different approach might be to use step-indexing. An alternative to
that would be to use guarded recursive types, which would allow you to
define something like value directly. However, I'm not aware of any
mature implementations of guarded recursive types.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Agda mailing list