Discussion:
[Agda] Operational and Denotational, Typed and Untyped Lambda Calculus
Philip Wadler
2018-03-29 12:31:54 UTC
Permalink
What is your favourite way to define lambda calculus in Agda? I am looking
for solutions both operational and denotational, and both typed and untyped.

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

Thank you for your help! 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/
Nils Anders Danielsson
2018-03-29 15:19:25 UTC
Permalink
Post by Philip Wadler
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
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
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
Philip Wadler
2018-03-30 18:36:21 UTC
Permalink
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
Larrytheliquid
2018-03-30 19:28:43 UTC
Permalink
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
Martin Escardo
2018-03-30 19:35:13 UTC
Permalink
Post by Philip Wadler
No favourites from anyone else? That doesn't seem much like this list!
(1) Of course, you can consider the type-theoretic incarnation of the
"set-theoretic model" of Goedel's system T (simply typed lambda calculus
with a base type for natural numbers, as you know).

http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf

This also considers a "dialogue" "forcing" model of system T, and then a
logical relation between this and the set-theoretical model to prove (in
Agda) that all system T definable functions (N->N)->N of the
set-theoretical model are continuous.

The paper quoted above works with the SKI-combinatory version of system
T, for simplicity of presentation. However, further accompanying Agda
files consider the lambda-calculus version, and more:
http://www.cs.bham.ac.uk/~mhe/dialogue/

(2) Again with system T, we can consider models in which all functions
(of all types) are continuous (rather than just the definable ones of
type (N->N)->N.)

This is done by my former PhD student Chuangjie Xu. https://cj-xu.github.io/

(3) Following from (2), this is actually a manifestation of the
Kleene-Kreisel continuous functionals from the 1950's, used at that time
(and to this day) to model computation with higher types. This is in the
above Agda code (2) and also in the paper

http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

(4) This hasn't been implemented in Agda yet, but it should:
http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf

And actually it needs a univalent extension of type theory, such as
cubical Agda: https://agda.readthedocs.io/en/latest/language/cubical.html

This last (4) is more in the vein of Dana Scott's ideas, but
constructively performed (following the lead of many people, including
Rosolini, Hyland, among others).

Best wishes,
Martin
Philip Wadler
2018-04-03 13:22:54 UTC
Permalink
Thank you for the further replies. I'm looking into them! 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 Philip Wadler
No favourites from anyone else? That doesn't seem much like this list!
(1) Of course, you can consider the type-theoretic incarnation of the
"set-theoretic model" of Goedel's system T (simply typed lambda calculus
with a base type for natural numbers, as you know).
http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf
This also considers a "dialogue" "forcing" model of system T, and then a
logical relation between this and the set-theoretical model to prove (in
Agda) that all system T definable functions (N->N)->N of the
set-theoretical model are continuous.
The paper quoted above works with the SKI-combinatory version of system T,
for simplicity of presentation. However, further accompanying Agda files
http://www.cs.bham.ac.uk/~mhe/dialogue/
(2) Again with system T, we can consider models in which all functions (of
all types) are continuous (rather than just the definable ones of type
(N->N)->N.)
This is done by my former PhD student Chuangjie Xu.
https://cj-xu.github.io/
(3) Following from (2), this is actually a manifestation of the
Kleene-Kreisel continuous functionals from the 1950's, used at that time
(and to this day) to model computation with higher types. This is in the
above Agda code (2) and also in the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf
http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf
And actually it needs a univalent extension of type theory, such as
cubical Agda: https://agda.readthedocs.io/en/latest/language/cubical.html
This last (4) is more in the vein of Dana Scott's ideas, but
constructively performed (following the lead of many people, including
Rosolini, Hyland, among others).
Best wishes,
Martin
Loading...