Restricted Computations and Parameters in Type-Theory of Acyclic Recursion

Roussanka Loukanova

Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria
rloukanova@gmail.com

ABSTRACT

KEYWORD

1. Introduction

This paper is part of the author’s work on development of a new type-theory of the mathematical notion of algorithms, its concepts, and potentials for applications to advanced, computational technologies, especially in Artificial Intelligence (AI). For the initiation of this new theory, see the original work on the formal languages of recursion (FLR) (Moschovakis, 1989; Moschovakis, 1993; Moschovakis, 1997). The formal languages of recursion FLR are untyped systems. The typed version of this new approach to algorithmic, acyclic computations was introduced, for the first time in (Moschovakis, 2006), by designating it with ${\mathrm{L}}_{ar}^{\lambda }$, and demonstrating it by its applications to computational semantics of natural language. For more recent developments of the language and theory of acyclic algorithms ${\mathrm{L}}_{ar}^{\lambda }$, see, e.g., (Loukanova, 2019b; Loukanova, 2019c; Loukanova, 2020b).

The class ${\mathrm{L}}_r^{\lambda }$, of the typed formal languages and theories of full recursion, is an extension of (Gallin, 1975) logic TY2, and thus, of Montague Intensional Logic (IL), (Thomason, 1974). In this paper, we extend the formal language and reduction calculus of ${\mathrm{L}}_{ar}^{\lambda }$ and ${\mathrm{L}}_r^{\lambda }$, by incorporating restrictions on terms designating objects and algorithmic computations, which are required to satisfy the corresponding restrictions.

Two standard, distinctive approaches for representing definite descriptions by logic expressions were introduced by (Russell, 1905) and (Strawson, 1950). These two different interpretations were reconsolidated by using Situation Theory to represent each of them, see (Loukanova, 2001), by using situated, restricted parameters.

At first, we extend the type-theory of acyclic recursion ${\mathrm{L}}_{ar}^{\lambda }$, by adding a restrictor operator and corresponding restricted ${\mathrm{L}}_{ar}^{\lambda }$-terms, their denotational semantics, and reduction rules.

We demonstrate the application of the extended ${\mathrm{L}}_{ar}^{\lambda }$, by representing the denotational and algorithmic semantics of various kinds of definite descriptors, by rendering them into restricted ${\mathrm{L}}_{ar}^{\lambda }$-terms.

The definite descriptors may have interpretations that can be:

(1)Uniqueness conditions over objects, similar to (Ludlow, 2021), while expressed in type-theory ${\mathrm{L}}_{ar}^{\lambda }$

(2)Restricted references to objects, the restricted values of which are computed in context

(3)In either case, the type-theory ${\mathrm{L}}_{ar}^{\lambda }$ allows the values of the definite descriptors to be erroneous, by flagging them with designated values for errors

The introduction of restricted memory (i.e., recursion) variables and restricted ${\mathrm{L}}_{ar}^{\lambda }$-terms, introduced in this paper, is a new, algorithmic approach, which pertains to syntax-semantics of programming languages and other specification languages widely used in Computer Science and Artificial Intelligence (AI).

The reduction calculi of ${\mathrm{L}}_{ar}^{\lambda }$ reduces every ${\mathrm{L}}_{ar}^{\lambda }$-term to its canonical form, which provides a mathematical foundation of the work of compilers for reducing recursive programs to iterative ones. The type-theory ${\mathrm{L}}_{ar}^{\lambda }$ has a special importance to computational syntax-semantics of human language, i.e., natural language

Restricted variables designate memory slots for storing information constrained to satisfy propositional restrictions. The definite descriptor provides restrictions for imposing properties over data and in algorithms with restricted parameters. The algorithmic restrictor is specifically important for computational semantics of formal languages, e.g., in programming, specification languages in data and Artificial Intelligence (AI), and computational syntax-semantics of natural language. In particular, we present alternative possibilities for algorithmic semantics of singular, nominal expressions. For example, a Noun Phrase (NP), which is a definite description, such as “the cube”, can designate an object in a semantic domain, via identifying it as the unique object satisfying the property denoted by the description “cube”. Definite descriptors are abundant in the languages of mathematics, as specialised, subject delimited fragments of human language, which can be intermixed with mathematical expressions, e.g., “the natural number n, such that n + 1 = 2”.

This paper is part of the author’s work on the development of type-theory of algorithms by targeting versatile applications, especially in advanced technology with Natural Language Processing (NLP) in AI. For instance, a sequence of papers (Loukanova, 2011a; Loukanova, 2011b; Loukanova, 2011c; Loukanova, 2012b; Loukanova, 2012a; Loukanova, 2013c; Loukanova, 2013b; Loukanova, 2013a) use ${\mathrm{L}}_{ar}^{\lambda }$ to represent fundamental semantic notions in human language. The research presented in (Loukanova, 2016) is on the applications of ${\mathrm{L}}_{ar}^{\lambda }$ in the important topic of quantifier scope ambiguities, while (Loukanova, 2020b) is on formalisation of binding arguments of recursive properties, represented by functions, across mutual recursion assignments in recursion terms and modeling neural receptors.

