1.1 On type-theory of recursion and algorithms

By Moschovakis (Reference Moschovakis1989, Reference Moschovakis, Oikkonen and Väänänen1993, Reference Moschovakis, Dalla Chiara, Doets, Mundici and van Benthem1997), Yiannis N. Moschovakis introduced the untyped version of the mathematical notion of algorithm via the formal language of recursion (FLR). The theory of FLR provides denotational and algorithmic semantics of its untyped formal language. The denotational semantics of FLR covers the mathematical structures having as their domain spaces the sets of functions determined by full recursion. Significantly, the algorithmic semantics of the FLR provides algorithms for computing the denotational values of the algorithmically meaningful FLR terms, in the space of recursive functions. The algorithmically meaningful FLR terms of full recursion designate algorithms that may be cyclic without ending.

The type-theory of acyclic recursion (TTAR) $\operatorname {L^{\lambda }_{ar}}$ , that is, of acyclic algorithms, was introduced by Moschovakis (Reference Moschovakis2006). In distinction to the untyped FLR, which includes endless cyclic algorithms, the type-theory $\operatorname {L^{\lambda }_{ar}}$ formalizes algorithms that terminate, that is, close-off, after finite number of steps of calculations. In Moschovakis (Reference Moschovakis2006), the focus is on demonstrating potential applications of $\operatorname {L^{\lambda }_{ar}}$ to computational semantics of natural language (NL), by an approach that is similar to semantics of programming languages. The language of $\operatorname {L^{\lambda }_{ar}}$ limits the set of its $\operatorname {L^{\lambda }_{ar}}$ terms by an acyclicity criterion given in Definition 3 of this article.

For an initial introductions to type-theory $\operatorname {L^{\lambda }_{ar}}$ of recursion, its syntax, its distinctive two kinds of semantics, namely denotational and algorithmic semantics, and reduction calculus, see Moschovakis (Reference Moschovakis2006). Formally, the $\operatorname {L^{\lambda }_{ar}}$ terms in Moschovakis (Reference Moschovakis2006) are defined by the clauses of the form (3a)–(3d) given in Definition 2 of this article, which satisfy the Acyclicity Constraint (AC) in Definition 3.

For detailed, formal introduction to the syntax and extended reduction calculus of TTAR $\operatorname {L^{\lambda }_{ar}}$ , its denotational and algorithmic semantics, see Loukanova (Reference Loukanova2019b). Further developments of TTAR $\operatorname {L^{\lambda }_{ar}}$ consist of extended formal languages and computational facilities of $\operatorname {L^{\lambda }_{ar}}$ , see Loukanova (Reference Loukanova, van den Herik and Filipe2016a, Reference Loukanova2016b, Reference Loukanova, Osswald, Retoré and Sutton2019a, Reference Loukanova2019b, Reference Loukanova, Grabowski, Loukanova and Schwarzweller2020, Reference Loukanova, Materna and Jespersen2022, Reference Loukanova2023b, Reference Loukanova2023c, Reference Loukanova2023d, Reference Loukanova, Bekki, Mineshima and McCready2024).

Often, I use the same designation of the developed classes of TTAR and algorithms, that is, TTAR, TTAA, or $\operatorname {L^{\lambda }_{ar}}$ . These classes suffice for representing significant fragments of NL.

1.2 Other systems for formal semantics of NLs

In this section, I present some of the formal systems for semantic representations of NL expressions, which have some significance with respect to $\operatorname {L^{\lambda }_{ar}}$ .

Originally, Russell (Reference Russell1905) proposed a logic system without types, for semantic representations of NL sentences consisting of combinations of verbs (Vs) and noun phrases (NPs). In the Russel logic, the semantic denotation of a sentence, which is a combination of an NP and a VP expressions, is the result of application of the function, which denotes the NP expression, to the denotation of the VP expression.

The papers Henkin (Reference Henkin1950) and Mostowski (Reference Mostowski1957) formalized Russel’s proposal by higher-order logic. Importantly, Mostowski (Reference Mostowski1957) introduced the logic of generalized quantifiers, which are essential for semantics of quantified expressions.

In several papers, Richard Montague extended the ideas of generalized quantifiers to the comprehensive formal semantics of a fragment of NL. Most successfully, Montague (Reference Montague, Hintikka, Moravcsik and Suppes1973) introduced Intensional Logic (IL) for semantic representation of NL quantifiers and intensional verbs, in his system of The Proper Treatment of Quantification (PTQ). His IL uses higher-order, simply typed, lambda calculus. In Montague IL, all NPs, including proper names, are translated into one-argument generalized quantifiers. All verbs, extensional and intensional, which have syntactic arguments requiring NPs, are translated into terms of “shifted up” types for suitable combinations with the types of the generalized quantifiers. The essential translation system into IL terms uses $\beta$ -conversions and meaning postulates to transform and simplify the resulting IL terms to typical logic terms. Following Montague IL and PTQ, various systems of formal semantics of NL fragments have been proposed in similar styles.

The concepts of the generalized quantifiers continue to be an essential type-theoretical facility, especially for formal semantics of NL, including in the algorithmic semantics of $\operatorname {L^{\lambda }_{ar}}$ .

The type-theory $\mathrm{TY}_2$ introduced by Gallin (Reference Gallin1975) is a significant move towards representation of context by states into the formal language and semantics of $\mathrm{TY}_2$ , which is a basis for generalizations of type-theoretic semantics of NL. A major result of Gallin (Reference Gallin1975) is the interpretation of Montague IL, which was introduced by Montague (Reference Montague, Hintikka, Moravcsik and Suppes1973) and Thomason (Reference Thomason1974), in $\mathrm{TY}_2$ .

Muskens l ambda t ype- t heory. Muskens relational logic $\textit{TT}_2$ , Muskens (Reference Muskens1995), is the basis for type-theoretic semantics in the Muskens generalized grammar (MGGr) that he developed. It covers partiality of semantic relations and generalized quantifiers. For introductions to MGGr, by comparing $\mathrm{TY}_2$ with IL, see Muskens (Reference Muskens1995) and Loukanova (Reference Loukanova, Bekki, Mineshima and McCready2023e).

Sadrzadeh and Muskens (Reference Sadrzadeh and Muskens2019) is a development of Muskens type-logic grammar. In the dynamic models of lambda calculus, the degree of co-occurrence of words in context determines similarity of words’ interpretations in the correspondingly changed context. Interesting questions emerge regarding whether and, if yes, how the type-theory $\operatorname {L^{\lambda }_{ar}}$ can be integrated with dynamic vector models for lambda calculus, towards further generalizations of algorithmic semantics of NL.

Type- t heory of a cyclic r ecursion in r elation to G allin t ype- t heory. The formal language of $\operatorname {L^{\lambda }_{ar}}$ strictly extends (Gallin Reference Gallin1975) type-theory $\mathrm{TY}_2$ , and by that (Montague Reference Montague, Hintikka, Moravcsik and Suppes1973) IL. Loukanova (Reference Loukanova2023c), Sections 4 and 5, gives a mathematical proof of this expressiveness of an extended version of $\operatorname {L^{\lambda }_{ar}}$ . TTAR, $\operatorname {L^{\lambda }_{ar}}$ , has recursion terms that are not algorithmically equivalent to any $\lambda$ -calculus, for example, $\mathrm{TY}_2$ terms. Such $\operatorname {L^{\lambda }_{ar}}$ recursion terms provide subtle semantic distinctions via computational algorithms of $\operatorname {L^{\lambda }_{ar}}$ .

Similarly to $\mathrm{TY}_2$ , $\operatorname {L^{\lambda }_{ar}}$ has the following characteristics:

Currying. $\operatorname {L^{\lambda }_{ar}}$ uses currying encoding of multi-argument relations and functions via one-argument functions, which is the basis of techniques often used in functional programming and other formal languages.

States and state dependency. $\operatorname {L^{\lambda }_{ar}}$ has types and terms designating states and state-dependent objects. In general, the nature of the states in the semantic domains of $\operatorname {L^{\lambda }_{ar}}$ can be left open and introduced depending on applications of $\operatorname {L^{\lambda }_{ar}}$ . Moschovakis (Reference Moschovakis2006) tentatively presented states as ordered tuples of components that represent context information for semantic denotations of NL expressions. Detailed context elements are formally used as situations, agents, space, and time locations in Situation Theory and Situation Semantics, see Loukanova (Reference Loukanova, Nguyen, Kowalczyk, Fred and Joaquim2014, Reference Loukanova2023a).

Passives in HPSG approach. Syntax–semantics analysis of the passives was introduced since the early stages of HPSG, see Pollard and Sag (Reference Pollard and Sag1994) and Sag et al. (Reference Sag, Wasow and Bender2003). Their approach reflects on solid linguistic research and significance of linguistic generalizations across syntactic structures of NL. My work on the syntax–semantics interfaces in NL is inspired and based on such significance of linguistic generalizations. The formal representation of the lexical and phrasal syntax of the passives, via feature-structure descriptions, which I employ for the syntax of NL, is bassed on the corresponding rules in Sag et al. (Reference Sag, Wasow and Bender2003).

1.3 On computational grammar of NL

A detailed introduction to a class of approaches of formal grammar of NL called Constraint-Based Lexicalized Grammar (CBLG), with linguistic motivations and bibliography, is given in Sag et al. (Reference Sag, Wasow and Bender2003). A formal generalization of the CBLG approaches covered in Sag et al. (Reference Sag, Wasow and Bender2003) is presented in Loukanova (Reference Loukanova2017), which, sometimes, I call generalized CBLG (GCBLG), by a focus on its mathematical models of linguistic information in functional domains. While GCBLG appears closest to the approach of Head-Driven Phrase Structure Grammar (HPSG), it covers common linguistic trends in varieties of other approaches to formal and computational syntax. In particular, in what follows, I list a related, major classification of approaches to formal grammar of NL, which includes many other specific classes of formalizations:

