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

1/--страниц