nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Wherefore Art Thou \(\ldots \) Semantics of Computation?

verfasst von : Furio Honsell

Erschienen in: History and Philosophy of Computing

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Nearly 60 years have passed since the notion of semantics was first used to explain Programming Languages. There was quite some divergence of opinions, at the time, in what the semantics of semantics was supposed to be. Today, in face of the plethora of different models and logical systems based thereupon, are we in a better position to address this socratic question? We analyse philosophical issues revolving around the Foundations of Formal Reasoning, Proof Cultures, Logical Frameworks, the Algebraic/Co-algebraic Duality, and Games. We put forward the thesis that, rather than being a drawback, plurality is what makes Semantics useful. In that Semantics of Computation is a “partita doppia”, a double check of what we think we understand in computing.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nächstes Kapitel Logic, Formal Linguistics and Computing in France: From Non-reception to Progressive Convergence

J. Backus, in 1959, used it explicitly in the title of the paper [12].

Bearing in mind [44], I speak here of “Computing” rather than “Computer Science”.

In Constructive Logic a formal proof of \(\forall x. \exists y. P\) contains an algorithm for computing y given x. E.g. the proof that primes are infinitely many contains a method for finding a prime larger than any one in a given list. B. Constable, the founder of Nuprl, mentioned this intriguing example: any finite list of integers has a subsequence of consecutive elements with a largest sum. A natural inductive proof of this obvious fact contains a linear algorithm for computing the largest sum, but if we do not follow the program-extraction approach we easily slip into a quadratic algorithm.

Viz. terms, variables, binders, schemata, rules, assumptions, proofs, theorems, etc.

Consider for instance e.g. Karatsuba’s multiplication. Already Babbage knew that: if \(x = x_1 B^m +x_0\), \(y = y_1 B^m +y_0\) then \(xy = x_1y_1B^{2m}+ (x_1y_0 + x_0y_1)B^m + x_0y_0\) but he failed to notice the optimization behind \( x_1y_0 + x_0y_1 = (x_1+x_0)(y_1+y_0) - x_1y_1 - x_0y_0\).

Look at Matita Proof Assistant’s logo.

Here is an intriguing list of problems which utilize arguments by analogy:

- Archimedes in his Organon [2] rather than giving a geometrical account of physical phenomena went the opposite way. He utilized physical analogies for addressing mathematical problems and anticipated calculus. His method was to conceive a geometrical figure as composed of thin slices, to which he assigned physical features and which he imagined to hang on a balance scale subject to gravity.

- Given any point inside a convex polyhedron, there exists a face of the polyhedron such that the projection of the point onto the plane of that face lies inside the face, for otherwise we would have a pepetuum mobile.

- Leibniz suggested to find the point of an acute triangle which has smallest sum of the distances to the vertices of the triangle by hanging equal weights to 3 threads passing through the vertexes, tied all three together in a single knot. The equlibrium point is reached when the potential energy is minimal.

- The towns A and B are separated by a straight river. In what place should we construct a bridge MN, orthogonal to the shores, in order to minimize the length of the road AMNB? Minimal paths are immediate once we think of them as light beams. The bridge corresponds to the refraction caused by a very dense medium.

- Induction per se does not appear in Euclid. Even the proof of the so-called Euclid’s Algorithm is carried out only up to 3. We conjecture that this is due to the fact that the Greek language, has dual, as well as plural endings. Three is already a multitude!.

This is nicely expressed by the following puzzle: what is the difference between solving a Sudoku using pencil and eraser by backtracking, rather than using a pen and writing a number only if a stringent argument forces it? The latter solution proves also uniqueness.

The alphabetical order of the name of the months.

The series can be read as 1, hence 1 one; hence 3 one’s; hence 4 ones’s, 0 two’s, and 1 three; so the next counting gives 6 one’s.

My favourite example is the following which wittily mocks racism: Who among the following five men is the alien? The first has blue eyes, white skin, medium height, and average build. The second has dark skin and eyes, medium height, and average build. The third has white skin, dark eyes, medium height, and average build. The fourth has short legs, white skin, dark eyes, and average build. Finally the fifth is overweight, has dark eyes, white skin and medium height. The third man is the alien since he shares 3 characteristics out of 4 with any of the others, while each of the others shares only 2.