1. Phrase Structure Grammars and Transformational Grammars: 1955–64; for example, see the initiation towards computational syntax (Chomsky Reference Chomsky1957, Reference Chomsky1965).

2. Generalized Phrase Structure Grammar (GPSG): 1979–87; for example, see the beginnings of actual computational syntax by Gazdar et al. (Reference Gazdar, Klein, Pullum and Sag1985).

3. Lexical Functional Grammar (LFG): 1979 to the present; for example, see Bresnan (Reference Bresnan2001) and Dalrymple (Reference Dalrymple2001, Reference Dalrymple2023)

4. Head-driven Phrase Structure Grammar (HPSG): since Pollard and Sag (Reference Pollard and Sag1994) and Müller et al. (Reference Müller, Abeillé, Borsley and Koenig2024) to the present, a linguistic approach and large-scale computational grammar of NL, see DELPH-INS (2025).

5. Constraint-Based L exicalized Grammar (CBLG): approaches to formal and computational syntax of NL, which represents comprehensive, linguistically motivated syntactic structures. Sag et al. (Reference Sag, Wasow and Bender2003) is a detailed introduction to the approaches of formal grammar of NL, giving references by extensive descriptions. The authors motivate the development of CBLG family of approaches to formal grammar of NL, starting with Finite State Automata and Context Free languages. Loukanova (Reference Loukanova2017) presents a possibility for mathematical models of syntactic structures of a class of formal languages of CBLG. The syntactic descriptions in CBLG are modeled by mathematical structures of sets of functions that represent complex, linguistically motivated information. The functions are recursively defined over linguistic features and take as values also such functions, which can be atomic or complex.

6. Categorial Grammar (CG): 1970 to the present. CG was originally developed by Ajdukiewicz (Reference Ajdukiewicz1937) as a mathematical theory suitable for significant syntactic structures of NL. See Carpenter (Reference Carpenter1998) for an extensive introduction and overview of the CG approaches.

7. Grammatical Framework (GF): GF is a type-theoretical formalism, with highly promising development for parallel, multilingual translation and text generation, see Ranta (Reference Ranta1994).

Computational syntax of NL has been well developed, in particular for widely used langages, for example, English, German, Norwegian, Japanese, etc. On the other hand, computational semantics and computational syntax–semantics interfaces, in computational grammar of NL, including CBLGs, are largely open research subjects.

1.4 Semantic representations in CBLG

Copestake et al. (Reference Copestake, Flickinger, Pollard and Sag2005) introduced the technique, called Minimal Recursion Semantics (MRS) and the formal language of MRS, in a semi-formal mode, while describing them strictly and clearly. Thus, MRS is a technique for formal representations of semantic information by specialized expressions of the language of MRS.

To some extent, MRS has been used in LFG, see Flickinger et al. (Reference Flickinger, Lønning, Dyvik, Oepen and Bond2005) on the initial implementation of the LOGON machine translation system.

HPSG is a well-developed, large-scale grammar, that is, HPSG approach, for various languages, especially for English, German, Norwegian, and Japanese, which also uses syntax–semantics interfaces via MRS, see DELPH-INS (2025).

Nowadays, MRS is well implemented and standardly used for semantic representation in HPSG approaches, see Müller et al. (Reference Müller, Abeillé, Borsley and Koenig2024), in particular Ch. 22 on MRS. The technique MRS in HPSG employs unification methods in varieties of the formal language of feature-value structure descriptions presented in Sag et al. (Reference Sag, Wasow and Bender2003). The syntax of HPSG is formalized by a more general GCBLG presented in Loukanova (Reference Loukanova2017).

Mathematical foundations of MRS in HPSG. The type-theory $\operatorname {L^{\lambda }_{ar}}$ presented in this paper provides a direct contribution to the mathematical foundation of the MRS technique implemented in the large-scale HPSG grammar approach. More precisely, $\operatorname {L^{\lambda }_{ar}}$ is mathematical foundation of MRS via currying encoding of semantic relations.

The mathematical model theory of situated, partial information, called Situation Theory, introduced and extended by Loukanova (Reference Loukanova, Nguyen, Kowalczyk, Fred and Joaquim2014, Reference Loukanova2023a), provides abstract mathematical objects that are recursively defined and depend on situations, times, space, and agents. The types, properties, and relations between objects are either primitive, that is, atomic, or complex and recursively defined, without currying encoding. Situation Theory has a special application to semantics of NL, called Situation Semantics.

In a specialized, restricted version, Situation Theory provides a mathematical foundation of the technique MRS, explicitly without currying encoding of properties and relations. Thus, MRS is an implementation technique for a version of Situation Semantics of NL.

One of the significant existing applications of $\operatorname {L^{\lambda }_{ar}}$ is the formalization of the semantic representations in the large-scale grammar approaches of HPSG, including by:

1. (1) initial representation of Situation Semantics expressions by the language of feature-value descriptions, and

2. (2) implementations of MRS in HPSG.

For an early development of TTAR and its application to mathematics of MRS, see Loukanova (Reference Loukanova, Bel-Enguix, Dahl and De La Puente2011b, Reference Loukanova, Bel-Enguix, Dahl and Jiménez-López2011a).

Note that semantic representations in HPSG, by MRS in feature-value descriptions, are representations of a simplified version of the specialized formal language of Situation Semantics presented in Loukanova (Reference Loukanova, Nguyen, Kowalczyk, Fred and Joaquim2014).

MRS uses constrained labels, that is, which are similar to specialized variables, where constraints are expressed by feature-value descriptions encoding formal terms of Situation Theory. The constrained MRS labels (variables) are formalized, via currying encoding, by restricted $\operatorname {L^{\lambda }_{ar}}$ terms, which are defined by the clauses of the form (3e) in Definition 2. A significant characteristic of MRS in HPSG, similarly to the syntax in HPSG, is that the facilities of lambda terms and calculus are not employed terms. That is efficiently compensated for by the HPSG hierarchy of typed constraints, suitably labeled by labels, which have the roles of variables and unification technique.

The formal language and mathematics of type-theory of TTAR, $\operatorname {L^{\lambda }_{ar}}$ , use the standard lambda terms for the compositional formation of terms and their denotational semantics, without reliance on unification methods. The algorithmic semantics of TTAR is provided by the specialized set of recursion variables, recursion terms, and reduction calculus; see the formal definitions and descriptions in Section 2.

My general contribution via TTAR, $\operatorname {L^{\lambda }_{ar}}$ , to Computational Grammar. Thus, the formal language and type-theory $\operatorname {L^{\lambda }_{ar}}$ provides the large-scale HPSG grammar including MRS expressions used in it, and the MRS technique presented independently outside HPSG grammar, with mathematical foundation and essential algorithmic semantics. My significant contribution (which is the first one up to my awareness) to MRS, HPS, and in general to Computational Grammar of NL is providing them with strict, reliable mathematical foundations, via developments of TTAR and the dependent-type-theory of situated information, that is, Situation Type-Theory of Situated Information and Semantics. TTAA, $\operatorname {L^{\lambda }_{ar}}$ , provides criterion for acyclicity in applications to computational syntax–semantics of NL.

I work on development of the mathematics of TTAR and utilizing TTAR for the semantic representations. In this paper, I incorporate the formal $\operatorname {L^{\lambda }_{ar}}$ terms inside feature-value structure descriptions of NL syntax. In addition, I often use standard context-free phrasal structure rules, including in this paper, for the syntax of NL to demonstrate how TTAR can be utilized for algorithmic syntax–semantics interfaces.

My contributions in this paper. I introduce the formal mathematics of TTAR. Then, I present the utility of TTAR for rendering NL passive forms, by descriptions and examples. TTAR has a rich language that allows optional terms for semantic representations of NL including passives. The selection depends on specific computational grammars and personal taste of a researcher. The canonical forms of TTAR terms provide criteria for algorithmic equivalence between terms. The mathematical characteristics of TTAR are among the many benefits of using TTAR for extending the existing approaches to computational semantics.

In addition, in this paper, I introduce a new way of rendering the passives, via specialized passivization marker, see the sections and examples on the verb “be” as a passivization marker. I add algorithmic patterns for representation of major classes of passives, by using such a marker, and without it.

A brief description of the content of the paper. In Section 2, I provide the formal syntax of type-theory $\operatorname {L^{\lambda }_{ar}}$ of acyclic recursion and algorithms (TTAR/TTAA). In Sections 3 and 4, I define the canonical forms and the extended reduction calculus of $\operatorname {L^{\lambda }_{ar}}$ . These computational concepts are valid also for the type-theory of full recursion and algorithms with cycles (TTR/TTA). Sections 5 and 6 introduce syntax–semantics interfaces via feature-structure descriptions. The rest of the paper introduces the application of TTAR to the syntax–semantics interfaces of passive forms in a generalized computational grammar, which includes connected lexical and phrasal structures.

In general, the algorithmic semantics of $\operatorname {L^{\lambda }_{ar}}$ presented in this paper can be employed for semantic representations of NL in a varieties of computational grammar, not only for CBLG approaches. In addition, I present a syntax–semantics technique via integration of semantic representations of NL, by the formal language of $\operatorname {L^{\lambda }_{ar}}$ , into CBLG syntax. In this paper, I focus on the specific linguistic phenomenon of passive forms of verbal expressions of NL.

