[Prev][Next][Index][Thread]
[coraki!pratt@sun.com: Wednesday seminar: Dynamic Types]
Date: Tue, 8 Dec 87 19:29:08 PST
From: coraki!pratt@sun.com (Vaughan Pratt)
To: conmod@navajo.stanford.edu
Subject: Wednesday seminar: Dynamic Types
Cc: friends@csli.stanford.edu, logmtc@sail.stanford.edu
Speaker: Vaughan Pratt
Title: Arithmetic of Dynamic Types
Location: MJ301
Time: 10:00-12:00, Wednesday Dec. 9
Abstract:
I will present a simplified and strengthened definition of "dynamic
type." The basic notion of a dynamic type as an edge-labeled and
vertex-labeled graph with additional categorical structure remains
unchanged. The difference is the elimination of the category Set from
the definition. Besides being more in tune with modern category
theory, the new definition has the practical effect of permitting new
types to be named, the most elementary of which is 2|>2, the dynamic
type of order ideals. Applications of 2|>2 include the definition of
the reals and the proof of Stone's theorem. The arithmetic of order
ideals is obtained by exactly the same process as for the arithmetic of
Set = 1|>1, Cat = (1|>1)|>1, Prom = 2|>(1|>1) (whose arithmetic
constitutes the concurrent programming language SSL), etc. I will
conclude with a discussion of the relevance of dynamic types to
Birkhoff's vision of generalized arithmetic.
-v