Gramsci said: “Conformism means nothing else but sociality, but I prefer to use “conformism” to irritate imbeciles!”.

The mathematical notion of sieve, is immediately programmed on streams.

- most English grammars are written in English;

- \(\ldots \) from the catalogue of a recent exhibition on analytic painting: “The result are paintings which are remarkable for the self-referentiality of their language” - \(\ldots \) from the catalogue of a cinema festival “\(\ldots \) every citation of a movie is a reflection on cinema itself, targeted to educate the audiences capable of deciphering the metatheory of cinema”;

- the mise en abîme in paintings and stories, the most remarkable example being the Mousetrap in Shakespeare’s Hamlet;

- there is no History without Historiography;

- Mythology can be defined as the way a culture narrates itself;

- self-awareness has been recommended since antiquity: Know thyself; and it has been taken as the cornerstone of phylosophical systems, e.g. Cogito ergo sum;

- the third man paradox in Plato’s Parmenides undermines the theory of ideas;

- the formal accounts of such notions as conventions, common knowledge, intentionality, fashion, and statistics usually involve self-reference in an essential way;

- many epistemic logic paradoxes arise from self referentiality;

- an ostensible definition of recursion: “recursion”: viz recursion;

- the power of equations, and implicit definitions ¹⁵ and fixed point theorems;

- a mind emerging from a brain which is an invention of the mind;

- Akbar the Moghul emperor, who championed tolerance, secularism, and reason, already at the end of the XVI\(^{\text{ th }}\) century, made the point that even to dispute reason one has to give a reason for that disputation;

- the circular assumption (X): if A, B, C, and X are true then Z is true could stop the infinite regress in Carroll’s anecdote in [15];

- impredicativity, say of reals, can be taken as a strong point of the theory;

- the set of concepts I mentioned in this list.

Stimulating puzzles are: the probability that the first outcome of tails will occurr after an even number of throws; and Ramanujam’s nested radical \(\sqrt{1 + 2\sqrt{1 + 3\sqrt{1 + \ldots }}}\).

I thank U. Zannier from the Scuola Normale Superiore in Pisa for pointing it out.

This is a very inspiring passage: “En reprenant la métaphore théâtrale, on pourrait rapprocher le contexte des processus où opèrent les notions algébriques du théâtre classique, où un petit nombre de protagonistes mène l’action dans un champ spatio-temporel circonscrit. Le contexte où opèrent les notions co-algébriques serait analogue, lui à ces opéras où le protagoniste est un peuple, et où de scéne en scéne, les changements d’états sont marqué s d’intégrales de destins.”.

In Stone spaces, i.e. compact totally disconnected Hausdorff spaces, a point is the filter of the clopen sets, which are a Boolean algebra, to which it belongs.

The game where player I first chooses a terminating game, then Player II starts playing that game, cannot exist because it is terminating, but if it were terminating then player I could choose this very game.

The following lateral thinking puzzle makes the point by showing that all games can be played in the misère version. “Two jockeys were tired of competing to see who had the fastest horse. So, one day, they decided to take up the opposite challenge: who has the slowest horse? But the race would never start, until \(\ldots \) someone suggested to \(\ldots \)!” The answer is to “swap horses”.

A simple example is race-to-twenty: starting from \(n\le 20\) the players add either 1 or 2, in turns, to the current sum. The first to reach 20 is the winner.

Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C.: Selected Papers on Automath, vol. 133. Studies Logic, Elsevier, Amsterdam (1984)MATH

Archimede: Metodo. Nel laboratorio di un genio. Bollati Boringhieri (2013)

Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Logic 51(1), 1–77 (1991)MathSciNetCrossRefMATH

Abramsky, S., Jagadeesan, R.: New foundations for the geometry of interaction. Inf. Comput. 111(1), 53–119 (1994)MathSciNetCrossRefMATH

Abramsky, S.: Retracing some paths in process algebra. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 1–17. Springer, Heidelberg (1996). doi:10.1007/3-540-61604-7_44 CrossRef

Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)MathSciNetCrossRefMATH

