scholarly journals Efficient Inference of Partial Types

1992 ◽  
Vol 21 (394) ◽  
Author(s):  
Dexter Kozen ◽  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Open Problem ◽  
Finite Automaton ◽  
Lambda Calculus ◽  
Time Algorithm ◽  
Type Inference ◽  
Exponential Time ◽  
Canonical Solution ◽  
Persistent Data ◽  
Exponential Time Algorithm ◽  
Construction Works

Partial types for the lambda-calculus were introduced by Thatte in 1988 as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data In that paper he showed that type inference for partial types was semidecidable. Decidability remained open until quite recently, when O'Keefe and Wand gave an exponential time algorithm for type inference.<p>In this paper we give an O(n^3) algorithm. Our algorithm constructs a certain finite automaton that represents a canonical solution to a given set of type constraints. Moreover, the construction works equally well for recursive types; this solves an open problem stated by O'Keefe and Wand.</p>

An Exact Exponential Time Algorithm for Power Dominating Set

Algorithmica ◽  
2011 ◽  
Vol 63 (1-2) ◽  
pp. 323-346 ◽  
Author(s):  
Daniel Binkele-Raible ◽  
Henning Fernau
Keyword(s):  
Dominating Set ◽  
Time Algorithm ◽  
Exponential Time ◽  
Exponential Time Algorithm

An improved exponential-time algorithm for k -SAT

2005 ◽  
Vol 52 (3) ◽  
pp. 337-364 ◽  
Author(s):  
Ramamohan Paturi ◽  
Pavel Pudlák ◽  
Michael E. Saks ◽  
Francis Zane
Keyword(s):  
Time Algorithm ◽  
Exponential Time ◽  
Exponential Time Algorithm

scholarly journals Bounded homomorphisms and finitely generated fiber products of lattices

2020 ◽  
Vol 30 (04) ◽  
pp. 693-710
Author(s):  
William DeMeo ◽  
Peter Mayr ◽  
Nik Ruškuc
Keyword(s):  
Word Problem ◽  
Time Algorithm ◽  
Finitely Generated ◽  
Bounded Lattice ◽  
Exponential Time ◽  
Unpublished Result ◽  
Lattice Homomorphisms ◽  
Finitely Presented ◽  
Exponential Time Algorithm

We investigate when fiber products of lattices are finitely generated and obtain a new characterization of bounded lattice homomorphisms onto lattices satisfying a property we call Dean’s condition (D) which arises from Dean’s solution to the word problem for finitely presented lattices. In particular, all finitely presented lattices and those satisfying Whitman’s condition satisfy (D). For lattice epimorphisms [Formula: see text], [Formula: see text], where [Formula: see text], [Formula: see text] are finitely generated and [Formula: see text] satisfies (D), we show the following: If [Formula: see text] and [Formula: see text] are bounded, then their fiber product (pullback) [Formula: see text] is finitely generated. While the converse is not true in general, it does hold when [Formula: see text] and [Formula: see text] are free. As a consequence, we obtain an (exponential time) algorithm to decide boundedness for finitely presented lattices and their finitely generated sublattices satisfying (D). This generalizes an unpublished result of Freese and Nation.

scholarly journals Pessimistic Leader-Follower Equilibria with Multiple Followers

2017 ◽  
Author(s):  
Stefano Coniglio ◽  
Nicola Gatti ◽  
Alberto Marchesi
Keyword(s):  
Nash Equilibrium ◽  
Normal Form ◽  
Scientific Literature ◽  
Time Algorithm ◽  
Exponential Time ◽  
Normal Form Games ◽  
Opposite Case ◽  
Pure Strategies ◽  
Multiple Followers ◽  
Exponential Time Algorithm

The problem of computing the strategy to commit to has been widely investigated in the scientific literature for the case where a single-follower is present. In the multi-follower setting though, results are only sporadic. In this paper, we address the multi-follower case for normal-form games, assuming that, after observing the leader’s commitment, the followers play pure strategies and reach a Nash equilibrium. We focus on the pessimistic case where, among many equilibria, one minimizing the leader’s utility is chosen (the opposite case is computationally trivial). We show that the problem is NP-hard even with only two followers, and propose an exact exponential-time algorithm which, for any number of followers, either finds an equilibrium when the game admits a finite one or, if not, an α-approximation of the supremum of the leader’ utility, for any α > 0.

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>

Sign in / Sign up

Export Citation Format

Share Document