Figure 1 depicts two approaches for algorithmic semantics of natural language (NL) used in the author’s work. By (1a), the computational grammar of NL delivers syntactic analyses of NL expressions. Afterwards, the syntactic analyses are used to render them into terms of ${\mathrm{L}}_{ar}^{\lambda }$, including the extended ${\mathrm{L}}_{rar}^{\lambda }$ introduced in this paper, to represent their algorithmic semantics. This approach is useful when algorithmic semantics of NL is the focus without providing syntactic analyses (in details), e.g., as in this paper. By (1b), the computational grammar of NL provides syntax-semantics analyses of NL, in a compositional mode (Loukanova, 2019a). Figure 2 gives the general scheme of the internal to ${\mathrm{L}}_{rar}^{\lambda }$ syntax-semantics relation between the syntax of the terms of ${\mathrm{L}}_{rar}^{\lambda }$ (${\mathrm{L}}_{ar}^{\lambda }$, ${\mathrm{L}}_r^{\lambda }$) and their algorithmic and denotational semantics.

$$\begin{array}{rl}& \underset{\text{Computational Grammar}}{\underbrace{\text{Computational Syntax of NL}}}\stackrel{\text{render}}{⟶}{\mathrm{L}}_{ar}^{\lambda }/{\mathrm{L}}_{\text{rar}}^{\lambda }\end{array} (1a)$$

$$\begin{array}{rl}& \underset{\text{Computational Grammar: Including Syntax-Semantics Interface}}{\underbrace{\text{Computational Syntax of NL}\stackrel{\text{render}}{⟷}{\mathrm{L}}_{ar}^{\lambda }/{\mathrm{L}}_{\text{rar}}^{\lambda }}}\end{array} (1b)$$

Recent work (Loukanova, 2019b; Loukanova, 2019c) extends the reduction calculus of type-theory of algorithms in useful ways, by targeting practical applications in advanced technologies, in line with the topic of this paper. A fundamental rule and conversion, η-conversion, of classic λ-calculi, was investigated for ${\mathrm{L}}_{ar}^{\lambda }$ (Loukanova, 2020a), by providing a version that grasps recursion assignments in canonical forms of ${\mathrm{L}}_{ar}^{\lambda }$ terms. A broader work (Loukanova, to appear) presents an algorithmic η-rule and η-reduction in ${\mathrm{L}}_{ar}^{\lambda }$.

To the best of the author’s knowledge, a precise, mathematical representation of the semantic notion of restricted parameters, as per se semantic objects, in type-theoretic, situated models was introduced by (Loukanova, 1991). The mathematical, semantic models introduced in that work are mathematical structures that include situated, dependent types defined hierarchically, by primitive types and recursion on situated propositions. The mathematical structures are based on relations, without coding them by one-argument functions, i.e., without currying encoding. At a semantic level, the restricted, typed objects of Situation Theory, were used to model both Russell and Strawson definite descriptors (Loukanova, 2001). In contrast to that work on Situation Theory, in this paper, we introduce syntactic counterparts of the semantic objects that are restricted parameters — restricted, memory (recursion) variables — as a special case of new, restricted ${\mathrm{L}}_{ar}^{\lambda }$-terms.

The generalised restrictor operator in Def. 2, (6a)–(6e), was introduced with a focus on algorithmic semantics, by extending the type-theory of algorithms ${\mathrm{L}}_{ar}^{\lambda }$ (Loukanova, 2021). The current paper presents this restrictor operator, by the syntax and semantics of type-theory of parametric algorithms, via covering syntax-semantics interrelations in ${\mathrm{L}}_{ar}^{\lambda }$ and ${\mathrm{L}}_r^{\lambda }$. In this extended paper, we emphasise the significance of the theoretical features of ${\mathrm{L}}_{ar}^{\lambda }$, which we have been developing by targeting advanced applications with new intelligent technologies, primarily through distributed computing in AI.

In Sect. 2, we introduce the formal syntax of the type-theory of algorithms with acyclic recursion and restrictor, ${\mathrm{L}}_{ar}^{\lambda }$ and ${\mathrm{L}}_{rar}^{\lambda }$, by pointing to the corresponding versions with full recursion, ${\mathrm{L}}_r^{\lambda }$ and ${\mathrm{L}}_{rr}^{\lambda }$. This new restrictor operator, for propositional restrictions, is at the object level of the formal language. In Sect. 3, we add the definition of the denotational semantics of ${\mathrm{L}}_{ar}^{\lambda }$, by including the denotation of the restrictor terms of the extended ${\mathrm{L}}_{rar}^{\lambda }$. Section 4 provides the full definition of the canonical forms of the terms of the extended type-theory ${\mathrm{L}}_{rar}^{\lambda }$. This definition has distinctive significance because the canonical forms of the proper terms determine the algorithmic semantics of the type-theory of parametric algorithms, in their respective versions, ${\mathrm{L}}_{ar}^{\lambda }$, ${\mathrm{L}}_{rar}^{\lambda }$, ${\mathrm{L}}_r^{\lambda }$, and ${\mathrm{L}}_{rr}^{\lambda }$. Section 5 introduces the most significant ingredient of the type-theory of algorithms, the reduction calculus, by covering terms with restrictor operator. The calculus is equipped with a set of reduction rules that define the system of reducing each term to its canonical form. In Sect. 6, we introduce the notion of generalised variables, as restricted memory slots, by using the restrictor operator. Then we investigate their major role in the theory of algorithms, as specialised memory slots for storing information that is computed algorithmically and restricted by conditions, also computed algorithmically. We demonstrate their reduction to basic memory variables which are irreducible terms. In Sect. 7, we present the significant role of algorithmic semantics in the type-theories of acyclic and full recursion, ${\mathrm{L}}_{rar}^{\lambda }$ and ${\mathrm{L}}_{rr}^{\lambda }$, with respect to their denotational semantics. The restrictor operator in the formal languages ${\mathrm{L}}_{ar}^{\lambda }$, ${\mathrm{L}}_{rar}^{\lambda }$, ${\mathrm{L}}_r^{\lambda }$, and ${\mathrm{L}}_{rr}^{\lambda }$ have algorithmic meanings, which is demonstrated in Sect. 8.

