Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Wherefore Art Thou Semantics of Computation? Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

From urelements to Computation

A Journey Through Applications of Fraenkel’s Permutation Model in Computer Science

verfasst von : Vincenzo Ciancia

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
loading …

Abstract

Around 1922-1938, a new permutation model of set theory was defined. The permutation model served as a counterexample in the first proof of independence of the Axiom of Choice from the other axioms of Zermelo-Fraenkel set theory. Almost a century later, a model introduced as part of a proof in abstract mathematics fostered a plethora of research results, ranging from the area of syntax and semantics of programming languages to minimization algorithms and automated verification of systems. Among these results, we find Lawvere-style algebraic syntax with binders, final-coalgebra semantics with resource allocation, and minimization algorithms for mobile systems. These results are also obtained in various different ways, by describing, in terms of category theory, a number of models equivalent to the permutation model.
We aim at providing both a brief history of some of these developments, and a mild introduction to the recent research line of “nominal computation theory”, where the essential notion of name is declined in several different ways.

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
Vorheriges Kapitel «Omnia Numerorum Videntur Ratione Formata». A ‘Computable World’ Theory in Early Medieval Philosophy
Nächstes Kapitel The Contribution of Carl Adam Petri to Our Understanding of ‘Computing’
Fußnoten
1
It is worth noting that after the adoption of the nominal methods that we are discussing in this section, several extensions of traditional functional languages appeared, where binding and alpha-equivalence are part of the language; see e.g. [41].
 
2
Additionally, in \( FM \)-sets it may happen that the action of some (but not all) permutations affecting urelements in the support of an element leave such element unchanged. By this, \( FM \)-sets also exhibit symmetry (see e.g. [8, 39] for more details).
 
3
And a group of permutations on the registers, which is required for minimization purposes; we are deliberately hiding this aspect under the carpet as it is too technical for the scope of this paper, but we leave this remark as a pointer for the reader interested in symmetry in computation (see [8] for more details).
 
4
There also are operations mapping a type to another, playing the same role as permutations in \( FM \); in our mild introduction, we omit the technical details, referring the interested reader to the references for more details.
 
