scholarly journals Pruning Terms for Principal Type Assignment

2000 ◽  
Vol 31 ◽  
pp. 144-159
Author(s):  
Takeuti Izumi
Keyword(s):  
Principal Type ◽  
Type Assignment

Type Inference: Some Results, Some Problems1

1993 ◽  
Vol 19 (1-2) ◽  
pp. 87-125
Author(s):  
Paola Giannini ◽  
Furio Honsell ◽  
Simona Ronchi Della Rocca
Keyword(s):  
Large Class ◽  
Higher Order ◽  
Type Inference ◽  
Principal Type ◽  
Open Problems ◽  
Inference Problem ◽  
Type Assignment ◽  
Unification Problem

In this paper we investigate the type inference problem for a large class of type assignment systems for the λ-calculus. This is the problem of determining if a term has a type in a given system. We discuss, in particular, a collection of type assignment systems which correspond to the typed systems of Barendregt’s “cube”. Type dependencies being shown redundant, we focus on the strongest of all, Fω, the type assignment version of the system Fω of Girard. In order to manipulate uniformly type inferences we give a syntax directed presentation of Fω and introduce the notions of scheme and of principal type scheme. Making essential use of them, we succeed in reducing the type inference problem for Fω to a restriction of the higher order semi-unification problem and in showing that the conditional type inference problem for Fω is undecidable. Throughout the paper we call attention to open problems and formulate some conjectures.

PRINCIPAL TYPE ASSIGNMENT TO LAMBDA TERMS

1991 ◽  
Vol 02 (02) ◽  
pp. 149-162 ◽  
Author(s):  
SACHIO HIROKAWA
Keyword(s):  
Decision Procedure ◽  
General Type ◽  
Principal Type ◽  
Type Assignment ◽  
The Given

A principal type-scheme of a λ-term is a most general type-scheme for the term. This paper presents two characterizations of principal type assignment figures. By the first characterization, a decision procedure is shown for the principality of a type assignment figure. By the second characterization, an algorithm is presented which transforms a type assignment to a λ-term into a principal type assignment to the term in O(k4m4) steps where k is the size of the given type and m is the size of the given term. This gives a new proof for the principal type-scheme theorem which states: if a λ-term has a type then it has a principal type. The proof in this paper is simpler than known proofs which use the unification.

scholarly journals Kripke Semantics for Intersection Formulas

2021 ◽  
Vol 22 (3) ◽  
pp. 1-16
Author(s):  
Andrej Dudenhefner ◽  
Paweł Urzyczyn
Keyword(s):  
Kripke Semantics ◽  
Type Assignment ◽  
Soundness And Completeness

We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.

scholarly journals Geometric aspects of self-adjoint Sturm–Liouville problems

2017 ◽  
Vol 147 (6) ◽  
pp. 1279-1295
Author(s):  
Yicao Wang
Keyword(s):  
Boundary Conditions ◽  
Liouville Equation ◽  
Adjoint Action ◽  
Principal Type ◽  
Unitary Matrices ◽  
Adjoint Orbits ◽  
Sturm Liouville ◽  
Refined Classification ◽  
Adjoint Orbit

In this paper we use U(2), the group of 2 × 2 unitary matrices, to parametrize the space of all self-adjoint boundary conditions for a fixed Sturm–Liouville equation on the interval [0, 1]. The adjoint action of U(2) on itself naturally leads to a refined classification of self-adjoint boundary conditions – each adjoint orbit is a subclass of these boundary conditions. We give explicit parametrizations of those adjoint orbits of principal type, i.e. orbits diffeomorphic to the 2-sphere S2, and investigate the behaviour of the nth eigenvalue λnas a function on such orbits.

Sign in / Sign up

Export Citation Format

Share Document