A Type Theory with Partially Defined Functions

Book English OPEN
Luo, Yong (2005)
  • Publisher: UKC
  • Subject: QA76

Only can totally defined functions be introduced in conventional dependently typed systems and such functions are normally defined by eliminators. Because of the limitation of the elimination rules, many (mathematical) functions cannot be defined in these systems. This paper argues that the restriction of totality is unnecessary, and proposes a type theory that allows partially defined functions. In this type theory, functions can be introduced by means of pattern matching. It is in general undecidable in dependently typed systems whether patterns cover all the canonical objects of a type, and it is one of the big problems for implementation. Without the restriction of totality, we don't have such problem of totality checking, and hence we have more flexibility to introduce functions than we do in conventional type systems.
  • References (26)
    26 references, page 1 of 3

    [Alt93] Th. Altenkirch. Constructions, Inductive Types and Strong Normalization . PhD thesis, Edinburgh University, 1993.

    [B+00] B. Barras et al. The Coq Proof Assistant Reference Manual (Version 6.3.1) . INRIA-Rocquencourt, 2000.

    [Bar84] H.P. Barendregt. The Lambda Calculus: its Syntax and Semantics. NorthHolland, revised edition, 1984.

    [Bar92] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Clarendon Press, 1992.

    [C+86] R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Pretice-Hall, 1986.

    [Coq92] Th. Coquand. Pattern matching with dependent types. Talk given at the BRA workshop on Proofs and Types, Bastad, 1992.

    [Geu93] Herman Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993.

    [Gog94] H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.

    [HHP87] R. Harper, F. Honsell, and G. Plotkin. A framework for dening logics. Proc. 2nd Ann. Symp. on Logic in Computer Science. IEEE, 1987.

    [HHP92] R. Harper, F. Honsell, and G. Plotkin. A framework for dening logics. Journal of ACM, 40(1):143184, 1992.

  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    Kent Academic Repository - IRUS-UK 0 10
Share - Bookmark