In GCBLG, similar to Sag et al. (Reference Sag, Wasow and Bender2003) and Loukanova (Reference Loukanova, Bel-Enguix and Jiménez-López2011c), I use the typed version of the formal language of feature-value descriptions, also known as attribute-value matrices (AVMs), see Johnson (Reference Johnson1988). AVMs express linguistic information underlining syntactic structures of NL, by a combination of dependent types, which are organized hierarchically by constraints. Constraints and other linguistic information are expressed by formal features having corresponding values. This paper shows that GCBLG can be used for integration of syntax–semantics interface in it. The semantic representations in GCBLG do not necessarily use recourse to unification techniques. For the syntactic parts of the grammar analysis of NL, I use, as in Loukanova (Reference Loukanova, Bel-Enguix and Jiménez-López2011c), some of the major syntactic categories and structures, without detailed syntactic components.

4.1 Extended congruence relation between terms

For a full, formal definition of the congruence relation, see Loukanova (Reference Loukanova2023c). Here, I present it informally:

4.2 Reduction rules of extended TTA

(cong) \begin{align} {\textbf {Congruence}} & \qquad\qquad \text{ If } A \equiv _{\mathsf{c}} B, \text{ then } A \Rightarrow B \end{align}

(trans) \begin{align} {\textbf {Transitivity}} & \qquad\qquad\text{ If }A \Rightarrow B \text{ and } B \Rightarrow C, \text{ then } A \Rightarrow C \end{align}

1. Compositionality. Reducing subterms, by term syntax:

   (ap-comp) \begin{align} &\text{ If } A \Rightarrow A' \text{ and } B \Rightarrow B', \text{ then } A(B) \Rightarrow A'(B') \end{align}
   (lq-comp) \begin{align} &\text{ If } A \Rightarrow B, \text{ and } \xi \in \{ \lambda , \exists , \forall \}, \text{ then } \xi (u) (A) \Rightarrow \xi (u) (B) \end{align}
   (rec-comp) \begin{align} \begin{split} &\text{ If } A_i \Rightarrow B_i, \text{ for } i = 0, \ldots , n, \text{ then } \\ & \hspace {3.5ex} A_{0} \,\mathsf{where}\, \{ p_{1} := A_{1}, \ldots , p_{n} := A_{n} \} \\ & \Rightarrow B_{0} \,\mathsf{where}\, \{ p_{1} := B_{1}, \ldots , p_{n} := B_{n} \} \end{split} \end{align}

1. Compositionality of the restrictor terms (in the extended $\operatorname {L}^{\lambda }_{r}$ and $\operatorname {L^{\lambda }_{ar}}$ )

   (st-comp) \begin{align} \begin{split} & \text{ If } C_i \Rightarrow R_i\, (i = 0, \ldots , n), \text{ then} \\[1ex] &C_{0}\ {\mathsf{such\ that}}{}\ \{ C_1, \ldots , C_n \}\\ \Rightarrow {}\, &R_0 \ {\mathsf{such\ that}}{}\ \{ R_1, \ldots , R_n \}\end{split} \end{align}

1. Head rule. Given that, for all $i=1$ , …, $n$ , $j=1$ , …, $m$ , $p_i \not = q_{j}$ and $p_i$ does not occur freely in $B_j$ :

   (head) \begin{align} \begin{split} &\bigl (A_{0} \,\mathsf{where}\, \lbrace \overrightarrow {p} := \overrightarrow {A} \, \rbrace \bigr ) \,\mathsf{where}\, \lbrace \overrightarrow {q} := \overrightarrow {B} \, \rbrace \\ \Rightarrow & A_{0} \,\mathsf{where}\, \lbrace \overrightarrow {p} := \overrightarrow {A}, \ \overrightarrow {q} := \overrightarrow {B} \, \rbrace \end{split} \end{align}

2. Bekič–Scott rule. Given that, for all $i=1$ , …, $n$ , $j=1$ , …, $m$ , $p_i \not = q_{j}$ and $q_j$ does not occur freely in $A_{0}$ and $A_i$

   (B-S) \begin{align} \begin{split} & A_{0} \,\mathsf{where}\, \lbrace \, p := \bigl (B_{0} \,\mathsf{where}\, \lbrace \overrightarrow {q} := \overrightarrow {B} \, \rbrace \bigr ), \overrightarrow {p} := \overrightarrow {A} \, \rbrace \\ \Rightarrow {} &A_{0} \,\mathsf{where}\, \lbrace \, p := B_{0}, \overrightarrow {q} := \overrightarrow {B}, \ \overrightarrow {p} := \overrightarrow {A} \, \rbrace \end{split} \end{align}

3. Recursion-application rule. Given that, for all $i=1$ , …, $n$ , $p_i$ does not occur freely in $B$

   (recap) \begin{align} (A_{0} \,\mathsf{where}\, \lbrace \overrightarrow {p} := \overrightarrow {A} \, \rbrace \bigr )(B) \Rightarrow {} A_{0}(B) \,\mathsf{where}\, \lbrace \overrightarrow {p} := \overrightarrow {A}\! \rbrace \end{align}

4. Application rule. Given that $B \in {\mathsf{Terms}}$ is proper and $b \in {\mathsf{RecV}}$ is fresh, that is, $b \in \bigl [ {\mathsf{RecV}} - \big ( {\mathsf{FreeV}}\big (A(B)\big ) \cup {\mathsf{BoundV}}\big (A(B)\big ) \big ) \bigr]$

   (ap) \begin{align} A(B) &\Rightarrow \ A(b) \,\mathsf{where}\, \lbrace \, b := B \, \rbrace \end{align}

5. $\lambda$ and quantifier rules. Let $\xi \in \{ \lambda , \exists , \forall \}$

   (ξ) \begin{align} &\xi (u) \, (A_{0} \,\mathsf{where}\, \{ p_{1} := A_{1}, \ldots , p_{n} := A_{n} \})\nonumber \\[2pt] \Rightarrow {} &\xi (u) \, A'_{0} \,\mathsf{where}\, \{ p'_{1} := \lambda (u) \, A'_{1}, \ldots , p'_{n} := \lambda (u) \, A'_{n} \} \end{align}

   given that, for every $i = 1$ , …, $n$ ( $n \geq 0$ ), $p'_i \in {\mathsf{RecV}}$ is a fresh recursion (memory) variable, and $A'_i$ ( $0\leq i \leq n$ ) is the result of the simultaneous replacements of all the free occurrences of $p_{1}, \ldots , p_{n}$ in $A_i$ with $p'_{1}(u), \ldots , p'_{n}(u)$ , respectively, that is, each $A'_{i}$ is as in (26):

   (26) \begin{align} A'_{i} &\equiv A_{i} \{ p_{1} :\equiv p'_{1}(u), \ldots , p_{n} :\equiv p'_{n}(u) \} \equiv A_i \{ \overrightarrow {p} :\equiv \overrightarrow {p'(u)} \}\ {(0\leq i \leq n)} \end{align}

Restrictor rules. (st1) / (st2)

Assume that for $j = 1, \ldots , m$ ( $m \geq 0$ ), $i= 1, \ldots , k$ ( $k \geq 0$ ), $m+k \geq 1$ , and:

1. (1) $A_{0}, C_1^{\tau _1}, \ldots , C_m^{\tau _m}, R_{1}^{\sigma _{1}}, \ldots , R_{k}^{\sigma _{k}} \equiv \overrightarrow {R^{\sigma }} \in {\mathsf{Terms}}$ ;

2. (2) $C_j^{\tau _j}$ and $R_{i}^{\sigma _{i}}$ have types of truth values, that is, $\tau _{j} \equiv \mathsf{t}$ or $\tau _{j} \equiv \, \widetilde{\mathsf{t}}$ ; and $\sigma _{i} \equiv \mathsf{t}$ or $\sigma _{i} \equiv \, \widetilde{\mathsf{t}}$ .

3. (3) Each $C_j^{\tau _j} \in {\mathsf{Terms}}$ is proper;

4. (4) Each $R_{i}^{\sigma _{i}} \in {\mathsf{Terms}}$ in $\overrightarrow {R^{\sigma }}$ is immediate;

5. (5) All $c_j \in {\mathsf{RecV}}_{\tau _{j} }$ are fresh with respect to $A_{0}$ , $\overrightarrow {C^{\tau }}$ , and $\overrightarrow {R^{\sigma }}$ .

Then, there are two cases for the reduction rule for the restrictor terms:

1. (st1) $A_0 \in {\mathsf{Terms}}$ is immediate

   (st1) \begin{align} \begin{split} &( A_0\ {\mathsf{such\ that}}{}\ \{ C_1, \ldots , C_m, \overrightarrow {R} \} ) \\ \Rightarrow {} & ( A_0 \ {\mathsf{such\ that}}{}\ \{ c_1, \ldots , c_m , \overrightarrow {R} \} ) \\ & \qquad\quad \mathsf{where}\, \{ c_1 := C_1, \ \ldots , c_m := C_m \} \end{split} \end{align}

   for fresh $c_j \in {\mathsf{RecV}}$ ( $j=1, \ldots , m$ )

2. (st2) $A_0 \in {\mathsf{Terms}}$ is proper

   (st2) \begin{align} \begin{split} ( A_0 &\ {\mathsf{such\ that}}{}\ \{ C_1, \ldots , C_m, \overrightarrow {R} \} ) \\ \Rightarrow {} ( a_0 &\ {\mathsf{such\ that}}{}\ \{ c_1, \ldots , c_m , \overrightarrow {R} \} ) \\ & \hspace {3ex} \,\mathsf{where}\, \{ a_0 := A_0, \ c_1 := C_1, \ \ldots , c_m := C_m \} \end{split} \end{align}

   for fresh $a_0, c_j \in {\mathsf{RecV}}$ ( $j=1, \ldots , m$ ).

