We define the notion of location for regular expressions with shuffle by extending the notion of position in standard regular expressions. Locations allow for the definition of the sets Follow, First, and Last with their usual semantics. From these, we construct an automaton for regular expressions with shuffle (APOS), which generalises the standard position/Glushkov automaton. The sets mentioned above are also the foundation for other constructions, such as the Follow automaton, and automata based on pointed expressions. As a consequence, all these constructions can be generalised to the shuffle operator. We show that the partial derivative automaton is a right-quotient of APOS. We relate APOS with another automaton construction based on positions that has been previously studied (A∂pos). The prefix automaton is extended to the shuffle operator and shown not to be a quotient of APOS. Locations are also used to define a position automaton for regular expressions with the intersection.

Several notions of synchronisation in concurrent systems can be modelled by regular shuffle operators. In this paper we consider regular expressions extended with three operators corresponding respectively to strong, arbitrary, and weak synchronisation. For these expressions, we define a location based position automaton. Furthermore, we show that the partial derivative automaton is still a quotient of the position automaton.

A representation of intersection types in terms of pregrammars is presented. Pregrammar based rewriting relations, corresponding respectively to type checking and inhabitation are defined and the latter is used to implement a Wajsberg/Ben-Yelles style alternating semi-decision algorithm for inhabitation. The usefulness of the framework is illustrated by revisiting and partially extending standard inhabitation related results for intersection types, as well as establishing new ones. It is shown how the notion of bounded multiset dimension emerges naturally and the relation between the two settings is clarified. A meaningful rank independent superset of the set of rank 2 types is identified for which EXPSPACE-completeness for inhabitation as well as for counting is proved. Finally, a standard result on negatively non-duplicated simple types is extended to intersection types.

In this paper we give a complete, formal definition of the formula-tree proof method, prove its correctness and illustrate its adequateness for research in the area of inhabitation of simple types.

A combinatory system (or equivalently the set of its basic combinators) is called combinatorially complete for a functional system, if any member of the latter can be defined by an entity of the former system. In this paper the decision problem of combinatory completeness for finite sets of proper combinators is studied for three subsystems of the pure lambda calculus. Precise characterizations of proper combinator bases for the linear and the affine λ-calculus are given, and the respective decision problems are shown to be decidable. Furthermore, it is determined which extensions with proper combinators of bases for the linear λ-calculus are combinatorially complete for the λ I -calculus.

Abstract Translations from Lambda calculi into combinatory logics can be used to avoid some implementational problems of the former systems. However, this scheme can only be efficient if the translation produces short output with a small number of combinators, in order to reduce the time and transient storage space spent during reduction of combinatory terms. In this paper we present a combinatory system and an abstraction algorithm, based on the original bracket abstraction operator of Schönfinkel [9]. The algorithm introduces at most one combinator for each abstraction in the initial Lambda term. This avoids explosive term growth during successive abstractions and makes the system suitable for practical applications. We prove the correctness of the algorithm and establish some relations between the combinatory system and the Lambda calculus.