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 AB “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