1. $\gamma ^*$ -Rule

   (29a) \begin{align} \begin{split} A \equiv _{\mathsf{c}} & A_{0} \,\mathsf{where}\, \lbrace \overrightarrow {a} := \overrightarrow {A}, \,p := \lambda (\overrightarrow {u}) \lambda (v) P, \,\overrightarrow {b} := \overrightarrow {B}\! \rbrace \end{split}\\[-29pt]\nonumber \end{align}
   (γ^*) \begin{align} \begin{split} {\Rightarrow _{\gamma ^*}}{}& A'_{0} \,\mathsf{where}\, \lbrace \overrightarrow {a} := \overrightarrow {A}', \, p' := \lambda (\overrightarrow {u}) P, \,\overrightarrow {b} := \overrightarrow {B'} \rbrace \end{split} \end{align}
   (29b) \begin{align} \begin{split} \equiv {} & A_{0}\{ p(\overrightarrow {u})(v) :\equiv p'(\overrightarrow {u}) \} \,\mathsf{where}\, \lbrace \,\\ & \hspace {18ex} \overrightarrow {a} := \overrightarrow {A}\{ p(\overrightarrow {u})(v) :\equiv p'(\overrightarrow {u}) \}, \\ & \hspace {18.5ex} p' := \lambda (\overrightarrow {u}) P, \, \\ & \hspace {18ex} \overrightarrow {b} := \overrightarrow {B}\{ p(\overrightarrow {u})(v) :\equiv p'(\overrightarrow {u}) \} \rbrace \end{split} \end{align}

   given that:

   1. − the term $A \in {\mathsf{Terms}}$ satisfies the $\gamma ^*$ -condition in Definition 9, for the assignment $p := \lambda (\overrightarrow {u})\lambda (v)P : (\overrightarrow {\vartheta } \to (\vartheta \to \tau ) )$ ;

   2. − $p' \in {\mathsf{RecV}}_{(\overrightarrow {\vartheta } \to \tau )}$ is a fresh recursion variable;

   3. − for each part $X_i$ of $\overrightarrow {X}$ in ( $\gamma^{*}$ ) (i.e., for each $X_i \equiv A_i$ in $\overrightarrow {X} \equiv \overrightarrow {A}$ , and each $X_i \equiv B_i$ in $\overrightarrow {X} \equiv \overrightarrow {B}$ ), $X'_i$ is the result of the free replacements $X'_i \equiv X_i\{ p(\overrightarrow {u})(v) :\equiv p'(\overrightarrow {u}) \}$ of all occurrences of $p(\overrightarrow {u})(v)$ by $p'(\overrightarrow {u})$ (in the free occurrences of $p$ ), modulo renaming the variables $\overrightarrow {u}, v$ , for $i \in \{0, \ldots , n_X \}$ , that is,

      (30) \begin{align} \overrightarrow {X'} \equiv \overrightarrow {X}\{ p(\overrightarrow {u})(v) :\equiv p'(\overrightarrow {u}) \} \end{align}

Definition 9 ( $\gamma ^*$ -Condition).

Assume that, for all $i=1, \ldots , n$ ( $n \geq 0$ ), $\tau , \vartheta , \vartheta _i \in {\mathsf{Types}}$ , $v, u_i \in {\mathsf{PureV}}$ , $p \in {\mathsf{RecV}}$ , and $P \in {\mathsf{Terms}}$ are such that $v : \vartheta$ , $u_i : \vartheta _i$ , $p : (\overrightarrow {\vartheta } \to (\vartheta \to \tau ) )$ , $P : \tau$ , and thus, $\lambda (\overrightarrow {u}^{\overrightarrow {\vartheta }} ) \lambda (v^{\vartheta }) (P^{\tau }) : (\overrightarrow {\vartheta } \to (\vartheta \to \tau ) )$ .

A recursion term $A \in {\mathsf{Terms}}$ satisfies the $\gamma ^*$ -condition for an assignment $p := \lambda (\overrightarrow {u}^{\overrightarrow {\vartheta }} ) \lambda (v^{\vartheta }) $ $(P^{\tau }) :(\overrightarrow {\vartheta } \to (\vartheta \to \tau ) )$ , with respect to $\lambda (v)$ , if and only if $A$ is of the form (31):

(31) \begin{align} A &\equiv A_{0}\,\mathsf{where}\, \lbrace \overrightarrow {a} := \overrightarrow {A}, \, p := \lambda (\overrightarrow {u}) \lambda (v)P, \overrightarrow {b} := \overrightarrow {B}\! \rbrace \end{align}

with the subterms of appropriate types, such that the following holds:

1. (1) $P \in {\mathsf{Terms}}_{\tau }$ does not have any free occurrences of $v$ , that is, $v \not \in {\mathsf{FreeV}}(P)$

2. (2) All occurrences of $p$ in $A_{0}$ , $\overrightarrow {A}$ , and $\overrightarrow {B}$ :

   1. (a) are free in $A_{0}$ , $\overrightarrow {A}$ , and $\overrightarrow {B}$ , that is, not in the scope of $\,\mathsf{where}\,$ -recursion assignments;

   2. (b) are occurrences in subterms $p(\overrightarrow {u})(v)$ , which are in a binding scope of $\xi (v)$ , for $\xi \in \{ \lambda , \exists , \forall \}$ , modulo renaming bound variables $\overrightarrow {u}, v$ , $i=1, \ldots , n$ ( $n \geq 0$ ).

Note: the latter requirement (b) maintains the sets of the free variables of the terms $A$ by the $\gamma ^*$ reductions.

The additional reduction ( $\gamma^{*}$ ) rule is introduced in Loukanova (Reference Loukanova, van den Herik and Rocha2019c) and extends the reduction calculus of $\operatorname {L^{\lambda }_{ar}}$ of Moschovakis (Reference Moschovakis2006), by reducing the complexity of the terms and their algorithmic semantics.

The more simple $\gamma$ -rule introduced in Loukanova (Reference Loukanova2019b) is a special case of the ( $\gamma^{*}$ ) rule. Both rules, $\gamma$ - and $\gamma ^{*}$ , simplify terms, by reducing subterms that have superfluous $\lambda$ -abstractions, $p := \lambda (v) P$ , for $v \not \in {\mathsf{FreeV}}(P)$ , and corresponding functional applications $p (T)$ that have constant values. The ( $\gamma^{*}$ ) rule is more versatile and more useful than the $\gamma$ -rule for such algorithmic simplifications. A sequence of multiple consecutive $\lambda$ -abstractions in an assignment part $p := \lambda (\overrightarrow {u}) \lambda (v) P$ of a recursion term $A$ , for $u_{i} \in \overrightarrow {u}$ , $v \not \in {\mathsf{FreeV}}(P)$ , can be such that $\overrightarrow {u} \in {\mathsf{FreeV}}(P)$ . This prevents application of the simple $\gamma$ -rule with respect to $\lambda (v)$ in $p := \lambda (\overrightarrow {u}) \lambda (v) P$ . The ( $\gamma^{*}$ ) rule provides reducing $A$ by removing the vacuous $\lambda (v)$ with respect to $p := \lambda (\overrightarrow {u}) \lambda (v) P$ . The ( $\gamma^{*}$ ) rule does not alter algorithmic semantics of $\operatorname {L^{\lambda }_{ar}}$ and $\operatorname {L}^{\lambda }_{r}$ , in any other essential way.

Definition 10 ( $\gamma ^*$ -Reduction).

For all $A, B \in {\mathsf{Terms}}$ , $A \Rightarrow ^{*}_{\gamma ^*} B$ iff there is a sequence (including empty one) of consecutive, immediate reductions by (cong)–( $\gamma^{*}$ ), that is:

(32) \begin{align} \begin{split} A \Rightarrow ^{*}_{\gamma ^*} B \iff &\textit{ there exist } A_{i} \in {\mathsf{Terms}}, 0 \leq i \leq n, \textit{ such that:} \\ & A \equiv A_{0}, \ A_{n} \equiv B, \textit{ and } \\ & A_{i} \Rightarrow A_{i+1}, \textit{ for some of the rules} (cong){-}(\gamma^{*}) \end{split} \end{align}

(33) \begin{align} \iff &\textit{ (abbreviated) } A \equiv A_{0} \Rightarrow \ldots \Rightarrow A_{n} \equiv B \ (n \geq 0) \end{align}

Often, we shall write $A \Rightarrow B$ instead of $A \Rightarrow ^{*}_{\gamma ^*} B$ , including when applying none or more than one rule. We shall avoide confusion between application of the individual ( $\gamma^{*}$ ) rule and any of the reduction rules. An application of the ( $\gamma^{*}$ ) rule to $A \in {\mathsf{Terms}}$ can be designated by $A {\Rightarrow _{(\gamma ^*)}} B$ , or by $A \Rightarrow ^{n}_{(\gamma *)} B$ when ( $\gamma^{*}$ ) rule has been applied $n$ ( $n \geq 0$ ) times.

Let $\operatorname {\mathfrak{A}}$ be a given semantic structure having a denotation function $ {\mathsf{den}}$ . In this paper, we do not include details about the denotational semantics and its denotation function. About such, see Moschovakis (Reference Moschovakis2006) and Loukanova (Reference Loukanova2019b, Reference Loukanova2023c, Reference Loukanova2023d, Reference Loukanova, Bekki, Mineshima and McCready2024).

For getting feeling of the essence of the ( $\gamma^{*}$ ) rule, we include the following statements.

Lemma 1. Assume that, for $i=1, \ldots , n$ ( $n \geq 0$ ),

$\tau , \vartheta , \vartheta _i \in {\mathsf{Types}}$ , $v, u_i \in {\mathsf{PureV}}$ , $p \in {\mathsf{RecV}}$ , $P \in {\mathsf{Terms}}_{\tau }$ ,

$v : \vartheta$ , $u_i : \vartheta _i$ , $p : (\overrightarrow {\vartheta } \to (\vartheta \to \tau ) )$ , $P : \tau$ , $p \not \in {\mathsf{FreeV}}(P)$ , and a given variable valuation $g$ is such that (34) holds:

(34) \begin{align} g (p) = & {\mathsf{den}} \bigl ( \lambda (\overrightarrow {u} ) \lambda (v) (P) \bigr ) (g) \end{align}

Then, for all $\overrightarrow {T}^{\overrightarrow {\vartheta }} \in {\mathsf{Terms}}_{\overrightarrow {\vartheta }}$ , $T^{\vartheta } \in {\mathsf{Terms}}_{\vartheta }$ , such that Footnote ¹ $v \not \in {\mathsf{FreeV}}(\overrightarrow {T})$ , the following (35a), (35b), and (36a)–(36c) hold:

(35a) \begin{align} \lambda (\overrightarrow {u} ) \lambda (v) (P) \equiv {} & \lambda (\overrightarrow {u}^{\overrightarrow {\vartheta }} ) \lambda (v^{\vartheta }) (P^{\tau }) : (\overrightarrow {\vartheta } \to (\vartheta \to \tau ) ) \end{align}

(35b) \begin{align} {\mathsf{den}} (p (\overrightarrow {T}) (T)) (g) = & {\mathsf{den}} \bigl ( \bigl [ \lambda (\overrightarrow {u} ) \lambda (v) (P) \bigr] (\overrightarrow {T}) (T) \bigr ) (g) \end{align}

Furthermore, assume that $v \not \in {\mathsf{FreeV}}(P)$ (as given in Definition 9 of the $\gamma ^*$ -Condition). Then, by the assumed types:

(36a) \begin{align} {\mathsf{den}} \bigl ( \bigl [ \lambda (v) (P) \bigr] (T) \bigr ) (g) &= {\mathsf{den}}(P) (g) \end{align}

(36b) \begin{align} {\mathsf{den}}(p (\overrightarrow {T}) (T)) (g) &= {\mathsf{den}} \bigl ( \bigl [ \lambda (\overrightarrow {u} ) \lambda (v) (P) \bigr] (\overrightarrow {T}) (T) \bigr ) (g) \end{align}

(36c) \begin{align} &= {\mathsf{den}} \bigl ( \bigl [ \lambda (\overrightarrow {u} ) (P) \bigr] (\overrightarrow {T}) \bigr ) (g) \end{align}

Thus, ( $\gamma^{*}$ ) rule does not affect the denotational semantics of $\operatorname {L^{\lambda }_{ar}}$ and $\operatorname {L}^{\lambda }_{r}$ , that is,

Theorem 2. In any given semantic structure $\operatorname {\mathfrak{A}}$ having a denotation function $ {\mathsf{den}}^{\operatorname {\mathfrak{A}}}$ :

(37) \begin{align} \begin{split} &\textit{ for all } A, A',\textit{ such that } A {\Rightarrow _{\gamma ^*}} A', \textit{ it holds that:} \\ & {\mathsf{den}}^{\operatorname {\mathfrak{A}}}(A) = {\mathsf{den}}^{\operatorname {\mathfrak{A}}}(A') \end{split} \end{align}

See detailed motivations, examples, and properties of the ( $\gamma^{*}$ ) and $\gamma$ -rule in the papers that are devoted to these rules and the corresponding extended reduction calculi, see Loukanova (Reference Loukanova2019b, Reference Loukanova, van den Herik and Rocha2019c, Reference Loukanova2023c). Further motivations and examples of the utility of the ( $\gamma^{*}$ ) rule are provided in Loukanova (Reference Loukanova2016b, Reference Loukanova, Grabowski, Loukanova and Schwarzweller2020, Reference Loukanova2023b, Reference Loukanova2023d).

Definition 11 ( $\gamma ^*$ -Irreducible terms).

We say that a term $A \in {\mathsf{Terms}}$ is $\gamma ^*$ - $\mathrm{irreducible}$ if and only if (38) holds:

(38) \begin{align} \begin{split} \textit{ for all } B \in {\mathsf{Terms}}, \quad A \Rightarrow ^{*}_{\gamma ^*} B &\implies A \equiv _{\mathsf{c}} B \end{split} \end{align}

For any term $A$ that is $\gamma ^*$ -irreducible, we say that $A$ is irreducible.

4.3 Canonical forms of terms

We use the notation $ {\mathsf{cf}}_{\gamma ^*}(A) \equiv {\mathsf{cf}}(A)$ as in Definition 7 of the Canonical Forms of Terms.

On the algorithmic semantics of the formal language of type-theory of recursion. The algorithmic meaning of a proper $A \in {\mathsf{Terms}}$ , that is, a non-immediate, algorithmically meaningful term, is designated by $ {\mathsf{alg}}(A)$ . It is determined by its canonical form $ {\mathsf{cf}}_{\gamma ^*}(A) \equiv {\mathsf{cf}}(A)$ .

Intuitively, for each proper $A\in {\mathsf{Terms}}$ , the algorithm $ {\mathsf{alg}}(A)$ for computing its denotation $ {\mathsf{den}} (A)$ consists of computation steps provided by the parts $A_{i}$ of its canonical form $ {\mathsf{cf}}(A) \equiv {A_0 \,\mathsf{where}\, \{p_1 := A_1, \ldots , p_n := A_n}\}$ , according to their $ {\mathsf{rank}} (A_{i})$ . Since the parts $A_{i}$ of the $ {\mathsf{cf}}(A)$ are explicit and irreducible, the computations for memorizing the values $ {\mathsf{den}}(A_{i})$ of the parts in the memory slots $p_{i}$ , by the assignments $p_{i} := A_{i}$ , are computationally the most basic. When the computational steps start from the lowest $ {\mathsf{rank}} (A_{i})$ , the algorithm for computing $ {\mathsf{den}}(A)$ is by iteration, that is, by recursive iteration.

For every $A \in {\mathsf{Terms}}$ , its canonical form $ {\mathsf{cf}}(A)$ , that is, $ {\mathsf{cf}}_{\gamma ^*}(A)$ , is obtained from $A$ by the reduction calculus of $\operatorname {L^{\lambda }_{ar}}$ , introduced in Section 4.2.

When $A \approx _{\gamma ^*} B$ , we say that $A$ and $B$ are algorithmically $\gamma ^*$ -equivalent, alternatively, that $A$ and $B$ are $\gamma ^*$ -synonymous in $\operatorname {\mathfrak{A}}$ . Often, we skip the label $\gamma ^{*}$ and mentioning $\operatorname {\mathfrak{A}}$ , when the context makes these clear, that is:

• • We write $A \approx B$ and $ {\mathsf{cf}}(A) \approx {\mathsf{cf}}(B)$ , and say that $A$ and $B$ are algorithmically equivalent.

• • We write $ {\mathsf{den}}(A) = {\mathsf{den}}(B)$ and $A=B$ , and say that $A$ and $B$ are denotationally equivalent.

8.1 Core semantic equivalence of a transfer between active and passive forms

The term $M_{0}$ in (52b) is a standard translation of such a sentence in lambda-calculi and in logic. The significance that $\operatorname {L^{\lambda }_{ar}}$ adds to it is that this terms can be reduced to its canonical form in $\operatorname {L^{\lambda }_{ar}}$ that designates the algorithmic steps in computing its denotation:

(52a) \begin{align} &\text{ Mary liked Jim} \xrightarrow {\mathsf{render}}{} M_{0}\\[-10pt]\nonumber \end{align}

(52b) \begin{align} M_{0} \equiv {} & [\textit{liked} (\textit{jim})](\textit{mary})\\[-10pt]\nonumber \end{align}

(52c) \begin{align} \Rightarrow {} \ldots \Rightarrow {} {\mathsf{cf}}(M_{0}) \equiv {} & \textit{liked} (j)(m) \,\mathsf{where}\, \{ j := \textit{jim}, \, m := \textit{mary} \}\\ &\text{ by 2x(ap) twice, (rec-comp), (recap), (head)}\nonumber \end{align}

In (53a) and (53b), I present another randering of the same sentence in the active form, (52a), to a different $\operatorname {L^{\lambda }_{ar}}$ term $ {\mathsf{cf}}(T)$ , in (53b), which provides a generalization to a parametric algorithm for computing denotations of classes of sentences via instantiations:

(53a) \begin{align} &\text{ Mary liked Jim} \xrightarrow {\mathsf{render}}{} {\mathsf{cf}}(T)\\[-10pt]\nonumber \end{align}

(53b) \begin{align} T \equiv {} & [L (\textit{jim})](\textit{mary}) \,\mathsf{where}\, \{ L := \textit{liked} \}\\[-10pt]\nonumber \end{align}

(53c) \begin{align} \Rightarrow {} \ldots \Rightarrow {} {\mathsf{cf}}(T) \equiv {} & L (j)(m) \,\mathsf{where}\, \{ L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \}\\ &\text{ by 2x(ap) twice, (rec-comp), (recap), (head)}\nonumber \end{align}

As a first option, let’s assume that the sentence (54a) in passive form is rendered to the term (54b), where the order of the $\lambda$ -abstractions over the arguments provides correspondence to the reordering of the syntactic arguments in (54a).

Corollary 1. The terms $B$ and $T$ in (54b) and (54c) are algorithmically equivalent, $B \approx {} T$ :

(54a) \begin{align} &\textit{ Jim is liked by Mary} \xrightarrow {\mathsf{render}}{} B \equiv {} {\mathsf{cf}}(B)\\[-10pt]\nonumber \end{align}

(54b) \begin{align} \begin{split} B \equiv {} & \bigl ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr ) (m) (j) \,\mathsf{where}\, \{ \\ & \qquad\quad\qquad L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{split}\\[-10pt]\nonumber \end{align}

(54c) \begin{align} B \approx {} T \equiv {} & L (j)(m) \,\mathsf{where}\, \{ L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{align}

Proof. The head parts of $B$ and $T$ in (54b) and (54c) are denotationally equivalent, by two denotational $\beta$ -conversions, that is,

(55) \begin{align} & \bigl ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr ) (m) (j) = L (j)(m) \end{align}

The terms $B$ and $T$ are proper, and their corresponding parts are explicit, irreducible, and denotationally equivalent. Therefore, by Definition 12, it follows that $B \approx {} T$ .

The canonical form $ {\mathsf{cf}}(T)$ of the active sentence in (53a) is algorithmically equivalent of the canonical form $ {\mathsf{cf}}(B)$ , by the above renderings, that is,

(56) \begin{align} B \approx {}& {\mathsf{cf}}(B) \equiv {} T \equiv {} {\mathsf{cf}}(T) \approx {} T \end{align}

This may seem as if being a discrepancy, but the important is that none of the terms $T \equiv {} {\mathsf{cf}}(T) \approx T$ is per se syntactically equivalent to $B \approx {} {\mathsf{cf}}(B)$ . There is formal syntactic difference between the canonical forms of the $\operatorname {L^{\lambda }_{ar}}$ terms rendering the corresponding active $ {\mathsf{cf}}(T)$ and passive $ {\mathsf{cf}}(B)$ forms.

The algorithmic equivalence $B \approx {} T$ , via (56), reflects on important linguistic information in NL, that is, the essential, core semantic event designated by a typical passive form of a sentence is the same as that of the corresponding active one. In the next sections, I show that the recursion variables and reduction calculus of $\operatorname {L^{\lambda }_{ar}}$ provide facility for algorithmic distinction between the active and passive expressions of the core semantic event in them, via the passivization role of the passive copula be. It is a passivization marker that blocks, that is, prevents the (second) $\beta$ -conversion over the semantic argument role that gets passivized, that is, over the one which is designated by the complement of the active sentence and promoted to the subject in the passive one.

9.1 The verb “be” as a passivization marker

When the lexeme “be” enters into a phrasal structure of a passive sentence, the function denoted by the constant $\textit{be}$ applies to and preserves the same property (the action) $X$ of type $(\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}})$ , which is designated by the syntactic complement (i.e., the passive VP[form pass]) of the lexeme “be,” acting over entities of type $\tilde {\mathsf{e}}$ , designated by the sentence subject.

