Transcript No Slide Title - Computer Science

Schemas as Toposes
Steven Vickers
Department of Pure Mathematics
Open University
Z schemas – specification
1st order theories – logic
geometric theories
toposes – as generalized topological spaces
Z schemas
e.g.
generic set
schema name
Trans [X]
declaration
R: XX
RR  R
meaning: “function”: {sets}  {sets}
X  {RXX  RR  R}
= {transitive relations on X}
predicate
First-order theory
e.g.
vocabulary
sort X
axiom
binary predicate R(x,y)
x,y,z:X. (R(x,y)  R(y,z)  R(x,z))
Meaning:
Set of all logical consequences of axioms amongst
well-formed formulae using vocabulary.
Models – of a first-order theory
• Interpret vocabulary as actual sets, relations, etc.
• … in such a way that the axioms are all true
e.g. for Trans
A model of Trans is a pair (X,R) with X a set and R a
transitive binary relation on it.
Guiding principle:
The purpose of a schema or theory is to
delineate a class of models
Schemas
as
Theories
Relational calculus
RR  R
Predicate calculus
can translate
x,y,z. (R(x,y)  R(y,z)  R(x,z))
Generics as parameters
Sorts as carriers
Higher-order
First-order
geometric logic
Types in Z
Z
integers

cartesian
product

power set
Presence of  means can have variables and terms for sets,
not just for elements.
e.g. S:X. …
Higher order! 1st order logic can’t do this.
Geometric logic
First order, many sorted.
Two levels of axiom formation:
• Formulas: built using , V, , , true, false
• Axioms:
x:X, y:Y, … ((x,y,…)  (x,y,…))
formulas
e.g. groups
Group [G]
e: G
-1:
GG
•: GG  G
x,y,z: G (true  x•(y•z) = (x•y) •z)
x: G (true  x•e = x  e•x = x)
x: G (true  x•x-1 = e  x-1•x = e)
Types out of logic
e.g. forcing Z  X+Y (disjoint union)
Th [X, Y, Z]
i: X  Z
j: Y  Z
x, x': X. (i(x) = i(x')  x = x')
y, y': Y. (j(y) = j(y')  y = y')
z: Z. (true  x: X. z = i(x)  y: Y. z = j(y))
x: X, y: Y. (i(x) = j(y)  false)
Moral
either:
can eliminate “type constructor” X+Y by
introducing new sort with 1st order structure and
axioms
or:
can harmlessly extend geometric logic
with + as type constructor
Using infinite disjunctions
e.g. forcing Y  F(X) (finite power set)
Th2 [X, Y]
: Y
{–}: X  Y
: YY  Y
y,y',y": Y. (true  (yy')y" = y(y'y"))
y,y': Y. (true  yy' = y'y)
y: Y. (true  y = y   y = y)
y: Y. (true  Vnnat x1, …, xn. y = {x1}  …{xn})
 x1, …, xm, x'1, …, x'n: X. ({x1}  …{xm} = {x'1}  …{x'n} 
1im V1jn xi = x'j  1jn V1im x'j = xi)
Weak 2nd order
Geometric logic has 2nd order capabilities for finite sets.
e.g.
S: F(X). (…)
– in formulas
S: F(X). (…)
– in axioms
Also, if S finite and  a formula then
xS. (x)
definable as a formula
Vnnat x1, …, xn. (S = {x1}  …{xn}  1in (xi))
Topology – e.g. real line
R
L, R  Q
true  q: Q. L(q)  q': Q. R(q')
q, q': Q. (q < q'  L(q')  L(q))
q: Q. (L(q)  q': Q. (q < q'  L(q'))
Each model is a real
number
(Dedekind section)
L(q): q < x
R(q): x < q
q, q': Q. (q > q'  R(q')  R(q))
q: Q. (R(q)  q': Q. (q > q'  R(q'))
q: Q. (L(q)  R(q)  false)
q, q': Q. (q < q'  L(q)  R(q'))
Topology is intrinsic:
each proposition is an
open set
GeoZ – geometric logic as specification language
•Take Z-style calculus
•Modify type system and logic to be geometric
Type constructors:
, +, equalizers, coequalizers, N, Z, Q, F, free algebras
But not:
 (power set),  (function set), R
•Constrains the language
•… but practical expressive power seems comparable with Z
Geometric logic – summary of features
• Advantages (simplicity) of 1st order logic
• … but can emulate higher order features (e.g. weak 2nd order)
• Natural picture: schema specifies “space of implementations”
• Good structure on each class of models – categorical,
topological
• Natural to consider maps that are functorial, continuous
Full mathematical answer is abstruse! –
geometric morphisms between classifying toposes
(topos as generalized topological space)
Challenge
Can the mathematics be made less abstruse for the sake of
specificational practice?
(And to the benefit of the mathematics too!)
Topology-free spaces
Synthetic topology
Idea:
Treat spaces like sets – forget topology
For functions:
Use constraints on mode of definition to ensure
definable  continuous
Old examples
• polynomial functions p: R  R are automatically continuous
p(x) = anxn + … + a1x + a0
• denotational semantics of programming languages
Given: a functional programming language, and a denotational
semantics for it.
Each function written in that language denotes a continuous map
between two topological spaces, “semantic domains”.
Continuity guaranteed by general semantic result.
Newer example
(Escardo) -calculus
-definable functions between topological spaces are
automatically continuous
– even if some of the function spaces don’t properly exist!
Simple proofs of topological results (compactness, closedness, …)
• express logical essence of proof
• hide topological housekeeping (continuity proofs etc.)
Geometric reasoning
Describe points of space = models of geometric theory
 intrinsic topology
Describe function using geometric constructions
 automatic continuity
Geometrically constructivist mathematics
 “topology-free spaces”
Logical approach 
locales / formal topologies
(propositional theories)
toposes
(predicate theories)
Topical Categories of Domains
(Vickers)
•Apply methods to denotational semantics.
[SFP] = “space” of SFP domains
topos
geometri
c
morphis
m
•Solving recursive domain equations X  F(X):
– any continuous map F: [SFP]  [SFP]
– has initial algebra X
– and its structure map : F(X)  X is an
isomorphism (a fixed point)
– copes with problems like F(X) = [XX]
(Topical Categories of Domains)
Task: define basic domain constructions (, +, function spaces,
power domains, …) geometrically (geometric constructivism).
Then e.g. function space construction is a geometric morphism.
[-  -]: [SFP]2  [SFP]
Constructive reasoning

geometric morphism

generalized continuity required for fixed points as limits
If E any local topos (e.g. [SFP]), F: E  E any geometric
morphism, then F has an initial fixed point.
  F()  F2()  F3()  …
– take colimit
Mathematical payoff
from geometric constructivism
• Focus on essence of mathematics
• Ignore topological housekeeping (e.g. continuity proofs)
• Includes generalization from topology to toposes
e.g.
• free access to fixed point results (e.g. domain equations)
• [SFP] a presheaf topos
– without examining category structure of topos
• “Spatial” proofs in locale theory
Current work (+ Townsend + Escardo)
• Make -calculus methods work with locales (propositional
geometric theories)
• Combine with geometric logic
e.g.
PU(PL(X))  $($X)
upper and lower
powerlocales
(cf. powerdomains)
Definable in terms of
geometric theories
function spaces
– so can use -calculus
Specificational aim
Mathematical “logic of continuity” (topology-free spaces)

Formal GeoZ specification language

Can test more fully in application
Conclusions
Computer science

has big influence on
Pure mathematics
The maths it leads to is worth investigating even for its own
sake
… BUT it retains links with computer science:
• motivation
• potential applications