[Agda] Operational and Denotational, Typed and Untyped Lambda Calculus

[Nils Anders Danielsson]

On 2018-03-29 14:31, Philip Wadler wrote:
> My favourite denotational untyped solution so far is due to Nils Anders Danielsson:
> 
> http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.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
Using the Partiality Monad":

   http://www.cse.chalmers.se/~nad/publications/danielsson-semantics-partiality-monad.html

> What would be even better is to define values semantically:
> 
>    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
semantics for an untyped language:

   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
by weak bisimilarity:

   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