For the purposes of this paper, that is, syntax–semantics of passivization in English, expressed by feature-value description (74), I assume that the lexeme “be” is rendered to a $\operatorname {L^{\lambda }_{ar}}$ -constant $\textit{be}$ that denotes the identity function over properties denoted by $X \in {\mathsf{Terms}}_{(\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}})}$ . The denotation $ {\mathsf{den}}(\textit{be})$ is expressed by (57a)–(57c), and similarly, for the inflected forms $\textit{is}$ , $\textit{was}$ , etc., if we suppress information about time carried by inflection:

(57a) \begin{align} \begin{split} & \textit{be} \in {\mathsf{Consts}}_{((\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}))}, \\ & \text{ such that, for a given }X \in {\mathsf{Terms}}_{(\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}})}\!: \textit{be} (X) = X \end{split}\\[-10pt]\nonumber \end{align}

(57b) \begin{align} \begin{split} & \text{ i.e., for a given variable valuation $g$: } \\ & {\mathsf{den}}( \textit{be} (X) ) (g) = {\mathsf{den}}(\textit{be}) \bigl [ {\mathsf{den}}(X) \bigr] (g) = {\mathsf{den}}(X) (g) \end{split}\\[-10pt]\nonumber \end{align}

(57c) \begin{align} &\textit{be} (X) = X \qquad \text{ iff } \qquad \textit{be} (X) {\models {\!|}} X \hspace {10ex} \text{ (denotational equality)}\\[-10pt]\nonumber \end{align}

