Programming with the
Mathematical and the Physical
Uday S. Reddy
School of Computer Science
The University of Birmingham
1
Programming Language Semantics
Building mathematical & conceptual models of
programming language concepts.
Draws upon
• Linguistics
• Mathematical logic
2
Example
Bong game created by Jason Moey
3
History
• Founded by Christopher Strachey
(Oxford Programming Research Group).
Jointly with Dana Scott.
• Other major figures:
– Gordon Plotkin (Edinburgh)
– Robin Milner (Edinburgh/Cambridge)
– John Reynolds (Syracuse/Carnegie-Mellon)
4
The General Picture
Space of programs
Semantic space
5
The General Picture
Space of programs
Semantic space
6
The General Picture
Space of programs
Semantic space
7
The General Picture
Space of programs
Semantic space
More abstract
Semantic space
8
Fully Abstract Models
• A fully abstract model identifies all programs that
have the same observable behavior.
• Signifies that all aspects of the behavior have
been captured correctly and accurately.
9
My Contributions
• 1990 – Started looking at the “local variable” problem.
• 1993 – Produced a new semantic model for interferencecontrolled imperative programs (object-based model).
–
–
Journal version published in 1996.
Proved fully abstract by Guy McCusker, 2002.
• 1994 – “Passivity and Independence:” a mathematically
cleaner version of the model.
• 1995 – Extended to general imperative programs
(joint work with Peter O’Hearn).
–
Proved fully abstract up to second-order types.
• 1998 – Application to object-oriented programs.
• 2003 – A model for heap variables (joint work with Hongseok
Yang).
10
Other Developments
• 1995 – Samson Abramsky refines my model into a
“games” model.
– Proves it intensionally fully abstract (joint work with Guy
McCusker).
• 1998 – Abramsky, Honda and McCusker apply the
same ideas to heap variables.
– Again proved intensionally fully abstract.
11
Other Developments
• 1995 – The structure identified in “Passivity and
Independence” also found to be present in an older
model of O’Hearn and Tennent.
– “Syntactic Control of Interference Revisited.”
• This model also has a “doubly-closed” structure.
(Two forms of conjunction and implication).
• 1999 – Leads to the logic of “Bunched Implications.”
12
Other Developments
• 1995 – In joint work with John Gray, found that
“strict” state-transformation functions give a
model with similar effect as my model.
• 1997 – O’Hearn and Reynolds generalize the idea
to “linear” functions.
Prove it fully abstract up to second-order types.
13
Full Abstraction
“Reddy’s model was therefore the first example of a fully
abstract semantics for a higher-order imperative language,
though this was not known at the time; and it remains the
only fully abstract model for an interference-controlled
language that we are aware of.”
- Guy McCusker, 2002
14
This Talk
• Focus on one of the issues that I had to grapple
with:
Mathematical and Physical entities
• What it means in
– philosophical and
– scientific terms.
• What it might mean for Computer Science as a
discipline.
15
Mathematical and Physical
The Science of Computing, in its origin, could
be said to be a branch of Mathematics.
• Mathematicians did calculations.
• Developed algorithms for calculations.
• Organized large-scale computations
(via “human computers”).
• Used early automatic computers to do
mathematical calculations.
16
Insert
logarithms book
picture from
Cogwheel Brain.
"I wish to God these calculations had been
executed by steam!”
- Charles Babbage, 1821.
17
Difference Engine No. 1
Partly built in 1834.
Cost £17,478.
(The equivalent of 22
steam locomotives!)
Would have cost another
£15,000 for completion.
18
Difference Engine No. 2
Built in 1991 using
Babbage’s designs.
Cost £240,000.
19
Computers are used today for a variety of
applications that are not purely mathematical.
Help fly
airplanes.
20
Control
spacecraft
21
Control
satellites
22
Air
traffic
control
23
Railway
control
24
Keck Observatory
Deformable mirror that
changes its shape
670 times per second
to account for atmospheric
distortion.
25
Consumer devices
26
• Computers are also used for a variety of
applications such as:
– Banking
– Trading
– Information Systems
• Modeling abstract entities with a “physical sense.”
27
The Mathematical and The Physical in
Computer Programs
28
Programming Languages
• Physical paradigm
(Imperative programming)
– Based on mutable entities:
“variables”.
– Actions for modifying such
entities.
•
Sources of inspiration:
–
–
–
–
Traditional algorithms
Instruction manuals
Recipe books
Turing machine model
• Mathematical paradigm
(Functional programming)
– Based on functions for
calculation
•
Sources of inspiration:
– Recursive function theory
– Lambda calculus model
– Denotational semantics of
programming languages
29
Imperative paradigm
Example: To sum a series of numbers
[ 5 20 -6 7 42 ]
0
ACC
ACC is a variable
(memory location,
a “physical” entity)
Repeatedly apply the rule:
ACC  ACC + {list element}
30
Imperative paradigm
Example: To sum a series of numbers
[ 5 20 -6 7 42 ]
0
ACC
+
31
Imperative paradigm
Example: To sum a series of numbers
[ 5 20 -6 7 42 ]
5
ACC
+
32
Imperative paradigm
Example: To sum a series of numbers
[ 5 20 -6 7 42 ]
25 ACC
+
33
Imperative paradigm
Example: To sum a series of numbers
[ 5 20 -6 7 42 ]
19 ACC
+
34
Imperative paradigm
Example: To sum a series of numbers
[ 5 20 -6 7 42 ]
26 ACC
+
35
Imperative paradigm
Example: To sum a series of numbers
[ 5 20 -6 7 42 ]
68 ACC
{ let ACC  an integer variable;
for each list element do
ACC  ACC + “list element”;
}
36
Functional paradigm
SUM [ 5 20 -6 7 42 ]
= 5 + SUM [ 20 -6 7 42 ]
= 5 + 20 + SUM [ -6 7 42 ]
= 5 + 20 + (-6) + SUM [ 7 42 ]
= 5 + 20 + (-6) + 7 + SUM [ 42 ]
No variables
involved.
No actions to be
described.
= 5 + 20 + (-6) + 7 + 42 + SUM [ ]
= 5 + 20 + (-6) + 7 + 42 + 0
= 68
Pure calculation!
37
What is a mathematical entity?
• Mathematicians themselves have not produced a
definition of the idea.
• We can try to generalize from the kinds of things
mathematicians study:
– numbers, sets, functions, predicates.
– Geometric objects: points, lines, shapes.
• Generalizing:
“ideas,” “abstractions,” “concepts,”
“Platonic” entities?
• Not tied to time or space.
• Freely transportable from one context to another
(“copyable” and “discardable”).
38
And, what about physical entities?
• Examples:
– Particles, fluids
– Coins, currency
– People, machines
• Also, abstractions of physical entities:
– Bank accounts
• Generalizing:
“objects”, “things”, “materials”,
“agents”.
39
Physical Entities
• Physical objects have “identity” that persists
through time.
• They cannot be copied or duplicated.
• Actions might involve changing state within an
available space of states.
• They might also involve transformation or
reconfiguration.
• Objects might have a limited life span
(get created and destroyed).
Happens often in computer programs.
40
Philosophical Interlude
• Propounded a Theory of Ideas.
• A “real” world of unique ideas.
• Physical world is an imperfect
reflection of it.
Plato
On Astronomy
“These sparks that paint the sky,… we must recognize that
they fall far short of the truth,… These can be
apprehended only by reason and thought, not by sight.
[Therefore] we must use the blazonry of the heavens as
patterns to aid in the study of those realities…”
41
Philosophical interlude
Aristotle admitted an external world.
Universals
abstract concepts
properties
Particulars
substances
“that is called universal which is such
as to belong to more than one thing.”
42
Philosophical Interlude
• “Universal” and “particular” continue to be used in
philosophical parlance.
• Roughly correspond to “mathematical” and “physical” in my
terminology.
• The characterization of “particulars” is very much a live
topic, cf. Russell’s theory of “bundles.”
• Universals are just referred to as “properties.”
• Do mathematicians accept that everything they study is a
“property” of other things that they don’t study?
43
Newtonian Modeling
Physical system
State space
Philosphiae
Naturalis
Principia
Mathematica
44
Mathematical Semantics
of Computer Languages
• Mutable physical systems go through states.
state = instantaneous description of
the system configuration
A mathematical entity!
• Actions as state transformation functions.
Action = [State  State]
• The basis of Christopher Strachey’s
modeling of programming languages,
1971.
45
Shortcomings of Strachey’s Modeling
Works well for
“global variables.”
Need support for “objects” and
“ownership” of locations.
Full abstraction fails for this reason.
{ let ACC  an integer variable;
…………
p( );
…………
External procedure
}
46
Possible World Model
The set of locations is not fixed.
The “world” can grow when new
locations are allocated.
John Reynolds
Further
development by:
Frank Oles
Bob Tennent
Peter O’Hearn
47
Possible World Model
Worlds
Semantic spaces
48
Possible World Model
• For every world W:
Action(W) = [State(W)  State(W)]
• Major conceptual leap:
S IM PLE T YPES
PO S S IBLE W O RLD S
(S T R A C H E Y )
(R E Y N O L D S )
A c tio n is a se t
A c tio n : W o rld s  S e ts
(a “fu n c to r”)
O p e ra tio n s o n S e ts:
A  B , [A  B ]
P ro g ra m p h ra se s
d e n o te fu n c tio n s
O p e ra tio n s o n F u n c to rs:
F  G , [F  G ]
P ro g ra m p h ra se s
n a tu ra l tra n sfo rm a tio n s
49
Possible World Model
• These “functors” are remarkably like ordinary
sets.
• They have a standard set theory based on
intuitionistic logic.
• Well-studied in category theory.
• Remarkable that they fit so well with the
programming language setting.
50
But all is not well!
• The possible world model should have worked, but it did not.
• Simple counter-examples to full abstraction.
• The problem was that category theory didn’t do its job.
– The mathematics was inadequate to reflect the intuitions.
• [O’Hearn and Tennent, 1993]
“Relational parametricity and local variables.”
• Brian Dunphy’s Ph.D. thesis shows that this is just categorytheory fixed up.
51
The Period 1990-93
• The possible world model was losing accuracy for unknown
reasons!
• Is the enterprise of building “mathematical” models for
physical entities doomed?
• Should we look for a more direct approach to modeling
physical entities?
• April/May 1992: Found a solution, two months before I
learnt of the O’Hearn-Tennent work.
• Took another two years to polish it and make it
understandable.
52
Girard’s Linear Logic
• The beginnings of a mathematical framework for
incorporating physical entities.
• Normally, parameter symbols can be used many times:
2x
2
 5x  7
