8th Workshop, CSL '94 Kazimierz, Poland, September 25–30, 1994 Selected Papers
We give syntax and a PER-model semantics for a typed λ-calculus with subtypes and singleton types. The calculus may be seen as a minimal calculus of subtyping with a simple form of dependent types. The aim is to study singleton types and to take a canny step towards more complex dependent subtyping systems. Singleton types have applications in the use of type systems for specification and program...
Labeled types and a new relation between types are added to the lambda calculus of objects as described in [6]. This relation is a trade-off between the possibility of having a restricted form of width subtyping and the features of the delegation-based language itself. The original type inference system allows both specialization of the type of an inherited method to the type of the inheriting object...
This paper extends Curry-Howard interpretations of Intuitionistic Logic and Intuitionistic Linear Logic rules for recursion. The resulting term languages, the λrec-calculus and the linear λrec-calculus respectively, are given sound categorical interpretations. The embedding of proofs of Intuitionistic Logic into proofs of Intuitionistic Linear Logic given by the Girard Translation is extended with...
The combination of higher-order subtyping with intersection types yields a typed model of object-oriented programming with multiple inheritance [11]. The target calculus, F ⋀ ω , a natural generalization of Girard's system F ω with intersection types and bounded polymorphism, is of independent interest, and is our subject of study. Our main contribution is the...
We consider a λ-calculus for which applicative terms have no longer the form (...((u u 1) u 2)... u n) but the form (u [u 1;...;u n]), for which [u 1;...;u n] is a list of terms. While the structure of the usual λ-calculus is isomorphic to the structure of natural deduction, this new structure is isomorphic to the structure of Gentzen-style...
In this paper we discuss usability, and propose to take that notion as a formalisation of (un)definedness in typed lambda calculus, especially in calculi based on PCF. We discuss some important properties that make usability attractive as a formalisation of (un)definedness. There is a remarkable difference between usability and solvability: in the untyped lambda calculus the solvable terms are precisely...
There is a natural isomorphism identifying second order types of the simple typed λ calculus with free homogeneous term algebras. Let τ A and τ B be types representing algebras A and B respectively. Any closed term of the type τ A → τ B represents a computable function between algebras A and B. The problem investigated in the paper is to find and characterize...
This paper describes a criterion for the existence of generalizations of a particularly simple form given complex terms in short proofs within schematic theories: The soundness of replacing single quantifiers, which bind variables in schema instances, by blocks of quantifiers of the same type. The criterion is shown to be necessary in general and sufficient for languages consisting of monadic function...
Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed...
We shall describe two general methods for proving lower bounds on the lengths of proofs in propositional calculus and give examples of such lower bounds. One of the methods is based on interactive proofs where one player is claiming that he has a falsifying assignment for a tautology and the second player is trying to convict him of a lie. The second method is based on boolean valuations. For the...
We consider graphs in which it is possible to specify linear orderings of the sets of vertices, in uniform ways, by MS (i.e., Monadic Second-order) formulas. We also consider classes of graphs ℂ such that for every L $$\subseteq$$ ℂ, L is recognizable iff it is MS-definable. Our results concern in particular dependency graphs of partially commutative words.
The spectrum, Sp(ϕ), of a sentence ϕ is the set of cardinalities of finite structures which satisfy ϕ. We prove that any set of integers which is in Func 1 ∞ i.e. in the class of spectra of first-order sentences of type containing only unary function symbols is also in BIN 1 i.e. in the class of spectra of first-order sentences of type involving only a single binary...
It is well known that monadic second-order logic with linear order captures exactly regular languages. On the other hand, if addition is allowed, then J.F.Lynch has proved that existential monadic secondorder logic captures at least all the languages in NTIME(n), and then expresses some NP-complete languages (e.g. knapsack problem). It seems that most combinatorial NP-complete problems (e.g...
We define matchings, and show that they capture the essence of context-freeness. More precisely, we show that the class of context-free languages coincides with the class of those sets of strings which can be defined by sentences of the form ∃ bϕ, where ϕ is first order, b is a binary predicate symbol, and the range of the second order quantifier is restricted to the class of matchings. Several variations...
We extend recent work about the relationship between logically defined classes of NP optimization problems and the asymptotic growth of optimal solutions on random inputs. We consider the syntactic class Min F +Π2(1) of minimization problems. Kolaitis and Thakur proved that every problem in this class is log-approximable. We show that for every problem Q in the class Min F +Π2(l)...
We prove some general results about the existence of 0–1 and convergence laws for L ∞,ω k and L ∞,ω k on classes of finite structures equipped with a sequence of arbitrary probability measures {μ n }, as well as a few results for particular classes. First, two new proofs...
By “initial segments of P” we mean classes DTime(n k ). The question of whether for any fixed signature the first-order definable predicates in finite models of this signature are all in an initial segment of P is shown to be related to other intriguing open problems in complexity theory and logic, like P=PSpace. The second part of the paper strengthens the...
Many features of current logic programming languages are not captured by conventional semantics. Their fundamentally non-ground character, and the uniform way in which such languages have been extended to typed domains subject to constraints, suggest that a categorical treatment of constraint domains, of programming syntax and of semantics may be closer in spirit to declarative programming than conventional...
The paper investigates reasoning with set-relations: intersection, inclusion and identity of 1-element sets. A language is introduced which, interpreted in a multi-algebraic semantics, allows one to specify such relations. An inference system is given and shown sound and refutationally ground-complete for a particular proof strategy which selects only maximal literals from the premise clauses. Each...