(57d) \begin{align} &\textit{is} (X) = X, \ \textit{was} (X) = X, \ldots \end{align}

That is, predicatively: $ {\mathsf{den}}( \textit{be} [ \textit{liked} (\textit{jim})] ) = {\mathsf{den}}( \textit{liked} (\textit{jim}) )$ , by suppressing tense information provided by inflection.

Compositionally, the sentence (58a) can be rendered as in (58b) and (58c). Then, by the reduction rules, we get (58f) and (58g) and its canonical form in (58l)–(58m):

(58a) \begin{align} &\text{ Jim is liked by Mary} \end{align}

(58b) \begin{align} \xrightarrow {\mathsf{render}}{} & A \equiv {} \Bigl [ \textit{is} \bigl [\underbrace { \underbrace {( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) ) }_{ [\text{L-ed}]_{ [\textit {part-lxm pass}] } } (\textit{mary}) }_{\mathrm{[ L-ed\ by\ Mary]\, \textrm {VP}[\textit {pass}] }} \bigr] \Bigr] (\textit{jim}) \,\mathsf{where}\, \{ \end{align}

(58c) \begin{align} & \hspace {40ex} L := \textit{liked} \} \end{align}

(58d) \begin{align} \Rightarrow {} \ldots \Rightarrow {} A' \equiv {} & \bigl [ \textit{is} \bigl [( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) ) (m) \ \bigr] \bigr] (j) \,\mathsf{where}\, \{\\[-10pt]\nonumber \end{align}

(58e) \begin{align} & \hspace {20ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \}\\ &\text{ by 2x(ap) twice, (rec-comp), (recap), (head)} \nonumber\\[-8pt]\nonumber \end{align}

(58f) \begin{align} \equiv {}& \underbrace { \bigl [ \textit{is} \bigl [\underbrace { \underbrace { ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) ) }_{[\text{L-ed}]_{ [\textit {part-lxm pass}] } \xrightarrow {\mathsf{render}}{} A_{0,0} } (m) }_{\text{ [L-ed by } m] \ \mathrm{VP}[\textit {pass}] \xrightarrow {\mathsf{render}}{} A_{0,1} } \bigr] \bigr] }_{\mathrm{ is } [\text{L-ed by } m] \textrm {VP}[\textit {pass}] \xrightarrow {\mathsf{render}}{} A_{0,2} } (j) \,\mathsf{where}\, \left \{\right . \end{align}

(58g) \begin{align} & \hspace {20ex} \underbrace {L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary}}_{\text{ specifications can be removed}}\! \left .\right \} \end{align}

(58h) \begin{align} \Rightarrow {} & \Bigl [ [ \textit{is} (P)] \,\mathsf{where}\, \{ P := \bigl ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr ) (m) \} \Bigr] (j) \end{align}

(58i) \begin{align} & \hspace {12ex} \,\mathsf{where}\, \{ \underbrace { L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} }_{\text{ specifications can be removed}} \}\\ &\text{ by (ap), (ap-comp), (rec-comp)}\nonumber \end{align}

(58j) \begin{align} \Rightarrow {} & \Bigl [ [ \textit{is} (P)](j) \,\mathsf{where}\, \{ P := \bigl ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr ) (m) \} \Bigr] \end{align}

(58k) \begin{align} & \hspace {12ex} \,\mathsf{where}\, \{ \underbrace { L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} }_{\text{ specifications can be removed}} \}\\ &\text{ by (recap), (rec-comp)}\nonumber \end{align}

(58l) \begin{align} \Rightarrow {} & {\mathsf{cf}}(A) \equiv {} & \\ & [ \textit{is} (P)](j) \,\mathsf{where}\, \{ P := \underbrace {\bigl ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr ) (m), }_{\text{ [L-ed by $m$]} \ \mathrm{VP}[\textit {pass}] \xrightarrow {\mathsf{render}}{} A_{0,1}}\nonumber \end{align}

(58m) \begin{align} & \hspace {18ex} \underbrace {L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} }_{\text{ specifications can be removed}} \}\\ &\text{ by (head)} \nonumber \\ \approx {} & M \equiv {} {\mathsf{cf}}(M) \equiv {} \nonumber \end{align}

(58n) \begin{align} & P(j) \,\mathsf{where}\, \{ P := \underbrace {\bigl ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr ) (m), }_{\text{ [L-ed by $m$]} \ \mathrm{VP}[\textit {pass}] \xrightarrow {\mathsf{render}}{} A_{0,1} } \end{align}

(58o) \begin{align} & \hspace {18ex} \underbrace {L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} }_{\text{ specifications can be removed}} \}\\ \nonumber &\text{ by (57d) for}\ \textit{is} (P) = P \end{align}

Optionally, instead of (58a) and (58b), we can render the same sentence (58a) directly to $ {\mathsf{cf}}(A)$ :

(59) \begin{align} &\text{ Jim is liked by Mary} \xrightarrow {\mathsf{render}}{} {\mathsf{cf}}(A) \end{align}

Passivization by “be” marker. In terms like (58b) and (58c) and (60a) and (60b), the $\operatorname {L^{\lambda }_{ar}}$ subterm $\textit{is}$ , which renders the passive copula, has a special role. It is a passivization “marker” that prevents denotational $\beta$ -substitution in the canonical forms. By this, it blocks algorithmic equivalence between passive and active renderings.

Now, let’s consider the term $R$ in (60a) and (60b), which is received from $A'$ in (58d) and (58e), by denotational $\beta$ -substitution of the bound variable $y_{m}$ with $m$ , in the head part of $A'$ . The terms $A'$ and $R$ are denotationally equivalent, that is, $A' = R$ , but we cannot directly conclude that $A \approx A' \approx R$ . We prove that this holds below.

By the reduction calculus of $\operatorname {L^{\lambda }_{ar}}$ , we have the following reductions of $R$ to its canonical form $ {\mathsf{cf}}(R)$ , and $R \approx {\mathsf{cf}}(R)$ :

(60a) \begin{align} R & \equiv {} \bigl [ \textit{is} \bigl [\bigl( \lambda x_{j} \bigl [L (x_{j}) (m) \bigr] \bigr) \bigr] \bigr] (j) \,\mathsf{where}\, \{ \end{align}

(60b) \begin{align} & \hspace {24ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{align}

(60c) \begin{align} R & \equiv {} \underbrace { \bigl [ \textit{is} \bigl [\underbrace { ( \lambda x_{j} \bigl [L (x_{j}) (m) \bigr] ) }_{\text{[L-ed by }m] \mathrm{VP}[\textit {pass}] \xrightarrow {\mathsf{render}}{} R_{0,1} } \bigr] \bigr] }_{\text{ is [L-ed by }m] \mathrm{VP}[\textit {pass}] \xrightarrow {\mathsf{render}}{} R_{0,2} } (j) \,\mathsf{where}\, \{ \end{align}

(60d) \begin{align} & \hspace {24ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{align}

(60e) \begin{align} \Rightarrow {} & \bigl [ \textit{is} (R_{0,1}) \,\mathsf{where}\, \bigl\{ R_{0,1} := \lambda x_{j} \bigl [L (x_{j}) (m) \bigr] \bigr\} \bigr] (j) \,\mathsf{where}\, \{ \end{align}

(60f) \begin{align} & \hspace {24ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{align}

(60g) \begin{align} &\text{ by (ap) to the head subterm and (rec-comp)} \nonumber \\ \Rightarrow {} & \bigl [ \bigl [ \textit{is} (R_{0,1}) \bigr] (j) \,\mathsf{where}\, \bigl\{ R_{0,1} := \lambda x_{j} \bigl [L (x_{j}) (m) \bigr] \bigr\} \bigr] \,\mathsf{where}\, \{ \end{align}

(60h) \begin{align} & \hspace {22ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{align}

(60i) \begin{align} &\text{ by (recap) to the head subterm and (rec-comp)}\nonumber \\ \Rightarrow {} & \bigl [\textit{is} (R_{0,1} ) \bigr] (j) \,\mathsf{where}\, \{ R_{0,1} := \lambda x_{j} \bigl [L (x_{j}) (m) \bigr], \, \end{align}

(60j) \begin{align} & \hspace {22ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{align}

(60k) \begin{align} \nonumber &\text{ by (head)} \\ \Rightarrow {} {\mathsf{cf}}(R) \equiv {} & \bigl [\textit{is} (P ) \bigr] (j) \,\mathsf{where}\, \{ P := \lambda x_{j} \bigl [L (x_{j}) (m) \bigr], \, \end{align}

(60l) \begin{align} & \hspace {22ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \} \end{align}

(60m) \begin{align} \nonumber &\text{ by (cong) renaming of the bound } R_{0,1} \text{ to } P \\ \approx {} {\mathsf{cf}}(R') \equiv {} & \bigl [ P(j) \,\mathsf{where}\, \{ P := \lambda x_{j} \bigl [L (x_{j}) (m) \bigr], \, \end{align}

(60n) \begin{align} & \hspace {22ex} L := \textit{liked}, \, j := \textit{jim}, \, m := \textit{mary} \}\\ \nonumber &\text{ by (57d) for } \textit{is} (P) = P \end{align}

Informally, the head term (60k)–(60l) expresses that $j$ is $P$ , where $P$ is [L-ed by $m$ ], that is $j$ is liked by $m$ .

Corollary 2. For the terms $A$ , $A'$ , $ {\mathsf{cf}}(A)$ , $R$ , and $ {\mathsf{cf}}(R)$ , respectively, in (58a)–(58m) and (60a)–(60j), the following algorithmic equivalences hold:

(61) \begin{align} A \approx {} A' \approx {} {\mathsf{cf}}(A) \approx {} R \approx {} {\mathsf{cf}}(R) \end{align}

Proof.

(62a) \begin{align} {\mathsf{den}} \bigl ( \bigl [ \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr] (m) \bigr ) &= {\mathsf{den}} \bigl ( \lambda x_{j} L (x_{j}) (m) \bigr ) \end{align}

Therefore, $ {\mathsf{cf}}(A) \approx {} {\mathsf{cf}}(R)$ , by Definition 12.

9.2 Generalized parametric algorithms of passivization via passivization marker

From (58a), (58c)–(58d), and (53a)–(53c), by removing the specific instantiations of the lexical renderings into recursion variables for memory slots, we get the following algorithmic patterns, in canonical forms:

Algorithmic p attern of a ctive s entences . Let’s assume that the passivization copulas “be,” respectively inflected, are rendered into $\operatorname {L^{\lambda }_{ar}}$ terms:

$\textit{be} \in {\mathsf{Consts}}_{((\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}))}$ ,

$\textit{is}, \ \textit{was}, \ldots \in {\mathsf{Terms}}_{((\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}))}$ .

Assume the following:

$j, m \in {\mathsf{RecV}}_{\tilde {\mathsf{e} } }$ , which we use for saving in them values of terms rendering NPs denoting entities;

$L \in {\mathsf{RecV}}_{( \tilde {\mathsf{e}} \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) ) }$ , for saving the denotations of terms denoting two-argument relations, encoded by currying, that is, a class of relations of type: $( \tilde {\mathsf{e}} \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) )$ .

We generalize the example rendering (53a)–(53c), by skiping the specific instantiations of lexemes, we get the following parametric algorithm for computing the denotations of a class of sentences with two-argument verbal head:

(63a) \begin{align} & [ [\unicode{x1D6F7}]_{\mathrm{VP}} \ [ [\chi]_{\mathrm{V}} \ [\unicode{x1D6F9}]_{\mathrm{NP}}]_{\mathrm{VP}}]_{\mathrm{S}} \text{ (in active form)} \end{align}

(63b) \begin{align} \xrightarrow {\mathsf{render}}{} & T \equiv {} {\mathsf{cf}}(T) \equiv {} L (j)(m) \end{align}

The general syntactic structures of sentences in active and corresponding passive form given in (63a) and (64a) are syntactic schemes that are syntactically parametric. In them, $\unicode{x1D6F7}$ , $\unicode{x1D6F9}$ , and $\chi$ are auxiliary symbols, that is, meta-variables, not belonging to the NL under analysis, neither to the formal language $\operatorname {L^{\lambda }_{ar}}$ . They represent any grammatical NL expressions of the syntactic categories given as indices to the brackets.

On the other hand, the expressions $L(j)(m)$ in (63b), and also in (64b)–(64e), abbreviated by $A, {\mathsf{cf}}(A), {\mathsf{cf}}(R), {\mathsf{cf}}(M)$ , are well-formed $\operatorname {L^{\lambda }_{ar}}$ terms. The recursion variables $j,m, L$ are free recursion variables, that is, $\operatorname {L^{\lambda }_{ar}}$ terms, rendering correspondingly $ [\unicode{x1D6F9}]_{\mathrm{NP}}$ , $ [\unicode{x1D6F7}]_{\mathrm{NP}}$ , the verbal expression $\chi$ . They have to be of suitable $\operatorname {L^{\lambda }_{ar}}$ types, otherwise are not specified.

Algorithmic p attern of p assive s entences. From (58a) and (58b)–(58c), we get algorithmic patterns for computing the passive forms of the class of algorithms for the active sentences of the form (63a) and (63b). The specific algorithms are obtained by instantiations of the memory locations of the recursive variables $L$ , $m$ , $j$ :

(64a) \begin{align} \begin{split} & [ [\unicode{x1D6F9}]_{\mathrm{NP}} \ [\text{is} \ [ [ F_{\textit{passprt}} ( \chi )]_{\mathrm{V} [\mathrm{FORM} \, passprt]} \\ & \hspace {20ex} \ \Bigl ( [\text{by} \ [\unicode{x1D6F7}]_{\mathrm{NP}}]_{{\mathrm{PP}}} \Bigr )]_{\mathrm{VP} [\mathrm{FORM} \, pass] }]_{\mathrm{VP}[\mathrm{FORM} \, pass]}]_{\mathrm{S}} \\ & \hspace {28ex} \text{ (in corresponding passive form)} \\ \xrightarrow {\mathsf{render}}{} & A / {\mathsf{cf}}(A) / {\mathsf{cf}}(R) / {\mathsf{cf}}(M) \kern50pt\text{ (optional renderings)} \end{split} \end{align}

(64b) \begin{align} & A \equiv {} \bigl [ \textit{is} \bigl [ ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) ) (m) \bigr] \bigr] (j) \end{align}

(64c) \begin{align} \Rightarrow {} & {\mathsf{cf}}(A) \equiv {} [ \textit{is} (P)](j) \,\mathsf{where}\, \bigr\{ P := \underbrace {\bigl ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) \bigr ) (m)}_{\text{ [L-ed by } m] \ \mathrm{VP}[\textit {pass}] \xrightarrow {\mathsf{render}}{} A_{0,1} } \bigl\} \end{align}

(64d) \begin{align} \approx {} & {\mathsf{cf}}(R) \equiv {}\bigl [\textit{is} (P ) \bigr] (j) \,\mathsf{where}\, \bigr\{ P := \lambda x_{j} \bigl [L (x_{j}) (m) \bigr]\bigr\}\\[-10pt]\nonumber \end{align}

(64e) \begin{align} \approx {} & {\mathsf{cf}}(M) \equiv {}\bigl [ P \bigr] (j) \,\mathsf{where}\, \bigl\{ P := \lambda x_{j} \bigl [L (x_{j}) (m) \bigr] \bigr\} \end{align}

Optionality of the PP c omplement d esignating the a gent. We present the optional PP complement of the passives by inclosing that PP in parentheses. Note that the instantiations of the algorithmic patterns (64b)–(64e) by specific recursion assignments to the memory variables $j,m,L$ provided by specific instances of the semtence (64a).

See (78) for presenting the optionality of this PP in feature-structure description of the passive participle word “given” and examples of passive sentences.

In the cases when the optional PP complement [by $\unicode{x1D6F7}$ ] is skipped, the corresponding semantic role of the verbal term must be saturated. The formal language of $\operatorname {L^{\lambda }_{ar}}$ has its unique facility to present this semantically, by filling the corresponding semantic role by its variables, which can be a free recursion variable $m$ as in (64b)–(64e) . The memory variable $m$ tentatively designating the agent and rendered by $\unicode{x1D6F7}$ remains underspecified without any instantiation of it, even after the other memory variables are instantiated.

We can generalize the patterns of renderings of the passive forms (64a) by any one of the following options, which are algorithmically equivalent:

1. (1) (64b)

   Generalization of (58b)–(58c), by underspecification of the head verb, the subject, and the complement, and using the passivization marker $\textit{is}$ in (64a) acting on the terms renderings:

   1. (a) $\bigl [\textit{is} \bigl [ ( \lambda y_{m} \lambda x_{j} L (x_{j}) (y_{m}) ) (m) \bigr] \bigr]$ is rendering the passive VP: $\chi \xrightarrow {\mathsf{render}} L$ to be instantiated by the head verbal participle; $\unicode{x1D6F7} \xrightarrow {\mathsf{render}} m$ , to be instantiated by the rendering of $\unicode{x1D6F7}$ .

   2. (b) the rendering of the promoted new subject $j$ , to be instantiated by the rendering of $\unicode{x1D6F9}$ .

2. (2) (64c) the canonical form of (64b).

3. (3) (64d) from (64c) by algorithmic equivalence via denotational $\beta$ -conversion and by Definition 12.

4. (4) (64e) from (64d) without the rendering $\textit{is}$ of the copula verb “be,” by (57d) for $\textit{is} (P) = P$ , but after it has completed its role as a passivization marker and by moving the rendering of the passive VP into the memory variable (slot) $P$ .

Each one of the terms in the options (1)–(4) corresponds denotationally to the same core semantic event $L(j)(m)$ expressed by the active sentences of the form (63a)–(63b):

(65a) \begin{align} {\mathsf{den}}(A) &= {\mathsf{den}}( {\mathsf{cf}}(A)) = {\mathsf{den}}( {\mathsf{cf}}(R)) = {\mathsf{den}}( {\mathsf{cf}}(M)) = L(j)(m)\\[-10pt]\nonumber \end{align}

(65b) \begin{align} A &\approx {} {\mathsf{cf}}(A) \approx {} {\mathsf{cf}}(R) \approx {} {\mathsf{cf}}(M) \not \approx {} = L(j)(m) \end{align}

11.1 TTAA terms in syntax–semantics analysis of passives via feature-structure descriptions

The entry of the lexeme “be” can be given by a feature-structure description, for example, that in (74) (there may be other alternatives). The feature-structure description (74) represents a bare lexeme for the passive be, which is uninflected. It is a potential input to specific inflection rules:

(74)

Informally, in (74), the verb “be” has $\boxed {1}$ as its spr, by the feature-value description [spr $\langle$ $\boxed {1}$ np [agr $\boxed {4}$ ] $\rangle$ ]. That is, the syntactic subject of the verb “be” is $\boxed {1}$ , which is the same as the subject [spr $\langle$ $\boxed {1}$ $\rangle$ ] of its comps element $\boxed {2}$ . The lexeme “be” takes as a complement $\boxed {2}$ , expressed by the feature-value description comps $\langle$ $\boxed {2}$ $\rangle$ . And also, $\boxed {2}$ is the second argument element of its arg-st, by which $\boxed {2}$ is a VP in passive form and has a semantic representative of type $(\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}})$ .

The comps of “be” is not expressed explicitly in (74) because it is derived by the type constraints in syntax–semantics of feature-structure descriptions.

The word feature-structure description (76) for the past form of the passive be can be licensed by an inflectional lexical rule Past 3rd-Singular Tense Verb Lexical Rule, which is defined similarly to the Present Continuous 3rd-Singular Tense Verb Lexical Rule in Loukanova (Reference Loukanova, Bel-Enguix, Dahl and Jiménez-López2011e).

The underspecified $W^{((\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}))} \in {\mathsf{Terms}}$ renders the inflected word “was,” where the inflection information is rendered by a conjunction in (75b). The underspecification of $W$ is for the referring (utterance) state $u$ ; $ut$ is a location variable that saves the time of the referring (utterance) or predication state, via $\textit{ut} := \textit{lt} (u)$ :

(75a) \begin{align} \mathsf{was} & \xrightarrow {\mathsf{render}} W \end{align}

(75b) \begin{align} W & \equiv \lambda (v) \, \lambda (x) \, \lambda (s) \bigl [ w(v)(x)(s) \land t(s) \bigr] \,\mathsf{where}\, \{ w := \textit{be}, \, \end{align}

(75c) \begin{align} & \hspace {8ex} t := \lambda (s) \bigl ( \textit{lt}(s) \prec \textit{ut} \bigr ) , \, \textit{lt} := \textit{time}, \, \textit{ut} := \textit{lt} (u) \} \end{align}

(75d) \begin{align} & \hspace {2.5ex} : ((\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}})) \end{align}

In this section, we maintain the expression of the inflection of the passive was in the larger expressions by conjunction for the tense restrictions. Note that we can express this inflection information by restrictor terms, similarly to that in the active verbal forms in Section 10, which we use in Section 12.

The syntax–semantics interface of the underspecified passive word “was” can be represented by the feature-structure description (76), via suitable encoding of $W^{((\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}) \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}}))} \in {\mathsf{Terms}}$ as the value of the feature sem:

(76)

The feature-structure description (76) of the passive word “was” represents its underspecified syntax–semantics interface open for specifications by VPs in passive forms, where the verbal head can be instantiated by a passive participle.

In (75a)–(75c), the $\lambda (v)$ abstraction is over the passive verb phrase, $\lambda (x)$ is over the subject of the passive action (which is the complement in the active verbal phrase), the value $\textit{time} (s)$ is the time component of the state $s$ , and the value $\textit{time} (u)$ is the time component of the state $u$ of using the passive “be” expression.

In (75a)–(75c), and respectively (76), we may introduce the application of the head term, that is, of t-head term, to the free recursion variable $h \in {\mathsf{RecV}}_{(\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}})}$ as declaration, that is, reservation, of the free memory slot, of respective type, for passive VP having underspecified verbal passive participle. This memory slot can be specified by a class of VPs in passive form (where the verbal head is passive participle). Here, we refrain from this application to maintain the logic type of was.

11.2 Passive participle lexemes

In what follows, as a pattern for algorithmic syntax–semantics analysis of passive forms, I present two optional word feature structures of the passive participle lexemes “given,” (78) and (92), derived from the transitive lexeme give, for example, given in (77).

We can represent the syntax–semantics interface of the lexeme give by the feature-structure description (77):

(77)

The word pair consisting of a passive participle like “given” and its syntax–semantics interrelations can be represented by the feature-structure description (78):

(78)

Note that (77) is not restricted by the ARP, which applies to lexemes of type word, that is, the NP in the SPR list is not restricted to be identical to the first NP in the ARG-ST list. Then, there are two words “given” as the optional outputs of the Passive Lexical Rule followed by the Constant Lexeme Lexical Rule, (78) and (92). The word structure (78) has two complements in the COMPS list, where the feature description $\boxed {3}$ PP [syn [head [form by]]] represents the syntax–semantics information of the corresponding argument marking PP. Argument marking PPs can be presented by using a technique as in Loukanova and Jiménez-López (Reference Loukanova, Jiménez-López, Pérez, Sánchez, Mathieu, Rodríguez, Adam, Ortega, Moreno, Navarro, Hirsch, Lopes-Cardoso and Julián2012). The word structure (78) has two syntactic complements in its comps list, while the second one that is a PP is optional and can be skipped, for example, (92) has just one complement. In both cases, the $\operatorname {L^{\lambda }_{ar}}$ constant $\textit{give}$ has three semantic arguments:

(79a) \begin{align} & \textit{give} \in {\mathsf{Consts}}_{( \tilde {\mathsf{e}} \rightarrow (\tilde {\mathsf{e}} \rightarrow (\tilde {\mathsf{e}} \rightarrow \tilde {\mathsf{t}})) )} \end{align}

(79b) \begin{align} &\mathsf{given} \xrightarrow {\mathsf{render}} \ \big [\lambda x_j \lambda z_k \lambda y_f \, give(y_f)(x_j)(z_k)\big] \end{align}

Optionality of the PP complement designating the agent. In English, the subject of a sentence in active form, having as its verb head “give,” is a NP, which is obligatory. In a corresponding sentence of passive form this NP is transformed into the NP-head of a PP, [by NP] $_{\mathrm{PP}}$ . This PP is optionally skipped. I present this optionality by inclosing its corresponding feature-structure description $\boxed {3}$ in parentheses, in the argument-structure list value of arg-st (78).