We study the formal and linguistic properties of a class of parenthesis-free categorial grammars derived from those of Ades and Steedman by varying the set of reduction rules. We characterize the reduction rules capable of generating context-sensitive languages as those having a partial combination rule and a combination rule in the reverse direction. We show that any categorial language is a permutation of some context-free language, thus inheriting properties dependent on symbol counting only. We compare some of their properties with other contemporary formalisms.

AbstracLThis paper develops algorithms by which decision procedures for the functional calculus can be applied mechanically.Given any expression in Skolem normal form with prefix (3y~)(3y2) ... (3y,~,)(z~)(z~) ... (z,~) and matrix M, the algorithms lead to the construction of a nu~trix M* such that M D M* is valid and such that the expressions (3yl)(3y~) ... (3y,~)(zl)(z~) ... (z,~).Mand (3yl)(3y2) "" (3y,,,)(zl)(z~) -.. (z,~).M*areinterprovable.This procedure is thus a semi-decision procedure for the general Skolem case.For two special cases of this prefix, it is further proved that the method provides a solution to the decision problem in the sense that the given expression is a theorem if and only if M* is tautologous.These cases are ~1) a matrix M in which every elementary part contains at least one of the individual variables z~ , z~, .. • , z,~ or contains only one individual variable or contains both Yl and y2 and no other individual variables; and (2) a matrix M in which every elementary part contains at least one of the individual variables z~ , z2, .--,z,, or contains only one individual variable or contains all of y~, y2, '" , ym •

In a previous paper [4] by the same author a semi-decisi(m procedure for the funetionM calculus was described.A part of the procedure has now been programmed for the 7090 computer.In this paper a FORTRAN program is described which decides expressions with prefix (By1) (By2) (z~) -.. (z,d and matrix containing only dyadic funet.ionalvariables.The program has been run for some standard examples and takes less t:han seven seconds for the longest one.

The "computed output sequence" of a finite automaton is defined as the sequence which results from the output sequence when all occurrences of a special output symbol X are deleted.A "computation pair" consists of an input sequence and the resultant computed output sequence, and the "computation" of an automaton is the set of all its computation pairs.The class of infinite computations is broader than the class of behaviors of finite automata.Burks has therefore raised the question of the existence of a decision procedure to determine if two automata have the same computation.In this paper, such a decision procedure is given.

Alonzo Church has proposed a system of “restricted recursive arithmetic” for the analysis of computer circuits which include time delays and feedback. Restricted recursive arithmetic, which will be referred to as rra, was introduced by Church in this Journal, vol. 20 (1955), pp. 286–287, in a review of an article by Edmund C. Berkeley. It is the purpose of this paper to present some results which have been found for the system rra.