Abramsky, S., Lenisa, M.: Linear realizability and full completeness for typed lambda-calculi. Ann. Pure Appl. Logic 134(2–3), 122–168 (2005)MathSciNetCrossRefMATH

Abramsky, S.P.: A structural approach to reversible computation. Theor. Comput. Sci. 347(3), 441–464 (2005)MathSciNetCrossRefMATH

Aczel, P.: Non-Well-Founded Sets. CSLI LN 14, Stanford (1988)

10.

Aczel, P.: Final universes of processes. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 1–28. Springer, Heidelberg (1994). doi:10.1007/3-540-58027-1_1 CrossRef

11.

André, Y.: Qu’est-ce que coagir?: pour une philosophie de la coaction. Notes d’exposé au Colloque Objet/Relation, ENS, Paris (2014)

12.

Backus, J.W.: The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM conference. In: Proceedings of the International Conference on Information Processing UNESCO, pp. 125–132. Typewritten preprint (1959)

13.

Badiou, A.: L’être et l’événement (1988)

14.

Barwise, J., Moss, L.S., Circles, V.: On the Mathematics of Non-Wellfounded Phenomena. CSLI LN 60, Stanford (1996)

15.

Carroll, L.: What the Tortoise Said to Achilles. Mind 4, 278–280 (1895)CrossRef

16.

Cardone, F., Hindley, R.: Lambda-calculus and combinators in the 20th century. In: Logic from Russell to Church, pp. 723–817 (2009)

17.

Conway, J.: On Numbers and Games. A. K. Peters, Natick (2000)MATH

18.

Huet, G., Coquand, T., Phlin-Mohring, C., Herbelin, H. et al.: The coq proof assistant. https://coq.inria.fr

19.

Dreyfus, H.L., Dreyfus, S.E.: Making a mind vs modeling a brain, artificial intelligence back at a branchpoint. Daedalus Art. Int. 117(1), 185–197 (1990)

20.

Di Gianantonio, P., Franco, G., Honsell, F.: Game semantics for Untyped \(\lambda \beta \eta \)-Calculus. In: TLCA 1999, SLNCS 1581 (1999)

21.

Egidi, L., Honsell, F., Ronchi, S.: Operational, denotational and logical descriptions: a case study. Fundam. Inform. 16(1), 149–169 (1992)MathSciNetMATH

22.

Lions, J.L.: Rapport de la Commission d’enqute Ariane 501 Echec du vol Ariane 501 (1997).http://www.capcomespace.net/dossiers/espace_europeen/ariane/ariane5/AR501/AR501_rapport_denquete.htm.

23.

Fitch, F.B.: Self-reference in philosophy. MInd 55(217), 64–73 (1946)CrossRef

24.

Forti, M., Honsell, F.: Set theory with free construction principles. Ann. Scuola Norm. Sup. Pisa 10(3), 493–522 (1983)MathSciNetMATH

25.

Steel, T.B. (ed.): Formal language description languages for computer programming. In: Proceedings of IFIP TC 2 Working Conference on Formal Language Description Languages, Vienna, 15–18 September 1964, North Holland (1966)

26.

Gadducci, F.: Graph rewriting for the \(\pi \)-calculus. MSCS 17(3), 407–437 (2007)MathSciNetMATH

27.

Gadducci, F., Montanari, U.: Comparing logics for rewriting: rewriting logic, action calculi and tile logic. Theor. Comput. Sci. 285(2), 319–358 (2002)MathSciNetCrossRefMATH

28.

Girard, J.-Y.: Linear logic. Theor. Comp. Sci. 50, 1–102 (1987)MathSciNetCrossRefMATH

29.

Girard, J.Y.: Geometry of interaction I: interpretation of system F. In: Logic Colloquium 1988, North-Holland (1989)

30.

Girard, J.-Y.: The Blind Spot: lectures on logic. Eur. Math. Soc. 2011, 537 pages (2011)MathSciNetMATH

31.

Gramsci, A.: Prison Notebooks. Columbia University Press, New York (1992)

32.

Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993)MathSciNetCrossRefMATH

33.

