Computing Science seminar by Murdoch Gabbay

You are not a number: how nameless foundations took over the world and made us think we have only numbers, and no names.

 

The semantic foundations of mathematics, such as higher-order logic and set theory, assume only basic data such as numbers or the empty set.  Yet, to do logic, programming, computation, or search, we need names.  Names come in many shapes and sizes: universal variables in logic and the lambda-calculus, holes in proof-search and meta-programming, pointers, channel names, nonces, method names, and much more.   Conventional semantics struggle to account for these rich structures by reducing them to edges in graphs, arguments of functions, or basic sets---if you like, they try to Godel encode everything down to "numbers".  Nominal semantics approach names as first-class entities: the mathematical universe reduces not just to numbers, but to numbers and names.  If we want to give our names extra structure, to make them model variables, or pointers, or holes, and so on, then we can do so by nominal axiomatic methods just as in conventional semantics we build groups, rings, fields, graphs, functions, and so on. Even if the reader does not care about foundations, foundations do care about the reader in the sense that they define, and delimit, the common vocabulary by which we pose questions, build models, do logic, and write programs.  In that sense nominal techniques are not just a bunch of theorems but a new language in which we could better express ourselves, and say new things. In this talk I will give a broad and non-technical overview of nominal techniques, sketching the journey from abstract foundations to some decently concrete mathematical applications, with special attention to the "new things" that are so difficult to express if we only have numbers and no names.  Further information can be found on http://www.gabbay.org.uk.

 

Speaker

Murdoch Gabbay

Hosted by

David Pym

Venue

Meston 2