Literatur
1.
Bojanczyk, M., Klin, B., Lasota, S., Torunczyk, S.: Turing machines with atoms. In: 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS), pp. 183–192. IEEE Computer Society (2013)
2.
Bojanczyk, M., Klin, B., Lasota, S.: Automata with group actions. In: Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science, LICS 2011, pp. 355–364. IEEE Computer Society (2011)
3.
Bonchi, F., Buscemi, M.G., Ciancia, V., Gadducci, F.: A presheaf environment for the explicit fusion calculus. J. Autom. Reasoning 49(2), 161–183 (2012)MathSciNetCrossRefMATH
4.
5.
6.
Ciancia, V., Kurz, A., Montanari, U.: Families of symmetries as efficient models of resource binding. Electron. Notes Theor. Comput. Sci. 264(2), 63–81 (2010)MathSciNetCrossRefMATH
7.
Ciancia, V., Montanari, U.: A name abstraction functor for named sets. Electron. Notes Theor. Comput. Sci. 203(5), 49–70 (2008)MathSciNetCrossRefMATH
8.
Ciancia, V., Montanari, U.: Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput. 208(12), 1349–1367 (2010)MathSciNetCrossRefMATH
9.
Ciancia, V., Sammartino, M.: A class of automata for the verification of infinite, resource-allocating behaviours. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 97–111. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-45917-1_​7
10.
Ciancia, V., Tuosto, E.: A novel class of automata for languages on infinite alphabets. Technical report, Technical Report CS-09-003, Leicester (2009)
11.
Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. ACM Trans. Softw. Eng. Methodol. 12(4), 440–473 (2003)CrossRef
12.
Ferrari, G., Montanari, U., Tuosto, E.: Coalgebraic minimization of hd-automata for the \(\pi \)-calculus using polymorphic types. Theor. Comput. Sci. 331(23), 325–365 (2005)MathSciNetCrossRefMATH
13.
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings of 14th Symposium on Logic in Computer Science, pp. 193–202. IEEE Computer Society (1999)
14.
15.
Fiore, M., Moggi, E., Sangiorgi, D.: A fully-abstract model for the pi-calculus. In: Proceedings of Eleventh Annual IEEE Symposium on Logic in Computer Science, LICS 1996, pp. 43–54. IEEE Computer Society (1996)
16.
Fraenkel, A.: Der Begriff “definit” und die Unabhängigkeit des Auswahlaxioms. Berl. Ber. 1922, 253–257 (1922)MATH
17.
Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: Proceedings of 14th Symposium on Logic in Computer Science, pp. 214–224. IEEE Computer Society (1999)
18.
19.
Gadducci, F., Miculan, M., Montanari, U.: About permutation algebras, (pre)sheaves and named sets. High.-Order Symbolic Comput. 19(2–3), 283–304 (2006)CrossRefMATH
20.
Jacobs, B., Silva, A.: Initial algebras of terms with binding and algebraic structure. In: Casadio, C., Coecke, B., Moortgat, M., Scott, P. (eds.) Categories and Types in Logic, Language, and Physics. LNCS, vol. 8222, pp. 211–234. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54789-8_​12 CrossRef
21.
Kaminski, M., Francez, N.: Finite-memory automata (extended abstract). In: 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, 22–24 October 1990, vol. 2, pp. 683–688. IEEE Computer Society (1990)
22.
Klin, B., Lasota, S., Ochremiak, J., Toruńczyk, S.: Turing machines with atoms, constraint satisfaction problems, and descriptive complexity. In: CSL-LICS 2014, pp. 58: 1–58: 10. ACM (2014)
23.
Kozen, D., Mamouras, K., Petrişan, D., Silva, A.: Nominal Kleene coalgebra. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 286–298. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-47666-6_​23
24.
Kozen, D., Mamouras, K., Silva, A.: Completeness and incompleteness in nominal Kleene algebra. In: Kahl, W., Winter, M., Oliveira, J.N. (eds.) RAMICS 2015. LNCS, vol. 9348, pp. 51–66. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-24704-5_​4 CrossRef
25.
26.
27.
28.
Milner, R.: A Calculus of Communicating Systems. Springer-Verlag New York, Inc., New York (1982)MATH
29.
Milner, R.: Whats in a name? In: Herbert, A., Jones, K. (eds.) Computer Systems. Monographs in Computer Science, pp. 205–209. Springer, New York (2004)CrossRef
30.
31.
Montanari, U., Pistore, M.: \(\pi \)-calculus, structured coalgebras, and minimal HD-automata. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 569–578. Springer, Heidelberg (2000). doi:10.​1007/​3-540-44612-5_​52
32.
Montanari, U., Sammartino, M.: A network-conscious -calculus and its coalgebraic semantics. Theor. Comput. Sci. 546, 188–224 (2014)MathSciNetCrossRefMATH
33.
Moore, G.: Zermelo’s Axiom of Choice: Its Origins, Development, and Influence. Studies in the History of Mathematics and Physical Sciences. Springer-Verlag, New York (1982)CrossRef
34.
Mostowski, A.: Uber den Begriff einer Endlichen Menge. Comptes rendus des sances de la Socit des Sciences et des Lettres de Varsovie, Classe III 31(8), 1320 (1938)
35.
Murawski, A., Ramsay, S., Tzevelekos, N.: Bisimilarity in fresh-register automata. In: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 156–167. IEEE Computer Society (2015)
36.
Needham, R.M.: Distributed Systems. ACM, New York (1989). pp. 89–101
37.
Pistore, M.: History Dependent Automata. Ph.D. thesis, Università di Pisa, Dipartimento di Informatica (1999)
38.
39.
Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, Cambridge (2013)CrossRefMATH
40.
41.
Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programming with binders made simple. In: ICFP 2003, pp. 263–274. ACM (2003)
42.
Tzevelekos, N.: Fresh-register automata. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 295–306. ACM (2011)
43.
Metadaten
Titel
From urelements to Computation
verfasst von
Vincenzo Ciancia
Copyright-Jahr
2016
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_10