Akademska digitalna zbirka SLovenije - logo
VSE knjižnice (vzajemna bibliografsko-kataložna baza podatkov COBIB.SI)
  • Categorical completeness results for the simply-typed lambda-calculus
    Simpson, Alex
    We investigate, in a categorical setting, some completeness properties of beta-eta conversion between closed terms of the simply-typed lambda calculus. A cartesian-closed category is said to be ... complete if, for any two unconvertible terms, there is some interpretation of the calculus in the category that distinguishes them. It is said to have a complete interpretation if there is some interpretation that equates only interconvertible terms. We give simple necessary and sufficient conditions on the category for each of the two forms of completeness to hold. The classic completeness results of, e.g., Friedman and Plotkin are immediate consequences. As another application, we derive a syntactic theorem of Statman characterizing beta-eta conversion as a maximum consistent congruence relation satisfying a property known as typical ambiguity.
    Vir: Typed lambda calculi and applications : Second International Conference on Typed Lambda Calculi and Applications, TLCA'95 Edinburgh, United Kingdom, April 10-12, 1995 : proceedings (Str. 414-427)
    Vrsta gradiva - prispevek na konferenci
    Leto - 1995
    Jezik - angleški
    COBISS.SI-ID - 17181273

    Povezava(-e):

    http://dx.doi.org/10.1007/BFb0014068

Vnos na polico