scholarly journals Type Inference with Inequalities

1990 ◽  
Vol 19 (336) ◽  
Author(s):  
Michael I. Schwartzbach
Keyword(s):  
General Result ◽  
Existence Of Solutions ◽  
Finite Automata ◽  
Minimal Solution ◽  
Type Inference ◽  
Constraint Solving ◽  
Multiple Inheritance ◽  
Exponential Time ◽  
Systems Of Inequalities ◽  
Infinite Collection

Type inference can be phrased as constraint-solving over types. We consider an implicitly typed language equipped with recursive types, multiple inheritance, 1st order parametric polymorphism, and assignments. Type correctness is expressed as satisfiability of a possibly infinite collection of (monotonic) inequalities on the types of variables and expressions. A general result about systems of inequalities over semilattices yields a solvable form. We distinguish between deciding <em>typability</em> (the existence of solutions) and <em>type inference</em> (the computation of a minimal solution). In our case, both can be solved by means of nondeterministic finite automata; unusually, the two problems have different complexities: polynomial vs. exponential time.

scholarly journals Comparison Theorems for the Multidimensional BDSDEs and Applications

2012 ◽  
Vol 2012 ◽  
pp. 1-14 ◽  
Author(s):  
Bo Zhu ◽  
Baoyan Han
Keyword(s):  
Differential Equations ◽  
Stochastic Differential Equations ◽  
Comparison Theorem ◽  
Existence Of Solutions ◽  
Minimal Solution ◽  
Comparison Theorems ◽  
Doubly Stochastic

A class of backward doubly stochastic differential equations (BDSDEs) are studied. We obtain a comparison theorem of these multidimensional BDSDEs. As its applications, we derive the existence of solutions for this multidimensional BDSDEs with continuous coefficients. We can also prove that this solution is the minimal solution of the BDSDE.

scholarly journals Type Reconstruction for Type Classes

1995 ◽  
Vol 5 (2) ◽  
pp. 201-224 ◽  
Author(s):  
Tobias Nipkow ◽  
Christian Prehofer
Keyword(s):  
Programming Language ◽  
Functional Programming ◽  
Type Inference ◽  
Constraint Solving ◽  
Simple Type ◽  
Inference Problem ◽  
Unification Algorithm ◽  
Type Classes ◽  
Type Reconstruction ◽  
Inference Systems

AbstractWe study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This leads to simple type inference systems and algorithms which closely resemble those for ML. In particular, we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.

scholarly journals The complexity of type inference for higher-order typed lambda calculi

1994 ◽  
Vol 4 (4) ◽  
pp. 435-477 ◽  
Author(s):  
Fritz Henglein ◽  
Harry G. Mairson
Keyword(s):  
Lower Bounds ◽  
Higher Order ◽  
Type Inference ◽  
Boolean Logic ◽  
Turing Machines ◽  
Technical Tool ◽  
Inference Problem ◽  
Exponential Time ◽  
First Order ◽  
Order Types

AbstractWe analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus (F2) invented by Girard and Reynolds, as well as higher-order extensions F3, F4, …, Fω proposed by Girard. We prove that recognising the F2-typable terms requires exponential time, and for Fω the problem is non-elementary. We show as well a sequence of lower bounds on recognising the Fk-typable terms, where the bound for Fk+1 is exponentially larger than that for Fk.The lower bounds are based on generic simulation of Turing Machines, where computation is simulated at the expression and type level simultaneously. Non-accepting computations are mapped to non-normalising reduction sequences, and hence non-typable terms. The accepting computations are mapped to typable terms, where higher-order types encode reduction sequences, and first-order types encode the entire computation as a circuit, based on a unification simulation of Boolean logic. A primary technical tool in this reduction is the composition of polymorphic functions having different domains and ranges.These results are the first nontrivial lower bounds on type inference for the Girard/Reynolds system as well as its higher-order extensions. We hope that the analysis provides important combinatorial insights which will prove useful in the ultimate resolution of the complexity of the type inference problem.

scholarly journals Efficient Recursive Subtyping

1992 ◽  
Vol 21 (405) ◽  
Author(s):  
Dexter Kozen ◽  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Finite Automaton ◽  
Finite Automata ◽  
Lambda Calculus ◽  
Theoretic Approach ◽  
Exponential Time ◽  
Emptiness Problem ◽  
Definition Of

<p>Subtyping in the presence of recursive types for the lambda-calculus was studied by Amadio and Cardelli in 1991. They showed that the problem of deciding whether one recursive type is a subtype of another is decidable in exponential time.</p><p>In this paper we give an O(n^2) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states.</p><p>It is known that equality of recursive types and the covariant Böhm order can be decided efficiently by means of finite automata. Our results extend the automata-theoretic approach to handle orderings based on contravariance.</p>

Making Type Inference Practical

1992 ◽  
Vol 21 (385) ◽  
Author(s):  
Nicholas Oxhøj ◽  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Image Compression ◽  
Polynomial Time ◽  
Object Oriented ◽  
Type Inference ◽  
Code Optimization ◽  
Annotation Tool ◽  
Inference Algorithm ◽  
Exponential Time ◽  
Type Information ◽  
Object Oriented Languages

We present the implementation of a type inference algorithm for untyped object-oriented programs with inheritance, assignments, and late binding.The algorithm significantly improves our previous one, presented at OOPSLA'91, since it can handle collection classes, such as {\bf List}, in a useful way. Also, the complexity has been dramatically improved, from exponential time to low polynomial time. The implementation uses the techniques of incremental graph construction and constraint template instantiation to avoid representing intermediate results, doing superfluous work, and recomputing type information. Experiments indicate that the implementation type checks as much as 100 lines pr. second. This results in a mature product, on which a number of tools can be based, for example a safety tool, an image compression tool, a code optimization tool, and an annotation tool. This may make type inference for object-oriented languages practical.

scholarly journals Type Inference of SELF: Analysis of Objects with Dynamic and Multiple Inheritance

1993 ◽  
Vol 22 (436) ◽  
Author(s):  
Ole Agesen ◽  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Type Inference ◽  
Inference Algorithm ◽  
Optimizing Compilers ◽  
Multiple Inheritance

We have designed and implemented a type inference algorithm for the full <strong>SELF</strong> language. The algorithm can guarantee the safety and disambiguity of message sends, and provide useful information for browsers and optimizing compilers.

scholarly journals Type inference of SELF: Analysis of objects with dynamic and multiple inheritance

1995 ◽  
Vol 25 (9) ◽  
pp. 975-995 ◽  
Author(s):  
Ole Agesen ◽  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Type Inference ◽  
Multiple Inheritance

Efficient recursive subtyping

1995 ◽  
Vol 5 (1) ◽  
pp. 113-125 ◽  
Author(s):  
Dexter Kozen ◽  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Finite Automaton ◽  
Finite Automata ◽  
Theoretic Approach ◽  
Exponential Time ◽  
Emptiness Problem ◽  
Definition Of

Subtyping in the presence of recursive types for the λ-calculus was studied by Amadio and Cardelli in 1991 (Amadio and Cardelli 1991). In that paper they showed that the problem of deciding whether one recursive type is a subtype of another is decidable in exponential time. In this paper we give an 0(n2) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states.It is known that equality of recursive types and the covariant Bohm order can be decided efficiently by means of finite automata, since they are just language equality and language inclusion, respectively. Our results extend the automata-theoretic approach to handle orderings based on contravariance.

Sign in / Sign up

Export Citation Format

Share Document