• Linear language: a parameter has to be used exactly once.
5x  7 y
• Seems like an impoverished language. Girard’s genius was
essential for making a useful system out of it!
• Girard’s explanation: The linearly used parameters are
“resources” which are “used up” when they occur in formulas.
53
Girard’s Linear Logic
• The ideas of “resource” and “physical entity” are
close.
• Most linear logic models, however, involve a
“process” interpretation.
• All mathematical entities get reinterpreted as
computational processes, interacting with other
such processes.
54
Object-based Model
Object:
a programming abstraction that
encapsulates physical resources and
exports operations to manipulate them.
Everything that occurs in an imperative programming language
is an object: (Variables, commands, expressions and
other higher-type entities).
55
Object-based Model
A (pure) function on objects makes an
object look like another one.
56
Object-based Model
Function objects give rise to composition:
A
A
B
A
AB
“Composition as interaction” -- Samson Abramsky
57
Mathematical models for Objects
A number of models for linear logic:
Proof nets, Event-based models,
Geometry of Interaction, Games
Event: represents a single complete interaction
between an object and its environment.
[Plotkin, Nielsen, Winskel]
Again a “mathematical” entity!
A
A
B
58
Mathematical models for Objects
The observable behavior of an object can be
defined as a set of event sequences (“traces”).
(deposit,30)
(deposit,100)
(deposit,20)
(balance,150)
(balance,120)
(balance,20)
(balance,0)
A trace of a Bank Account object
59
Mathematical models for Objects
The observable behavior of an object can be
defined as a set of event sequences (“traces”).
(deposit,30)
(deposit,100)
(deposit,20)
(balance,150)
(balance,120)
(balance,20)
(balance,0)
A trace of a Bank Account object
60
Mathematical models for Objects
deposit
100