Definite descriptors play an important role in the many formal languages of logic, in many different applications in computer science, in computational grammars of natural languages, in Natural Language Processing (NLP), by corresponding reflections to AI. In Sect. 9, we provide possibilities for the application of restricted algorithms to represent definite descriptors, which are abundant in data of various forms, including in domain specific areas. For clarity, we exemplify them with expressions from human language, i.e., natural language. Sect. 9, covers various options for algorithmic semantics of descriptors by ${\mathrm{L}}_{rar}^{\lambda }$. In Sect. 10, we summarise the significance of the restrictor operator, some of the existing, forthcoming, and future work.

2. Terms for Algorithms with Acyclic Recursion and Restrictor

Definition 1 (Gallin Types). See (Gallin, 1975) logic TY₂:

$$\tau :\equiv \mathrm{e}|\mathrm{t}|\mathrm{s}\mid ({\tau }_1\to {\tau }_2) (Types)$$

We shall designate the type of the state dependent objects of type (s → τ) by (2), see Sect. 3. The semantic objects in the domain 𝕋(_s→τ) are called Carnap’s Intensions:

$$\tilde{\mathrm{\tau }}\equiv (\mathrm{s}\to \mathrm{\tau }),\text{for }\mathrm{\tau }\in \text{Types} (2)$$

The set of the constants Consts (also, shortly denoted by K) are given by denumerable (finite) sets of typed constants:

$${\text{Consts}}_{\mathrm{\tau }}=\{{\mathrm{c}}_0^{\mathrm{\tau }},\dots ,{\mathrm{c}}_{\mathrm{k}}^{\mathrm{\tau }}\}(\mathrm{k}\ge 0)\text{for all }\mathrm{\tau }\in \text{Types, }{\mathrm{K}}_{\mathrm{\tau }},\text{Consts}={\cup }_{\mathrm{\tau }}{\text{Consts}}_{\mathrm{\tau }} (3)$$

${\mathrm{L}}_{ar}^{\lambda }$ has Pure Variables, given by denumerable sets of typed pure variables:

$${\text{PureV}}_{\tau }=\{{\mathrm{v}}_0^{\tau },\dots \}\text{for all }\tau \in \text{Types, }{K}_{\tau },\text{PureV}={\cup }_{\tau }{\text{PureV}}_{\tau } (4)$$

${\mathrm{L}}_{ar}^{\lambda }$ has Recursion (Memory) Variables given by denumerable sets of typed recursion (memory) variables: $\mathrm{RecV}={\cup }_{\mathrm{\tau }}{\mathrm{RecV}}_{\mathrm{\tau }},\mathrm{for}{\mathrm{RecV}}_{\mathrm{\tau }}=\{{\mathrm{r}}_0^{\mathrm{\tau }},\dots \}$. The vocabulary is without intersections: Consts ≠ RecV ≠ PureV, and the set of all variables is Vars = PureV ∪ RecV.

$${\text{RecV}}_{\tau }=\{{\mathrm{r}}_0^{\tau },\dots \}\text{for all }\tau \in \text{Types, }{K}_{\tau },\text{RecV}={\cup }_{\tau }{\text{RecV}}_{\tau } (5)$$

In this section, we extend the formal language of ${\mathrm{L}}_{ar}^{\lambda }$ by adding a constant for a restrictor operator (such that), for the formation of new terms, with restrictions. The extended formal language of ${\mathrm{L}}_{rar}^{\lambda }$ has the same set of types, constants and variables, as ${\mathrm{L}}_{ar}^{\lambda }$. Sometimes, when it is clear from the context, we shall write ${\mathrm{L}}_{ar}^{\lambda }$ instead of ${\mathrm{L}}_{rar}^{\lambda }$, by assuming that ${\mathrm{L}}_{ar}^{\lambda }$ = ${\mathrm{L}}_{rar}^{\lambda }$. The Terms are defined by adding one more rule (6e), for the restrictor operator (a special operator constant) such that. Then, we extend the definition of the canonical forms and reduction calculus of ${\mathrm{L}}_{ar}^{\lambda }$.

Here, we present the recursive rules of the definition of the set of ${\mathrm{L}}_{rar}^{\lambda }$ -terms by Def. 2, (6a)–(6e), using an extended, typed Backus-Naur Form (TBNF) style, with the assumed types given as superscripts.

