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

[Larrytheliquid]

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).



On Fri, Mar 30, 2018 at 1:36 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> 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
>>
>>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>


-- 
Respectfully,
Larry Diehl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180330/e1b3d8cd/attachment.html>