Reply

PermalinkRaw Message

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 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/

*Post by Nils Anders Danielsson**Post by Philip Wadler*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

http://www.cse.chalmers.se/~nad/publications/danielsson-sema

ntics-partiality-monad.html

*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

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