We use the typical notations for type assignments, A : τ, and A^τ, to express that A is a term of type τ.

Definition 2 (Terms). The set ${\mathrm{Terms}}_{{\mathrm{L}}_{rar}^{\lambda }}$ of the terms consists of the expressions defined by the following rules:

$$A:\equiv {\mathrm{c}}^{\tau }:\tau \mid x^{\tau }:\tau {\text{(for c}}^{\tau }\in {\text{Consts}}_{\tau },x^{\tau }\in {\mathrm{PureV}}_{\tau }\cup {\mathrm{RecV}}_{\tau }\text{)} (6a)$$

$$\mid B^{(\sigma \to \tau )}\left(C^{\sigma }\right):\tau \text{(}\mathit{\text{application term}}\text{)} (6b)$$

$$\mid \lambda \left(v^{\sigma }\right)\left(B^{\tau }\right):(\sigma \to \tau )(\lambda -\mathit{\text{term}}\text{)} (6c)$$

$$\mid [A_0^{{\sigma }_0} \text{where }\{p_1^{{\sigma }_1}:=A_1^{{\sigma }_1},\dots ,p_n^{{\sigma }_n}:=A_n^{{\sigma }_n}\}]:{\sigma }_0\text{(}\mathit{\text{recursion term}}\text{)} (6d)$$

$$\mid \left(A_0^{{\sigma }_0}\text{such that }\{C_1^{{\tau }_1},\dots ,C_m^{{\tau }_m}\}\right):{\sigma }_0^{\mathrm{\prime }}\text{(}\mathit{\text{restrictor / restriction term}}\text{)} (6e)$$

given that:

(1)c ∈ Consts, x ∈ PureV ∪ RecV, v^σ ∈ PureV_σ

(2)B, C ∈ Terms of the respective types

(3)in (6d), for n ≥ 0, i = 0, …, n, σ_i ∈ Types, $A_{\mathit{i}}\in {\mathrm{Terms}}_{{\sigma }_{\mathit{i}}}$;

for i = 1, …, n, $pi\in {\mathrm{RecV}}_{{\sigma }_{\mathit{i}}}$, are pairwise different recursion variables, of the same types as of the terms, correspondingly assigned to them

(4)the sequence of assignments in (6d) satisfies the AC, (8a)–(8c)

(5)in (6e), for j = 1, …, m (m ≥ 0),

(a)$C_{\mathit{j}}^{{\mathit{\tau }}_{\mathit{j}}}$ ∈ Terms, for τ_j ∈ Types

(b)τ_j ∈ Types is either τ_j ≡ t, i.e., the type t of state-independent truth values, or ${\tau }_{\mathit{j}}\mathit{ }\mathit{\equiv }\mathit{ }\stackrel{\mathit{~}}{\mathit{t}}\mathit{ }\mathit{\equiv }\mathit{ }(s\mathit{ }\mathit{\to }\mathit{ }t)$, i.e., the type $\stackrel{\mathit{~}}{\mathit{t}}$ of truth values that may depend on states

and the type ${\sigma }_0^{\mathrm{\prime }}$ of the restrictor (restriction) term $A^{{\sigma }_0^{\mathrm{\prime }}}$ in (6e) is:

