I like the big-step normalization approach in terms of OPE's (order
preserving embeddings)
and environment closures used in James Chapman's thesis:
https://jmchapman.github.io/papers/tait2.pdf
Chantal and Thorsten's Agda version of using hereditary substitution via a
canonical
term syntax is also great, but it is more difficult to scale to additional
typing constructs:
http://www.cs.nott.ac.uk/~psztxa/publ/msfp10.pdf
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
normal
forms in closures, rather than expressions, and then defining the semantics
as a
version of a hereditary substituiton-based environment machine).
Here is the code, which uses a normalization function as the semantics:
https://github.com/larrytheliquid/sbe/blob/master/src/SBE/Intrinsic.agda
And a technical report explaining it:
http://www.larrytheliquid.com/drafts/sbe.pdf
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:
https://gist.github.com/larrytheliquid/6e7e9535d8f85f7a002f40f3d196cdc6
There is also a more efficient version that lazily computes conversion of
weak-head
normal forms by only expanding closures when necessary:
https://gist.github.com/larrytheliquid/b2a9171fea3aa4e461ef3181f8ca6889
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
terms
of a much simpler LF-like expression "surface" language with only the
function
type intro + elim rules (then you expose the intro + elim rules of other
types
via an initial environment, which may use your core language constructs).
Post by Philip WadlerThanks 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
. http://homepages.inf.ed.ac.uk/wadler/
Post by Nils Anders DanielssonPost by Philip Wadlerhttp://www.cse.chalmers.se/~nad/listings/partiality-monad/La
mbda.Simplified.Delay-monad.Interpreter.html
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
http://www.cse.chalmers.se/~nad/publications/danielsson-sema
ntics-partiality-monad.html
Post by Philip Wadlerdata 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
https://doi.org/10.1007/978-3-642-03359-9_10
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
http://types2017.elte.hu/proc.pdf#page=24
Note that higher inductive types are not (yet?) supported directly by
Agda.
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.
--
/NAD
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Respectfully,
Larry Diehl