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

[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
. http://homepages.inf.ed.ac.uk/wadler/

On 29 March 2018 at 12:19, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> 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/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
> Using the Partiality Monad":
>
>   http://www.cse.chalmers.se/~nad/publications/danielsson-sema
> ntics-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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180330/61a60ffd/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180330/61a60ffd/attachment.ksh>