$${\sigma }_0^{\mathrm{\prime }}\equiv \{\begin{array}{ll}{\sigma }_0,& \text{ if }{\tau }_i\equiv \mathrm{t},\text{ for all }i\in \{1,\dots ,n\}\\ {\sigma }_0\equiv (\mathrm{s}\to \sigma ),& \text{ if }{\tau }_i\equiv \tilde{\mathrm{t}}\text{, for some }i\in \{1,\dots ,n\},\text{ and }\\ & \text{ for some }\sigma \in \text{ Types, }{\sigma }_0\equiv (\mathrm{s}\to \sigma )\\ \widetilde{{\sigma }_0}\equiv (\mathrm{s}\to {\sigma }_0),& \text{ if }{\tau }_i\equiv \tilde{\mathrm{t}}\text{, for some }i\in \{1,\dots ,n\},\text{ and }\\ & \text{ there is no }\sigma ,\text{ s.th. }{\sigma }_0\equiv (\mathrm{s}\to \sigma )\end{array} (7a,\; 7b,\; 7c)$$

The type ${\sigma }_0^{\mathrm{\prime }}$ of the restrictor (restriction) term $A^{{\sigma }_0^{\mathrm{\prime }}}$ in (6e) is that of $A_0^{{\sigma }_0}$, in the cases (7a)–(7b). In the case (7c), the type σ₀ of A₀, does not depend directly on states because there is no σ, such that σ₀ ≡ (s → σ), while at least one of the restrictions C_i is of state-dependent type, ${\tau }_{\mathit{i}}\mathit{ }\mathit{\equiv }\mathit{ }\stackrel{\mathit{~}}{\mathit{t}}$, for some i ∈ { 1, …, n }. The state-dependence of the entire restriction term A is reflected by lifting the type σ₀ of A₀ to its state dependent version, in the type ${\sigma }_0^{\mathrm{\prime }}$ of A : ${\sigma }_0^{\mathrm{\prime }}$.

For each τ ∈ Types, Termsτ is the set of the terms of type τ.

We call the terms A of the form (6d) recursion terms, and the terms of the form (6e) restriction or restrictor terms (sometimes, also, restricted terms).

Acyclicity Constraint (AC) For any σ_i ∈ Types, $A_{\mathit{i}}\mathit{ }\in \mathit{ }{\mathrm{Terms}}_{{\sigma }_{\mathit{i}}}$, and pairwise different recursion variables, $p_{\mathit{i}}\mathit{ }\in {\mathrm{RecV}}_{{\sigma }_{\mathit{i}}}$, for i = 1, …, n:

$$\{p_1:=A_1,\dots ,p_n:=A_n\}(n\ge 0)\mathrm{is}\mathrm{an}\mathrm{acyclic}\mathrm{sequence}\mathrm{iff}\mathrm{there}\mathrm{is}\mathrm{a}\mathrm{function}\mathrm{rank},\mathrm{such}\mathrm{that}: (8a)$$

$$\mathrm{rank}:\{p_1,\dots ,p_n\}\to \mathrm{\mathbb{N}} (8b)$$

$$\mathrm{for}\mathrm{all}i,j\in \{1,\dots ,n\},p_j\in \mathrm{FreeV}\left(A_i\right)⟹\mathrm{rank}\left(p_j\right)<\mathrm{rank}\left(p_i\right) (8c)$$

We call the sequence (8a) acyclic system of assignments.

The formal language of ${\mathrm{L}}_{rar}^{\lambda }$, without the AC, (8a)–(8c), provides the version of the type-theory ${\mathrm{L}}_{rr}^{\lambda }$ of full recursion and restrictors.

Bound and Free Variables The sets FreeV(A) and BoundV(A), respectively of the free and bound variables of the ${\mathrm{L}}_{rar}^{\lambda }$-terms A, are defined by structural recursion on A, in the usual way, as part of Def. 2, (6a)–(6e), for each clause, with the exception of the recursion and restriction terms, i.e.:

(BFV1) For any recursion term A of the form (6d), i.e., A ≡ [A₀ where { p₁ := A₁, …, p_n := An }], all the free occurrences of p₁, …, p_n, in each of the terms A₀, …, An, are bound occurrences in A. All other free (bound) occurrences of variables in A₀, …, An are also free (bound) in A, and:

$$\begin{array}{rl}\mathrm{BoundV}\left(A\right)& =\mathrm{BoundV}(A_0 \text{where }\{p_1:=A_1,\dots ,p_n:=A_n\})\\ & =\underset{i=0}{\overset{n}{\cup }}\left(\mathrm{BoundV}\left(A_i\right)\right)\cup \{p_1,\dots ,p_n\}\end{array} (9a)$$

$$\begin{array}{rl}\mathrm{FreeV}\left(A\right)& =\mathrm{FreeV}\left(A_0\text{where }\{p_1:=A_1,\dots ,p_n:=A_n\}\right)\\ & =\underset{i=0}{\overset{n}{\cup }}\left(\mathrm{FreeV}\left(A_i\right)\right)-\{p_1,\dots ,p_n\}\end{array} (9b)$$

(BFV2) For any restriction term A of the form (6e), i.e., $A\equiv (A_{\mathit{0}}^{\mathit{\sigma }\mathit{0}}\mathit{ }\mathrm{such}\mathrm{that}\{C_{\mathit{1}}^{{\mathit{\tau }}_{\mathit{1}}},\dots ,C_{\mathit{m}}^{{\mathit{\tau }}_{\mathit{m}}}\left\}\right)$, all the free (bound) occurrences of variables in A₀, C₁, …, C_m are also free (bound) in A, and:

$$\begin{array}{rl}\text{BoundV}\left(A\right)& =\mathrm{BoundV}\left(A_0\right)\cup \underset{i=1}{\overset{m}{\cup }}\left(\mathrm{BoundV}\left(C_i\right)\right)\end{array} (10a)$$

$$\begin{array}{rl}\mathrm{FreeV}\left(A\right)& =\mathrm{FreeV}\left(A_0\right)\cup \underset{i=1}{\overset{m}{\cup }}\left(\mathrm{FreeV}\left(C_i\right)\right)\end{array} (10b)$$

All occurrences of constants in any ${\mathrm{L}}_{rar}^{\lambda }$-term are free.

Notation 1. Often, abbreviations for sequences are useful, e.g., for i = 1, …, n, j = 1, …, m (n, m ≥ 0), $p_{\mathit{i}}\mathit{ }\in \mathit{ }{\mathrm{RecV}}_{{\tau }_{\mathit{i}}}\mathit{,}\mathit{ }{A}_{\mathit{i}}\mathit{ }\in \mathit{ }{\mathrm{Terms}}_{{\tau }_{\mathit{i}}}$, v_j, ui ∈ PureV, H ∈ Terms, of suitable types:

$$\begin{array}{rl}\overrightarrow{p}:=\overrightarrow{A}& \equiv p_1:=A_1,\dots ,p_n:=A_n(n\ge 0)\end{array} (11a)$$

$$\begin{array}{rl}H\left(\overrightarrow{u}\right)& \equiv [\dots H\left(u_1\right)\dots ]\left(u_n\right)(n\ge 0)\end{array} (11b)$$

$$\begin{array}{rl}\lambda \left(\overrightarrow{v}\right)\left(H\right(\overrightarrow{u}\left)\right)& \equiv \lambda \left(v_1\right)(\dots \lambda \left(v_m\right)\left([\dots H\left(u_1\right)\dots ]\left(u_n\right)\right)\dots )\\ & \equiv \lambda \left(v_1\right)\dots \left(v_m\right)(H\left(u_1\right)\dots \left(u_n\right))\\ & \equiv \lambda (v_1,\dots ,v_m)\left(H(u_1,\dots ,u_n)\right)(n,m\ge 0)\end{array}\begin{array}{}\end{array} (11c)$$

3. Denotational Semantics of ${\mathrm{L}}_{ar}^{\lambda }$ and ${\mathrm{L}}_{rar}^{\lambda }$

A standard semantic structure is a tuple 𝔄(Consts) = $<\mathbb{T},I>$ that satisfies the following conditions:

•$\mathbb{T}\mathit{=}\left\{{\mathbb{T}}_{\mathrm{\sigma }}\right|\sigma \in Types\}$ is a frame, i.e., a set of sets of typed objects, such that:

–$\{0,1,er\}\subseteq {\mathbb{T}}_{\mathrm{t}}\subseteq {\mathbb{T}}_{\mathrm{e}}(e{r}_{\mathit{t}}\equiv e{r}_{\mathrm{e}}\equiv \mathrm{er}\equiv error)$

–${\mathbb{T}}_{\mathrm{s}}\ne \varnothing$ (the set of the states)

–${\mathbb{T}}_{(\tau 1\to \tau 2)}=({\mathbb{T}}_{\tau 1}\to {\mathbb{T}}_{\tau 2})=\left\{f\right|f:{\mathbb{T}}_{\tau 1}\to {\mathbb{T}}_{\tau 2}\}$ (standard frame)

–Optionally, ${\mathrm{L}}_{ar}^{\lambda }$ may designate different objects as the erroneous values, which are typed: er_(τ1→τ2) = h, is a function, such that, for every $c\in {\mathbb{T}}_{\tau 1},h\left(c\right)=e{r}_{\tau 2}$, i.e., designated typed erroneous objects as values

•I : Consts → ∪ $\mathbb{T}$ is the interpretation function, respecting the types: for every $c\in {\mathrm{Consts}}_{\mathrm{\sigma }},I\left(c\right)\in {\mathbb{T}}_{\sigma }$ there is some c ∈ ${\mathbb{T}}_{\tau }$, such that I(c) = c

•𝔄 has the set G of all variable valuations G, respecting the types:

$$G=\{g\mid g:\text{PureV}\cup \mathrm{RecV}\to \cup \mathbb{T},\text{and for every}x:\sigma ,g(x)\in {\mathbb{T}}_{\sigma }\}\begin{array}{}\end{array} (12)$$

Definition 3 (Denotation Function). There is a unique denotation function den^𝔄:

$${\mathrm{ten}}^{\mathfrak{A}}:\text{Terms}\to \{f\mid f:G\to \cup \mathbb{T}\} (13)$$

defined by structural induction (i.e., by recursion) on the terms, by (D1)–(D5). For any given, fixed semantic structure 𝔄, we write den ≡ den^𝔄.

(D1)(a) den(x)(g) = g(x), for all x ∈ PureV ∪ RecV

(b) den(c)(g) = I (c). for all c ∈ Consts

(D2)den(A(B))(g) = den(A)(g)(den(B)(g))

(D3)den(λx(B))(g) (t) = den(B)(g{ x := t }), for every $x\in {\mathrm{Vars}}_{\mathrm{\tau }},t\in {\mathbb{T}}_{\mathrm{\tau }}$

(D4)den(A₀ where {p₁ := A₁, …,p_n := An })(g) =

$\mathrm{den}\left(A_0\right)\left(g\right\{p_{\mathit{1}}:={\overline{p}}_1,\dots ,p_{\mathit{n}}:={\overline{p}}_n\left\}\right)$

where the values ${\overline{p}}_i\in {\mathbb{T}}_{{\tau }_i}$ are defined by recursion on rank(p_i):

$$\overline{p_i}=\mathrm{den}\left(A_i\right)\left(g\{p_{k_1}:={\overline{p}}_{k_1},\dots ,p_{k_m}:={\overline{p}}_{k_m}\}\right) (14)$$

given that pk₁, …, pk_m are all of the recursion variables p_j ∈ {p₁, …, p_n }, such that rank(p_j) < rank(p_i) Informally, den(A₁)(g), …, den(A_n)(g) are computed recursively and stored in p₁, …, p_n, respectively; the denotation den(A₀)(g) may depend on values stored in p₁, …, p_n.

(D5)The stipulation of the denotation of the restricted terms A of the form (6e) is in two cases, with respect to possible state dependent types of the components of A:

$$A\equiv \left(A_0^{{\sigma }_0}\text{such that }\{C_1^{{\tau }_1},\dots ,C_m^{{\tau }_m}\}\right)\equiv (A_0^{{\sigma }_0} \text{s.t.} \{\overrightarrow{C}\left\}\right) (15)$$

Case 1: for all i ∈ { 1, …, n }, C_i : t
For every g ∈ G:

$$\mathrm{den}(A_0^{{\sigma }_0} \text{s.t.} \{\overrightarrow{C}\left\}\right)\left(g\right)=\{\begin{array}{ll}\mathrm{den}\left(A_0\right)\left(g\right),& \text{if, for all }i\in \{1,\dots ,n\},\\ & \mathrm{den}\left(C_i\right)\left(g\right)=1\\ e{r}_{{\sigma }_0}& \text{if, for some }i\in \{1,\dots ,n\},\\ & \mathrm{den}\left(C_i\right)\left(g\right)=0 \text{or}\\ & \mathrm{den}\left(C_i\right)\left(g\right)=er\end{array} (16)$$

Case 2: for some i ∈ { 1, …, n }, Ci : $\tilde{\mathrm{t}}$ (state dependent proposition)
For every g ∈ G, and every state s ∈ $s\in {\mathbb{T}}_s$:

$$\begin{array}{l}\text{den}\left(A_0^{{\sigma }_{\text{O}}}\text{s}\text{.t}\text{.}\left\{\overrightarrow{C}\right\}\right)(g)(s)\\ =\{\begin{array}{ll}\text{den(}{A}_{\text{0}}\text{)(}g\text{)(}s\text{),}\hfill & \begin{array}{ll}\text{if}\hfill & den\left(C_i\right)(g)=1\text{, for all}i\text{s}\text{.th}\text{.}{C}_i:\text{t, and}\hfill \\ \hfill & \begin{array}{l}den\left(C_i\right)(g)\left(s\right)=1\text{, for all}i\text{s}\text{.th}\text{.}{C}_i:\tilde{\text{t}}\text{, and}\\ {\sigma }_0\equiv (\text{s}\to \sigma )\end{array}\hfill \end{array}\hfill \\ \text{den(}{A}_{\text{0}}\text{)(g),}\hfill & \begin{array}{ll}\text{if}\hfill & den\left(C_i\right)(g)=1\text{, for all}i\text{s}\text{.th}\text{.}{C}_i:\text{t, and}\hfill \\ \hfill & \begin{array}{l}den\left(C_i\right)(g)\left(s\right)=1\text{, for all}i\text{s}\text{.th}\text{.}{C}_i:\tilde{\text{t}}\text{, and}\\ \text{there is no }\sigma \in \text{Types,}\text{such}\text{that}{\sigma }_0\equiv (\text{s}\to \sigma )\end{array}\hfill \end{array}\hfill \\ e{r}_{{{\sigma }^{\prime }}_0},\hfill & \text{otherwise,}\text{for}{{\sigma }^{\prime }}_0\equiv \{\begin{array}{ll}\sigma ,\hfill & \text{such}\text{that}{\sigma }_0\equiv \left(\text{s}\to \sigma \right)\hfill \\ {\sigma }_0,\hfill & \text{if}\text{ther}\text{is}\text{no}\sigma \in \text{Types,}\text{such}\text{that}\hfill \\ \hfill & {\sigma }_0\equiv \left(\text{s}\to \sigma \right)\hfill \end{array}\hfill \end{array}\end{array} (17)$$

Informally, the denotation of a term A of the form (6e) is the denotation of A₀, in case all C_i are true, otherwise it is error, i.e., it is error in the following cases:

•the denotation of at least one of the terms A₀, C_i (i = 1, …, m) is error, or

•the denotation of at least one of the terms C_i is false (i = 1, …, m)

Immediate terms do not carry algorithmic sense; their denotations are obtained by the variable valuations. For details on the immediate terms, see (Moschovakis, 2006) and (Loukanova, 2019b). Here, we provide their definition because they play an essential role in the computational notions of ${\mathrm{L}}_{ar}^{\lambda }$ and ${\mathrm{L}}_{rar}^{\lambda }$, and for self-containment of the paper.

Definition 4 (Immediate and Proper Terms). The set of the immediate terms is defined recursively, e.g., by the style of typed BNF notation:

$${\mathrm{ImT}}^{\tau }:\equiv X^{\tau }\mid \underset{\text{(immediate applicative terms)}}{\underbrace{Y^{({\tau }_1\to \cdots \to ({\tau }_m\to \tau ))}\left(v_1^{{\tau }_1}\right)\dots \left(v_m^{{\tau }_m}\right)}} \left(\mathrm{ImAp}\right) (18a)$$

$$\begin{array}{l}{\mathrm{ImT}}^{({\sigma }_1\to \dots \to ({\sigma }_n\to \tau ))}:\equiv \\ \underset{\text{(immediate }\lambda \text{-terms)}}{\underbrace{\lambda \left(u_1^{{\sigma }_1}\right)\dots \lambda \left(u_n^{{\sigma }_n}\right)[Y^{({\tau }_1\to \cdots \to ({\tau }_m\to \tau ))}\left(v_1^{{\tau }_1}\right)\dots \left(v_m^{{\tau }_m}\right)]}} \left(\mathrm{Im\lambda }\right)\end{array} (18b)$$

for n ≥ 1, m ≥ 0; u_i, v_j ∈ PureV, for i = 1, …, n, j = 1, …, m; X ∈ PureV, Y ∈ RecV

A term A is proper if it is not immediate, i.e., the set PrT of the proper terms of ${\mathrm{L}}_{rar}^{\lambda }$ consists of all terms that are not in ImT:

$$\mathrm{PrT}=(\mathrm{Terms}-\mathrm{ImT})\begin{array}{}\\ \\ \end{array} (19)$$

4. Canonical Forms

For every term A ∈ Terms, there is a term cf (A), a canonical form of A, defined by structural recursion on the term A, according to Definition 5. We extend the corresponding definition given in (Moschovakis, 2006), by adding a clause for cf (A), for terms A of the form (6e).

Definition 5 (Canonical Forms of Terms). In each of the following clause, we assume that the bound recursion variables are distinct for the distinct terms, and from the free recursion variables, because the bound variables can be renamed, by the congruence relation, see Def. 6.

(CF1)For every c ∈ Consts_τ, cf (c) :≡ c ≡ c where { }

For every x ∈ PureV ∪ RecV, cf (x) :≡ x ≡ x where { }

(CF2)Assume that A ∈ Terms, and

$$\begin{array}{rl}\mathrm{cf}\left(A\right)& \equiv A_0 \text{where }\{p_1:=A_1,\dots ,p_n:=A_n\}(n\ge 0)\end{array} (20a)$$

$$\equiv A_0 \text{where }\{\overrightarrow{p}:=\overrightarrow{A}\} (20b)$$

(CF2a) If X is an immediate term, then

$$\mathrm{cf}\left(A\right(X\left)\right):\equiv A_0\left(X\right)\text{where }\{\overrightarrow{p}:=\overrightarrow{A}\}\begin{array}{}\\ \end{array} (21)$$

(CF2b) If B is a proper term and

$$\begin{array}{rl}\mathrm{cf}\left(B\right)& \equiv B_0 \text{where }\{q_1:=B_1,\dots ,q_m:=B_m\}(m\ge 0)\end{array} (22a)$$

$$\equiv B_0 \text{where }\{\overrightarrow{q}:=\overrightarrow{B}\} (22b)$$

then

$$\mathrm{cf}\left(A\right(B\left)\right):\equiv A_0\left(q_0\right) \text{where }\{\overrightarrow{p}:=\overrightarrow{A},q_0:=B_0,\overrightarrow{q}:=\overrightarrow{B}\}\begin{array}{}\\ \end{array} (23)$$

where q₀ ∈ RecV is a fresh recursion variable

(CF3) Assume that A ∈ Terms, and

$$\mathrm{cf}\left(A\right)\equiv A_0 \text{where }\{\overrightarrow{p}:=\overrightarrow{A}\} (24)$$

Then, for every u ∈ PureVτ, and fresh $p_1^{\mathrm{\prime }},\dots ,p_n^{\mathrm{\prime }}\in \mathrm{RecV}:$

$$\begin{array}{rl}\mathrm{cf}\left(\lambda \right(u\left)A\right):\equiv \lambda \left(u\right)A_0^{\mathrm{\prime }} \text{where }\{p_1^{\mathrm{\prime }}:& =\lambda \left(u\right)A_1^{\mathrm{\prime }},\dots ,\\ p_n^{\mathrm{\prime }}& :=\lambda \left(u\right)A_n^{\mathrm{\prime }}\}\end{array} (25)$$

where $A_i^{\mathrm{\text{'}}}$ is the result of the simultaneous replacement of all the free occurrences of p₁, …, p_n in A_i with $p_1^{\mathrm{\text{'}}}(u),\dots ,p_n^{\mathrm{\text{'}}}(u)$, respectively

(CF4) Assume that A ∈ Terms is such that

$$\mathrm{cf}\left(A\right)\equiv A_0 \text{where }\{\overrightarrow{p}:=\overrightarrow{A}\}\begin{array}{}\\ \end{array} (26)$$

and, for every i = 0, …, n,

$$\begin{array}{rl}\mathrm{cf}\left(A_i\right)& \equiv A_{i,0} \text{where }\{p_{i,1}:=A_{i,1},\dots ,p_{i,k_i}:=A_{i,k_i}\}\end{array} (27a)$$

$$\equiv A_{i,0} \text{where}\{\overrightarrow{p_i}:=\overrightarrow{A_i}\} (27b)$$

Then, for fresh p₁, …, p_n ∈ RecV:

$$\mathrm{cf}\left(A\right):\equiv A_{0,0} \text{where }\{\overrightarrow{p_0}:=\overrightarrow{A_0}, (28a)$$

$$\begin{array}{r}{p}_1:=A_{1,0},\overrightarrow{p_1}:=\overrightarrow{A_1},\\ ⋮\end{array} (28b)$$

$$p_n:=A_{n,0},\overrightarrow{p_n}:=\overrightarrow{A_n}\} (28c)$$

(CF5) Assume that j = 1, …, m (m ≥ 0), i = 1, …, k (k ≥ 0), and: