A.J. Kfoury

TCS Journal 2004 Journal Article

Principality and type inference for intersection types using expansion variables

• A.J. Kfoury
• J.B. Wells

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.

I&C Journal 1999 Journal Article

Alpha-Conversion and Typability

• A.J. Kfoury
• S. Ronchi della Rocca
• J. Tiuryn
• P. Urzyczyn

There are two results in this paper. We first prove that alpha-conversion on types can be eliminated from the second-orderλ-calculusFof Girard and Reynolds without affecting the typing power of the system. On the other hand we show that it is impossible to eliminate alpha-conversion on universally quantified variables in the higher-orderλ-calculusF ω of Girard, by exhibiting a term which is typable inF ω with alpha-conversion but not typable inF ω without alpha-conversion.

I&C Journal 1997 Journal Article

An Infinite Pebble Game and Applications

• A.J. Kfoury
• A.P. Stolboushkin

We generalize the pebble game to infinite directed acyclic graphs and use this generalization to give new and shorter proofs of the following well-known results: (1) that unbounded memory increases the power of logics of programs, and (2) that there exists a context-free grammar with infinite index.

I&C Journal 1993 Journal Article

The Undecidability of the Semi-unification Problem

• A.J. Kfoury
• J. Tiuryn
• P. Urzyczyn

The Semi-Unification Problem (SUP) is a natural generalization of both first-order unification and matching. The problem arises in various branches of computer science and logic. Although several special cases of SUP are known to be decidable, the problem in general has been open for several years. We show that SUP in general is undecidable, by reducing what we call the "boundedness problem" of Turing machines to SUP. The undecidability of this boundedness problem is established by a technique developed in the mid-1960s to prove related results about Turing machines

TCS Journal 1992 Journal Article

On the expressive power of finitely typed and universally polymorphic recursive procedures

• A.J. Kfoury
• J. Tiuryn
• P. Urzyczyn

Finitely typed functional programs are naturally classified by their levels. This syntactic classification of functional programs corresponds to a semantical classification: the higher the level of functional programs, the more functions they can compute. We call FL the language of finitely typed functional programs. The halting problem on finite interpretations is elementary recursive for every FL program, i. e. for every FL program P there is an elementary recursive procedure to decide for every finite interpretation I whether P halts on I. The well-known programming language ML is essentially FL, augmented with the polymorphic let-in constructor. We show that ML computes the same class of functions as FL. As a consequence.

I&C Journal 1992 Journal Article

Type reconstruction in finite rank fragments of the second-order λ-calculus

• A.J. Kfoury
• J. Tiuryn

The prove that the problem of type reconstruction in the polymorphic λ-calculus of rank 2 is polynomial-time equivalent to the problem of type reconstruction in ML, and is therefore DEXPTIME-complete. We also prove that for every k > 2, the problem of type reconstruction in the polymorphic λ-calculus of rank k, extended with suitably chosen constants with types of rank 1, is undecidable.

TCS Journal 1983 Journal Article

Definability by programs in first-order structures

• A.J. Kfoury