Skip to main content

Topological nominal semantics

Jamie Gabbay ( Heriot-Watt University )

My longest ever paper was called "Representation and duality of the
untyped lambda-calculus" at nearly 91 pages.

Though too long, the paper does something unusual and interesting: we
build a topological semantics for the lambda-calculus, in which
lambda-calculus terms are given semantics as open sets in a
topological space, and lambda-abstraction becomes both a logical
quantifier and a corresponding operation on open sets.

A similar programme has also been carried out for first-order logic.

Taken together, these two papers show how to extend Stone duality from
(for example) Boolean algebras, to algebras for first-order logic and
the lambda-calculus.   We can do this because we use nominal semantics
to handle the meaning of variables in first-order logic and the
lambda-calculus.

This talk will not be an exhaustive technical account.  Instead, I
will try to give an accessible overview of Stone-style duality theory,
and how and why new possibilities are opened up when looked at from
the point of view of nominal semantics.  I will outline what
topological semantics look like in a nominal universe, and explain why
this is new and interesting.

Interested readers can view the two papers here:

"Representation and duality of the untyped lambda-calculus"
http://www.gabbay.org.uk/papers.html#repdul
APAL, 2017

"Semantics out of context"
http://www.gabbay.org.uk/papers.html#semooc
Journal of the ACM, 2016

 

 

Share this: