Types and operations

• Autorzy: Ambroszkiewicz S.

Warianty tytułu

PL

Typy i operacje

• Języki publikacji: EN

Abstrakty

EN

A revision of the basic concepts of type, function (called here operation), and relation is proposed. A simple generic method is presented for constructing operations and types as concrete finite structures parameterized by natural numbers. The method gives rise to build inductively so called Universe intended to contain all what can be effectively constructed at least in the sense assumed in the paper. It is argued that the Universe is not yet another formal theory but may be considered as a grounding for some formal theories.

PL

Zaproponowana została rewizja podstawowych pojęć typu i funkcji (nazywanej tutaj operacją). Typy, obiekty tych typów oraz operacje są konstruowane za pomocą prostej i uniwersalnej metody jako skończone struktury parametryzowane liczbami naturalnymi. Metoda ta pozwala na budowanie tzw. Uniwersum, które, w zamierzeniu, ma zawierać wszystko co jest efektywnie konstruowalne przynajmniej w sensie, jaki jest przyjęty w tej pracy. Przedstawione są argumenty, że Uniwersum nie jest jeszcze jedną formalną teorią, lecz może służyć jako ugruntowanie dla pewnych formalnych teorii.

Słowa kluczowe

EN

types; semantics; foundations

PL

typy; semantyka; podstawy

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2014
• Tom: Nr 1030
• Strony: 1--72
• Opis fizyczny: Bibliogr. 40 poz., rys.

Twórcy

autor

Ambroszkiewicz S.

• Instytut Podstaw Informatyki PAN, ul. Jana Kazimierza 5, 01-248 Warszawa, Polska

Bibliografia

• [1] J. Adamek, S. Milius, and J. Velebil. Semantics of higher-order recursion schemes. Logical Methods in Computer Science, 7(1:15):1— 43, 2011.
• [2] Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. Preprint, 2013.
• [3] Ana Bove and Venanzio Capretta. Modelling general recursion in type theory. Math. Struct, in Comp. Science, 15:671-708, 2005.
• [4] T. Coquand. Coq proof assistant, chapter 4 calculus of inductive constructions. www http://coq.inria.fr/doc/Reference-Manual006.html, 2014. Site on www.
• [5] T. Coquand and Gerard Huet. The calculus of constructions. Technical Report RR-0530, INRIA, May 1986.
• [6] Thierry Coquand and Gerard Huet. The calculus of constructions. Inf. Comput, 76(2-3):95-120, February 1988.
• [7] Haskell B. Curry. Combinatory recursive objects of all finite types. Bull. Amer. Math. Soc, 70(6):814-817, 1964. http:// projecteuclid.org/euclid.bams /1183526340.
• [8] Haskell B. Curry and Robert Feys. Combinatory Logic, volume 1. Amsterdam: North Holland, 1958.
• [9] Gerhard Gentzen. Untersuchungen uber das logische Schliessen I and II. Mathematische Zeitschrift, 39:176-210, 405-431, 1934.
• [10] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science), 1990.
• [11] J.Y. Girard. Une extension de l'interpretation de godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et dans la theorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium 1971.
• [12] K. Godel. Uber eine bisher noch nicht beniitzte erweiterung des finiten standpunktes. Dialectica, 10:280 - 287, 1958.
• [13] A. Grzegorczyk. Computable functionals. Fundamenta Mathematicae, 42:168-202, 1955.
• [14] A. Grzegorczyk. On the definition of computable functionals. Fundamenta Mathematicae, 42:232-239, 1955.
• [15] A. Grzegorczyk. On the definitions of computable real continuous functions. Fundamenta Mathematicae, 44:61-71, 1957.
• [16] A. Grzegorczyk. Recursive objects in all finite types. Fundamenta Mathematicae, 54:73-93, 1964.
• [17] R. Harper. What is the big deal with HoTT? http://existentialtype.wordpress.com/2013/06/22/whats-the-big-deal-with-hott /.
• [18] D. Hilbert. Gesammelte Abhandlungen, volume 3. Berlin, 1935.
• [19] Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Proceedings. 14th Symposium on Logic in Computer Science, pages 204-204. IEEE Computer Society, 1999.
• [20] Stanislaw Jaskowski. Teoria dedukcji oparta na regulach zalozeniowych (theory of deduction based on suppositional rules). In Ksiega pamiatkowa pierwszego polskiego zjazdu matematycznego (Proceedings of the First Polish Mathematical Congress), 1927, page 36. Krakow: Polish Mathematical Society, 1929.
• [21] Stanislaw Jaskowski. On the rules of suppositions in formal logic. Studia Logica, 1:5-32, 1934.
• [22] Tomasz Kaczynski, Konstantin Mischaikow, and Marian Mrozek. Computational Homology- Springer-Verlag, 2004.
• [23] S. C. Kleene. Countable functionals. Constructivity in Mathematics: Proceedings of the colloquium held at Amsterdam, pages 81-100, 1959.
• [24] S. C. Kleene. Recursive functionals and quantifiers of finite types i. Transactions of the American Mathematical Society, 91:1-52, 1959.
• [25] S. C. Kleene. Recursive functionals and quantifiers of finite types ii. Transactions of the American Mathematical Society, 108:106-142, 1963.
• [26] G. Kreisel. Interpretation of analvsis of means of functionals offinite type,. Constructivity in Mathematics: Proceedings of colloquium held at Amsterdam, pages 101-128, 1959.
• [27] D. Lacombe. Remarques sur les operateurs recursifs et sur les fonctions recursives d'une variable reelle. Comptes Rendus de VAcademie des Sciences, Paris, 241:1250-1252, 1955.
• [28] P. Martin-L6f. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloqium 1973.
• [29] L. C. Paulson. Constructing recursion operators in intuitionistic type theory. J. Symbolic Computation, 2:325-355, 1986.
• [30] Rozsa Peter. Recursive functions. Elsevier Science Publishing Co Inc„ 1967.
• [31] J. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation 1974, pages, 408-425. Paris, Prance, 1074.
• [32] Barkley Rosser. An Informal Exposition of Proofs of Godel's Theo¬rems and Church's Theorem. Journal of Symbolic Logic, (2):53-60, 06.
• [33] Carsten Schiirmann, Joelle Despeyroux, and Frank Pfenning. Fundamental study, primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 266:1-57, 2001.
• [34] D. S. Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, 121,:411-440, 1969.
• [35] D. S. Scott. A theory of computable functions of higher type. University of Oxford, 1969.
• [36] D. S. Scott. Outline of mathematical theory of computation.Technical Monograph PRG-2, 1970.
• [37] A. Tarski. Logic, Semantics, Metamathematics, papers from 1923 to 1938. Indianapolis: Hackett Publishing Company, 1983.
• [38] A.S. Troelstra. History of constructivism in the 20th century, in set theory, arithmetic, and foundations of mathematics, theorems, philosophies. Lecture Notes in Logic, 36:7-9, 2011.
• [39] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study,http://homotopytypetheory.org/book, 2013.
• [40] Vladimir Voevodsky. The origins and motivations of univalent foundations. IAS - The Institute Letter. Summer 2014, Institute for Advanced Study, Princeton, NJ, USA, pages 8-9, 2014.