Honsell, F., Lenisa, M.: Conway games, algebraically and coalgebraically. Logical Meth. Comput. Sci. 7(3), 1–30 (2011)MathSciNetCrossRefMATH

34.

Honsell, F., Plotkin, G.D.: On the completeness of order-theoretic models of the lambda-calculus. Inf. Comput. 207(5), 583–594 (2009)MathSciNetCrossRefMATH

35.

Honsell, F.: 25 years of formal proof cultures: some problems, some philosophy. In: Proceeding of LFMTP 2013 ACM SIGPLAN Workshop, Boston (2013)

36.

Honsell, F., Lenisa, M.: Theories of Automatic Combinators (draft)

37.

Honsell, F., Liquori, L., Maksimović, P., Scagnetto, I.: LLFP: A Logical Framework for Modeling External Evidence using Monads, LMCS (2014, to appear)

38.

Jacobs, B., Rutten, J.J.M.M.: An introduction to (co)-algebras and (co)-induction. Cambridge Tracts in TCS 52, CUP (2011)

39.

Lenisa, M.: Themes in Final Semantics. Ph.D. Thesis CS Pisa, TD 6 (1998)

40.

Kripke, S.: Wittgenstein on Rules and Private Language. Blackwell, Oxford (1982)

41.

Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis, Napoli (1984)MATH

42.

Milner, R.: A calculus of communicating systems. In: SLNCS 92 (1980)

43.

Milner, R.: The use of machines to assit in rigorous proof. Phil. Lond. A Trans. R. Soc. 312(1522), 411–422 (1984)MathSciNetCrossRefMATH

44.

Milner, R.: Is Computing an Experimental Science? LFCS Inaugural Lecture (1986)

45.

Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inf. Comput. 100(1), 1–40 (1992)MathSciNetCrossRefMATH

46.

Moggi, E.: Notions of computation and monads. Inf. Comp. 93(1), 55–92 (1991)MathSciNetCrossRefMATH

47.

Plotkin, G.D.: Call-by-name, call-by-value and the \(\lambda \)-calculus. TCS 1(2), 125–159 (1975)MathSciNetCrossRefMATH

48.

Plotkin, G.: LCF considered as a programming language. TCS 5(3), 223–255 (1977)MathSciNetCrossRefMATH

49.

Poincaré, H.: La Science et l’Hypothèse. Flammarion, Paris (1902)

50.

Rutten, J., Turi, D.: On the foundations of final co-algebra semantics: non-well-founded sets, partial orders, metric spaces. MSCS 8(05), 481–540 (1998)MathSciNetMATH

51.

Rutten, J.: Universal co-algebra: a theory of systems. TCS 249(1), 3–80 (2000)MathSciNetCrossRefMATH

52.

Scherlis, W., Scott, D.: Semantically based programming tools. In: SLNCS 185 (1985)

53.

Scott, D.: Continuous lattices. In: Lawvere, F.W. (ed.) Dalhousie Conference on Toposes, Algebraic Geometry and Logic, SLNM 274 (1972)

54.

Scott, D.: Relating theories of the lambda calculus. lambda calculus and formalism. In: To H. B. Curry Essays in Combinagtory Logic. Academic Press, London (1980)

55.

Scott, D.S.: Domains for denotational semantics. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 577–610. Springer, Heidelberg (1982). doi:10.1007/BFb0012801 CrossRef

56.

Shopenhauer, A.: The World as Will and Representation (1844)

57.

Sen, A.: Sraffa, wittgenstein, and gramsci. J. Econ. Lit. 41(4), 1240–1255 (2003)CrossRef

58.

Smyth, M., Plotkin, G.: The category-theoretic solution of recursive domain equations. SIAM J. Comput. 11(4), 761–783 (1982)MathSciNetCrossRefMATH

59.

Turi, D., Plotkin, G.: Towards a Mathematical Operational Semantics. In: LICS 97. IEEE (1997)

Titel: Wherefore Art Thou Semantics of Computation?
verfasst von: Furio Honsell
Verlag: Springer International Publishing
Buch: History and Philosophy of Computing
Print ISBN: 978-3-319-47285-0

Electronic ISBN: 978-3-319-47286-7

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-47286-7_1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"