• English
  • Deutsch
  • Log In
    Password Login
    Research Outputs
    Fundings & Projects
    Researchers
    Institutes
    Statistics
Repository logo
Fraunhofer-Gesellschaft
  1. Home
  2. Fraunhofer-Gesellschaft
  3. Artikel
  4. Principality and approximation under dimensional bound
 
  • Details
  • Full
Options
2019
Journal Article
Title

Principality and approximation under dimensional bound

Abstract
We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional bound. The theory enables inference of principal type information under dimensional bound, it provides an algebraic and algorithmic theory of approximation of classical principal types in terms of computable bases of abstract vector spaces (more precisely, semimodules), and it shows a systematic connection of dimensional calculi to the theory of approximants. Finite, computable bases are shown to span standard principal typings of a given term for sufficiently high dimension, thereby providing an approximation to standard principality by type inference, and capturing it precisely for sufficiently large dimensional parameter. Subsidiary results include decidability of principal inhabitation for intersection types (given a type does there exist a normal form for which the type is principal?). Remarkably, combining bounded type inference with principal inhabitation allows us to compute approximate normal forms of arbitrary terms without using beta-reduction.
Author(s)
Dudenhefner, Andrej
TU Dortmund
Rehof, Jakob
TU Dortmund
Journal
Proceedings of the ACM on programming languages : PACMPL  
Open Access
DOI
10.1145/3290321
Additional full text version
Landing Page
Language
English
Fraunhofer-Institut für Software- und Systemtechnik ISST  
  • Cookie settings
  • Imprint
  • Privacy policy
  • Api
  • Contact
© 2024