Games models
split up the
“events” into
more primitive
“moves.”
balance?
Allow the
distinction
between inputs
and outputs.
20
61
Sharing, not Copying!
The basic “event” model does not allow sharing.
Games models do.
[O’Hearn and Reddy, 1995]
Possible world model using objects for worlds!
62
Philosophical Postlude
… the objects which are mathematically
primitive in physics, such as electrons,
protons, and points in space-time, are all
logically complex structures composed of
entities which are metaphysically more
primitive, which may be conveniently called
“events.”
-- The Analysis of Matter, 1927.
Bertrand
Russell
63
Is Computer Science
• a Mathematical Science or
• a Physical Science?
Computer Science deals with abstract concepts, like
Mathematics does.
It also deals with physical entities, like Physical Sciences do.
Constitutes a synthesis of the two kinds of entities, giving rise
to new abstractions of physical entities!
64
Thanks
Peter O’Hearn, Bob Tennent, John Reynolds.
Samson Abramsky, Radha Jagadeesan, Guy McCusker.
Dick Kieburtz, Phil Wadler, Christian Retoré.
Sam Kamin, Brian Dunphy, Hongseok Yang.
………… And all my friends and colleagues
from whom I have learnt a great deal.
65
Thank You!
66
Descargar

Programming With the Mathematical and Physical