In this article, we introduce Moschovakis higher-order type theory of acyclic recursion L-ar(lambda) . We present the potentials of L-ar(lambda) for incorporating different reduction systems in L-ar(lambda), with corresponding reduction calculi. At first, we introduce the original reduction calculus of L-ar(lambda), which reduces L-ar(lambda)-terms to their canonical forms. This reduction calculus determines the relation of referential, i.e., algorithmic, synonymy between L-ar(lambda)-terms with respect to a chosen semantic structure. Our contribution is the definition of a (gamma) rule and extending the reduction calculus of L-ar(lambda) and its referential synonymy to gamma-reduction and gamma-synonymy, respectively. The gamma-reduction is very useful for simplification of terms in canonical forms, by reducing subterms having superfluous gamma-abstraction and corresponding functional applications. Typically, such extra gamma abstractions can be introduced by the gamma-rule of the reduction calculus of L-ar(lambda).

The paper extends a higher-order type theory of acyclic algorithms by adding a reduction rule, which results in a stronger reduction calculus. The new reduction calculus determines a strong algorithmic equivalence between formal terms. It is very useful for simplifying terms, by eliminating sub-terms having superfluous lambda abstraction and corresponding spurious functional applications.

Computational linguistics studies natural language in its various manifestations from a computational point of view, both on the theoretical level (modeling grammar modules dealing with natural language form and meaning, and the relation between these two) and on the practical level (developing applications for language and speech technology). Right from the start in the 1950ties, there have been strong links with computer science, logic, and many areas of mathematics - one can think of Chomsky's contributions to the theory of formal languages and automata, or Lambek's logical modeling of natural language syntax. The symposium on Logic and Algorithms in Computational Linguistics 2018 (LACompLing2018) assesses the place of logic, mathematics, and computer science in present day computational linguistics. It intends to be a forum for presenting new results as well as work in progress.

This paper is a review of the formal definitions of a description language of functional models of Constraint-Based Lexicalized Grammar (CBLG), with a notion of well-formedness, models of linguistic objects, and the corresponding denotation function. The language uses feature-value descriptions. A formalization of CBLG is presented via definitions of several classes of objects by this formal language using mutual recursion. The core engine of the CBLG formal grammar is a hierarchical type system associated with constraints for representation of linguistic information. The constraints are classified as linguistic principles, grammar rules, lexical entries, lexical rules, and semantic representations. The formal system of CBLG targets a computational approach to human language grammar.

The paper is on a new approach to mathematics of the notion of algorithm. We extend the higher-order, type-theory of situated algorithms. The primary applications are to computational semantics of formal and natural languages and to computational neuroscience. We investigate the properties of functions and relations that bind argument slots of other functions and relations across a recursion operator acting via mutually recursive assignments.

Computational linguistics studies natural language in its various manifestations from a computational point of view, both on the theoretical level (modeling grammar modules dealing with natural language form and meaning, and the relation between these two) and on the practical level (developing applications for language and speech technology). Right from the start in the 1950ties, there have been strong links with computer science, logic, and many areas of mathematics - one can think of Chomsky's contributions to the theory of formal languages and automata, or Lambek's logical modeling of natural language syntax. The workshop assesses the place of logic, mathematics, and computer science in present day computational linguistics. It intends to be a forum for presenting new results as well as work in progress.

The paper introduces a higher-order, type-theoretical formal language LST GP of information content that is partial, parametric, underspecified, dependent on situations, and recursive. The terms of the formal language represent situation-theoretic objects. The language has specialized terms for constrained computations by mutual recursion. It introduces terms representing nets of parameters that are simultaneously constrained to satisfy restrictions.

The paper extends Moschovakis higher-order type theory of acyclic recursion by adding type polymorphism. We extend the type system of the theory to model parametric information that pertains to underspecified types. Different kinds of type polymorphism are presented via type variables and recursion constructs for alternative, disjunctive type assignments. Based on the new type system, we extend the reduction calculus of the theory of acyclic recursion. We motivate the type polymorphism with examples from English language.