# Towards a Neural Lambda Calculus: Neurosymbolic AI Applied to the Foundations of Functional Programming
**Authors**: João M. Flach, Álvaro F. Moreira, Luís C. Lamb
> Institute of InformaticsFederal University of Rio Grande do SulPorto Alegre, RS, Braziljmflach@inf.ufrgs.br, alvaro.moreira@inf.ufrgs.br, luislamb@acm.org
Abstract
In recent decades, deep neural network-based models have become the dominant paradigm in machine learning. The use of artificial neural networks in symbolic learning has recently been considered increasingly relevant. To study the capabilities of neural networks in the symbolic AI domain, researchers have explored the ability of deep neural networks to learn mathematical operations, logic inference, and even the execution of computer programs. The latter is known to be too complex a task for neural networks. Therefore, the results were not always successful and often required the introduction of biased elements in the learning process, in addition to restricting the scope of possible programs to be executed. In this work, we will analyze the ability of neural networks to learn how to execute programs as a whole. To do so, we propose a different approach. Instead of using an imperative programming language with complex structures, we use the Lambda Calculus ( $\lambda$ -Calculus), a simple and Turing-complete mathematical formalism, which serves as the basis for modern functional programming languages and is at the heart of computability theory. We will introduce the use of integrated neural learning and lambda-calculi formalization. We explore that the execution of a program in $\lambda$ -Calculus is based on reductions, and we will show that it is enough to learn how to perform these reductions so that we can execute any program. This manuscript is an improvement of a previous one posted in arXiv.org by Flach and Lamb, with significant contributions by Professor A.F. Moreira.
Keywords: Machine Learning, Lambda Calculus, Neurosymbolic AI, Neural Networks, Transformer Model, Sequence-to-Sequence Models, Computational Models.
1 Introduction
In machine learning, there has been a long-standing debate about the best way to approach the task of learning from data [19]. Rule-based inference emphasizes the use of explicit logical rules to reason about the data and make decisions, inferences, and predictions [12]. The other perspective, statistical learning, involves using mathematical models to automatically extract patterns and relationships from data [28, 19].
Deep neural networks have been used successfully in applications such as speech recognition, machine translation, and handwriting recognition. Recently, advances in the field have resulted in the introduction of models that are changing the landscape and allowing us to tackle a wider range of problems, including symbolic ones, using neural networks. When neural networks are applied to symbolic problems, the result is a hybrid approach that combines the advantages of both rule-based (in which logic-based ones are prominent) and statistical approaches. This combination falls into the realm of neurosymbolic AI [8, 16]. This field combines the statistical nature of machine learning with the logical nature of reasoning in AI [8], and has recently attracted the attention of researchers from several subfields of AI and computer science [12, 3] as it can contribute to offering explainable machine learning approaches. This interest is sparked by the need to build more robust AI models [11], as initially advocated by Valiant and now a subject of increasing interest in AI research [34, 33, 23].
In this work, we intend to explore the capacity of machine learning models, specifically the Transformer [35], to learn rules to perform computations, a task traditionally seen as too complex for neural networks to handle.
The idea of training a machine learning model to perform computations is relatively new. Most works in this field restrict the class of programs that the model can take as input and consist of teaching the model to understand rules for the evaluation of mathematical expressions.
We, on the other hand, use the Lambda Calculus ( $\lambda$ -Calculus) as the underlying framework [2]. Introduced by Alonzo Church in the 1930s [7], it is a simple, elegant, and Turing-complete formal system based on function abstraction that captures the notion of function definition and function application. It is the base for modern functional programming languages, such as OCaml, Racket, Haskell, and others [24], and it has become one of the main computational models alongside Turing Machines [5].
In essence, the $\lambda$ -Calculus can be seen as a programming language whose programs, called $\lambda$ terms, can be subject to reductions that can be interpreted as computations performed within the formalism. Applying a single reduction to a term represents a one-step computation in the $\lambda$ -Calculus. On the other hand, a full computation involves successive single reductions of a term until a normal form is obtained (if it has one), i.e., a term that cannot be reduced any further.
In summary, our research question is: “Can a machine learning model learn to perform computations?”. To gradually enhance our understanding of the subject matter and enable us to provide an answer to our research question, we propose the following two hypotheses.
- H1: The Transformer model can learn to perform one-step computation on Lambda Calculus.
- H2: The Transformer model can learn to perform full computation on Lambda Calculus.
Considering that lambda terms do not have a fixed size, we use a sequence-to-sequence (seq2seq) model, which can take inputs and produce outputs of any length. Specifically, we use a model that has been widely used for several types of applications and has also been tested for symbolic tasks: the Transformer [35].
2 Related Work
In [36], seq2seq models are used to learn to evaluate short computer programs using an imperative language with the Python syntax. However, their domain is restricted to short programs that can use just some arithmetic operations, variable assignment, if-statements, and for loops (not nested).
Some other studies also have worked towards developing models that learn algorithms or learn to execute computer code, including [15, 14, 32]. However, the domain of these works is restricted to some arithmetical operations or sequence computations (copying, duplicating, sorting). Additional work concentrates on acquiring an understanding of program representation. For example, [22] builds generative models of "natural source code", i.e., code written by humans and meant to be understood by other humans, while [25] applies neural networks to determine if two programs are equivalent.
The Transformer model [35] brought several key advancements and improvements compared to the state-of-the-art seq2seq models prevalent at that time. This new model boasted improved parallelism, reduced sequential processing requirements, and the ability to handle longer sequences, among other things. These innovative features have contributed to the widespread adoption of the Transformer model in various Machine Learning applications.
In a study by [18], the Transformer model was applied to learn how to symbolically integrate functions, producing very promising results. The authors demonstrated that the model was capable of learning to perform integrals in a way that was both accurate and efficient, outperforming existing methods in many cases. This study highlights the versatility and potential of the Transformer model, making it a valuable tool for tackling a wide range of machine learning tasks, especially in areas that require symbolic reasoning and mathematical operations.
In addition, the Transformer model has enabled recent developments in chatbot technologies. An example of a chatbot that has emerged as a result of this development is the ChatGPT available at: https://openai.com/blog/chatgpt/, which is based on a state-of-the-art AI model, the GPT-3, from [4]. These chatbots can answer questions about various subjects [27] and perform basic symbolic reasoning. However, their symbolic reasoning capability is still limited, giving some incorrect answers to straightforward questions.
In the present work, we shift from the imperative paradigm that all other works have used, to the functional paradigm, which is the case for the $\lambda$ -Calculus. With this, we abstract the idea of learning to compute computer programs to learn to perform reductions in $\lambda$ terms.
With this approach, in the sequel we will show that to learn one-step computation, we obtained an accuracy of $88.89\%$ in completely random terms $\lambda$ and of $99.73\%$ in terms representing Boolean expressions. For the full computation task, we obtained an accuracy of $97.70\%$ for $\lambda$ terms that represent boolean expressions. Taking into account a string similarity metric, most of our predicted $\lambda$ terms were above $99\%$ similar to the correct ones.
With these results, we think that the change to the functional paradigm and the use of the Transformer model are two improvements that will be relevant in future research.
3 The Lambda Calculus: A Summary
In this section, we present an overview of the main aspects of the Lambda Calculus that will be used in the paper.
3.1 Syntax
We start by defining the syntax of lambda terms. In the following, $x$ denotes a member of an infinite and countable set of variables.
**Definition 1 (λ𝜆\lambdaitalic_λ-terms)**
*The set of $\lambda$ -terms is defined by the following abstract grammar:
$$
\begin{array}[]{lcl}M,N,\ldots::=&x~{}~{}|~{}~{}\lambda x.M~{}~{}|~{}~{}M~{}N%
\end{array}
$$*
Every variable is a $\lambda$ term; the term $\lambda x.M$ is a function with parameter $x$ and body $M$ ; the term $M\;N$ is the application of the term $M$ to the argument $N$ .
In a term $\lambda x.M$ , all the occurrences of variable $x$ inside $M$ are called bound occurrences.
3.2 Reductions
The main reduction of the formalism is a binary relation between terms called $\beta$ reduction, which is based on the substitution operation. A substitution takes a $\lambda$ term and substitutes a variable in it with another $\lambda$ term, similar to what is done in mathematics when a function is applied to an argument.
**Definition 2 (Redex)**
*A redex (reducible expression) is any subterm in the format
$$
(\lambda x.M)\;N
$$*
If a term has no redexes, the term is a normal form. Otherwise, the term is reducible. Now, the $\beta$ -reduction relation can be defined as:
**Definition 3 (One-Step)**
*$\beta$ -reduction ( $→_{\beta}$ ) is the smallest relation on lambda terms such that $\displaystyle\frac{\begin{array}[]{@{}c@{}}M→_{\beta}M^{\prime}\end{%
array}}{\begin{array}[]{@{}c@{}}M\;N→_{\beta}M^{\prime}\;N\end{array}}$ $\displaystyle\frac{\begin{array}[]{@{}c@{}}N→_{\beta}N^{\prime}\end{%
array}}{\begin{array}[]{@{}c@{}}M\;N→_{\beta}M\;N^{\prime}\end{array}}$ $\displaystyle\frac{\begin{array}[]{@{}c@{}}M→_{\beta}M^{\prime}\end{%
array}}{\begin{array}[]{@{}c@{}}\lambda x.M→_{\beta}\lambda x.M^{%
\prime}\end{array}}$ $\displaystyle\begin{array}[]{@{}c@{}}(\lambda x.M)\;N→_{\beta}M[x:=N%
]\end{array}$*
In the above definition, $M[x:=N]$ is the notation used to represent the term that results from the substitution of all the occurrences of the variable $x$ in the term $M$ by a term $N$ .
The multi-step reduction $\mathrel{\mathrlap{→}\mkern 1.0mu→}_{\beta}$ is defined as the reflexive and transitive closure of $→_{\beta}$ , as follows:
**Definition 4 (Multi-Step)**
*$\mathrel{\mathrlap{→}\mkern 1.0mu→}_{\beta}$ is the smallest relation on lambda terms such that $\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{%
}}M\mathrel{\mathrlap{→}\mkern 1.0mu→}_{\beta}M\end{array}}$ $\displaystyle\frac{\begin{array}[]{@{}c@{}}M\mathrel{\mathrlap{→}%
\mkern 1.0mu→}_{\beta}N~{}N\mathrel{\mathrlap{→}\mkern 1.0%
mu→}_{\beta}P\end{array}}{\begin{array}[]{@{}c@{}}M\mathrel{%
\mathrlap{→}\mkern 1.0mu→}_{\beta}P\end{array}}$ $\displaystyle\frac{\begin{array}[]{@{}c@{}}M→_{\beta}N\end{array}}{%
\begin{array}[]{@{}c@{}}M\mathrel{\mathrlap{→}\mkern 1.0mu%
→}_{\beta}N\end{array}}$*
We say that a term $M$ has a normal form if there is a term $N$ such that $M\mathrel{\mathrlap{→}\mkern 1.0mu→}_{\beta}N$ and N is a normal form. Not every term has a normal form. One example is the term $(\lambda x.x\;x)\;(\lambda x.x\;x)$ that $\beta$ -reduces to itself.
A term can have more than one redex, which means that when we try to apply $\beta$ -reduction on a term, we have multiple possibilities. It is useful to have a strategy to select which redex we want to reduce at each computation step. An evaluation strategy is a function that chooses a single redex for every reducible term.
The two most common evaluation strategies are: (i) normal or leftmost order, where the leftmost, outermost redex of a term is reduced first, and the (ii) applicative or strict order, where rightmost, innermost redex of a term is reduced first. An outermost redex is a redex not contained in another redex, and an innermost redex is a redex that does not contain other redexes.
Choosing the evaluation strategy is important to clearly define which redex to reduce through $\beta$ -reduction. Furthermore, it is not just a matter of personal preference since there is a theorem that says that if a term $M$ has a normal form $P$ , then the normal order evaluation strategy will always reach $P$ from $M$ , in a finite number of $\beta$ reductions.
Therefore, in this work, we always use the normal order evaluation strategy when making $\beta$ reductions on terms to ensure that if the term has a normal form, we can reach it.
There is another type of reduction in the Lambda calculus, the $\alpha$ -reduction, which is responsible for the renaming of bound variables when necessary. But since we are following the Barendregt convention [2], which states that the name of the bound variables will always be unique, we do not need to consider $\alpha$ -reduction in this work.
3.3 Encodings and Computations
The notion of encoding is well-known in Computer Science; for example, our modern computers operate on binary code, on top of which we build abstract ideas. In Lambda calculus, the idea is the same. We can use the structure of function abstractions and applications to encode representations for numbers, booleans, strings, etc.
In this work, we adopt the Church Encoding for representing Boolean expressions. Examples of such encoding are given below:
$$
\begin{array}[]{lcl}\mathtt{true}&\equiv&\lambda x.\lambda y.x\\
\mathtt{false}&\equiv&\lambda x.\lambda y.y\\
\mathtt{and}&\equiv&\lambda p.\lambda q.~{}(p~{}q)~{}p\\
\mathtt{or}&\equiv&\lambda p.\lambda q.~{}(p~{}p)~{}q\\
\mathtt{not}&\equiv&\lambda p.(p~{}\mathtt{false})~{}\mathtt{true}\end{array}
$$
With the Boolean constants $\mathtt{true}$ and $\mathtt{false}$ , and with the Boolean operator $\mathtt{and}$ , we can codify other Boolean expression such as $\mathit{true~{}\wedge~{}false}$ as the lambda term $(\mathtt{and}\ \mathtt{true})~{}\mathtt{false}$ that reduces to its normal form $\mathtt{false}$ in four small-steps as follows:
$$
\begin{array}[]{lcl}&&(\mathtt{and}\ \mathtt{true})~{}\mathtt{false}\\
&\equiv&((\lambda p.\lambda q.~{}(p~{}q)~{}p)~{}\mathtt{true})~{}\mathtt{false%
}\\
&\rightarrow_{\beta}&(\lambda q.~{}(\mathtt{true}\ ~{}q)~{}\mathtt{true})~{}%
\mathtt{false}\\
&\rightarrow_{\beta}&(\mathtt{true}\ ~{}\mathtt{false})~{}\mathtt{true}\\
&\equiv&((\lambda x.\lambda y.~{}x)~{}\mathtt{false})~{}\mathtt{true}\\
&\rightarrow_{\beta}&(\lambda y.~{}\mathtt{false})~{}\mathtt{true}\\
&\rightarrow_{\beta}&\mathtt{false}\\
&\equiv&\lambda x.\lambda y.y\end{array}
$$
3.4 Prefix Notation
The lambda terms presented in the previous section are written in what we call traditional notation. For this work, we only consider $\lambda$ -terms in the prefix notation for the learning tasks. To write lambda terms in the prefix notation, we need to add the application symbol (@) to the syntax. An application written as $(N~{}M)~{}P$ in the traditional notation, for example, is written as $\textit{@}\textit{@}M~{}N~{}P$ in the prefix notation.
We also change the $\lambda$ symbol for this representation using the uppercase letter “L”. The terms $\mathtt{true}$ , $\mathtt{false}$ , and $\mathtt{and}$ in the prefix notation are:
$$
\begin{array}[]{lcl}\mathtt{true}&\equiv&\mathrm{L}~{}x~{}\mathrm{L}~{}y~{}x\\
\mathtt{false}&\equiv&\mathrm{L}~{}x~{}\mathrm{L}~{}y~{}y\\
\mathtt{and}&\equiv&\mathrm{L}~{}p~{}\mathrm{L}~{}q~{}@~{}@~{}p~{}q~{}p\\
\end{array}
$$
We chose prefix notation because it offers a well-organized structure derived from a tree-like representation. This structure allows for a more straightforward representation of expressions as it is unambiguous and eliminates the need for parentheses. This makes it easier to process expressions, particularly for the purposes of learning and understanding complex mathematical concepts.
3.5 De Bruijn Index
The De Bruijn index is a tool for defining $\lambda$ -terms without having to name the variables [10]. This approach can benefit us, since the terms are agnostic to the variable naming and are simpler in the sense that they are shorter.
Basically, it just replaces the variable names by natural numbers. The abstraction no longer has a variable name, and every variable occurrence is represented by a number, indicating at which abstraction it is binded. These nameless terms are called de Bruijn terms, and the numeric variables are called de Bruijn indices [26].
For simplicity, we denote the free variables with the number $0 0$ , and the indices of the bound variables start at $1$ . This notation assumes that each de Bruijn index corresponds to the number of binders (abstractions) under which the variable is.
This notation can also be used in conjunction with the prefix notation. We will use it to compare with the traditional notation and see if there is any advantage in using a notation with no variable names for the tasks we are interested in.
Here we have examples of lambda terms in de Bruijn notation next to their prefixed notation:
$$
\begin{array}[]{lclll}\mathtt{true}&\equiv&\lambda.\lambda.2&-&\quad\mathrm{L}%
~{}\mathrm{L}~{}2\\
\mathtt{false}&\equiv&\lambda.\lambda.1&-&\quad\mathrm{L}~{}\mathrm{L}~{}1\\
\mathtt{and}&\equiv&\lambda.\lambda.~{}(2~{}1)~{}2&-&\quad\mathrm{L}~{}\mathrm%
{L}~{}\textit{@}~{}\textit{@}~{}2~{}1~{}2\\
\end{array}
$$
4 ML and Neurosymbolic AI
Machine learning (ML) is a subfield of artificial intelligence that involves the development of algorithms and models that can learn from data to make predictions or decisions. ML algorithms can be trained on large amounts of data, allowing them to identify patterns and relationships in the data and improve their accuracy over time [13].
In supervised learning, algorithms are trained on labeled data, where the output or target variable is known [13]. These algorithms can make predictions about new and unseen data and can be used in applications such as image classification or stock price prediction, for instance.
Unsupervised learning algorithms are trained on unlabeled data where the output or target variable is not known. These algorithms can identify patterns and relationships in the data and can be used in applications that require grouping data into clusters or detecting anomalies in them.
Reinforcement learning algorithms are designed to learn from interactions with an environment. These algorithms receive a reward or penalty for each action they take, and they can be used in various applications, such as game-playing and robotics.
This work focuses on supervised learning, particularly on connectionist AI (neural networks).
4.1 Neurosymbolic AI
Neurosymbolic AI is a field of artificial intelligence that combines the strengths of both symbolic AI and connectionist AI. Symbolic AI represents knowledge in a structured and human-readable form and uses rule-based reasoning systems to perform tasks. Connectionist AI, on the other hand, represents knowledge as patterns in a network of simple processing units. Neurosymbolic models aim to merge the two approaches by incorporating symbolic reasoning and/or representation with neural networks’ learning and generalization capabilities [8].
The paper [16] presents six different forms of neurosymbolic AI, varying in how and where the two approaches are combined. In the present work, we use the form Neuro: Symbolic $→$ Neuro, where we take a symbolic domain (reductions of the $\lambda$ calculus) and apply it to a neural architecture (the Transformer).
4.2 Neural Networks
Artificial Neural Networks (NNs) were inspired by the structure and function of the human brain and are designed to process large amounts of data to identify patterns and relationships. Their fundamental unit is the neuron, which essentially "activates" when a linear combination of its inputs surpasses a certain threshold. A Neural Network is merely a collection of interconnected neurons whose properties are determined by the arrangement of the neurons and their characteristics [29].
These neurons are often organized into layers. The input data are fed into the first layer, and the output of each neuron in a given layer is used as the input for the next layer until the final layer produces the network output. The connections between the neurons are represented by weights that are updated during the training process to minimize the error between the predicted output and the actual output.
NNs have been applied to a wide range of tasks, including image classification, speech recognition, and natural language processing. One of the main advantages of NNs is their ability to model nonlinear relationships between inputs and outputs. This makes NNs a powerful tool for solving complex real-world problems. However, traditional NNs have fixed-size inputs and outputs, which are not suitable for our desired tasks, which have inputs and outputs of variable sizes.
4.3 Sequence-to-sequence Models
Although neural networks are versatile and effective, they are only suitable for problems where inputs and targets can be represented by fixed-dimensional vector encodings. This is a significant constraint, as many crucial problems are better expressed using sequences of unknown lengths, such as speech recognition and machine translation. It is evident that a versatile method that can learn to translate sequences to sequences without being restricted to a specific domain would be valuable [30].
Sequence-to-sequence (seq2seq) models emerged from this need. They are a type of deep learning model that is used for tasks that involve mapping an input sequence to an output sequence of variable length. They have traditionally been applied to various natural language processing tasks, such as machine translation, text summarization, and text generation. The assembly of seq2seq models can be done according to different model architectures such as RNN [21], LTSM [30], GRU [6] and Transformer [35].
Given that we can see the tasks we want to accomplish in this work as machine translation tasks, we have opted to employ the sequence-to-sequence model using the Transformer.
4.4 The Transformer Model
The Transformer model is a type of neural network architecture that was introduced in [35]. It is designed to handle sequential data, such as natural language, and has quickly become one of the most popular models for tasks such as natural language processing, machine translation, text classification, and question answering. One of the key innovations of the Transformer model is its use of a self-attention mechanism, which allows the model to dynamically weigh the importance of different parts of the input sequence. This allows the Transformer to capture long-range dependencies in the data, which is particularly useful for processing sequences of variable lengths. Another advantage of the Transformer is its parallelization capacity, which allows it to be trained efficiently on large amounts of data. The Transformer model can be trained in parallel on multiple sequences, which is not possible with other traditional sequence-to-sequence models.
We chose the Transformer model mainly because to perform the $\beta$ -reduction over lambda terms, it is necessary to substitute every occurrence of the variable in question with a term, and we believe that the self-attention mechanism can be used to “pay attention” to all these variable occurrences when performing the task.
5 Building Experiments
For each of the hypotheses outlined in the Introduction, we propose a different task for our model to learn. The hypothesis H1 claims the model can perform a single-step computation in the $\lambda$ -Calculus, that is, it can take a $\lambda$ -term and transform it according to the single-step $\beta$ -reduction rules of Definition 3 following a normal order strategy. We call this the One-Step Beta Reduction (OBR) task.
The hypothesis H2 is that the model can perform multiple reduction steps in Lambda Calculus, taking a normalizable $\lambda$ -term, i.e., a $\lambda$ -term that has a normal form, and transforming it into its normal form through multiple beta reduction steps, following a normal order strategy. We call the task associated with this hypothesis the Multi-Step Beta Reduction (MBR) task.
The primary focus of our research question aligns with the second hypothesis. However, we chose to begin with a more straightforward hypothesis as a starting point. The first task is considered easier because it requires the execution of a single computational step, which is less complex than performing a full computation. This approach helps us gradually build our understanding and confidence before moving on to the more challenging second hypothesis.
To support these hypotheses, we generate several datasets for each of the tasks and use them to train machine learning models. By training the models on these datasets, we will determine if the models can learn and perform the tasks associated with each hypothesis.
5.1 On Training
To learn the tasks mentioned before, we use a neural model. Since the $\lambda$ -terms we are using do not have a fixed size, we need our model to accept inputs of varying lengths and generate outputs accordingly. To achieve this, we use a sequence-to-sequence model (seq2seq), which allows for inputs and outputs of different sizes. Specifically, we use the Transformer model proposed by [35]. This model has been widely used for various applications, including symbolic ones, as demonstrated by [18].
For the hyperparameters, preliminary tests showed us that the parameters used by [18] were good enough for our tasks. If needed, they can be adjusted in the training process. So, the initial hyperparameters are the following:
- Number of encoding layers - 6
- Number of decoding layers - 6
- Embedding layer dimension - 1024
- Number of attention heads - 8
- Optimizer - Adam [17]
- Learning rate - $1× 10^{-4}$
- Loss function - Cross Entropy
5.1.1 Experimental Setting
The experiments were conducted on a server with the following configuration:
- CPU: Intel(R) Core(TM) i7-8700 CPU @ 3.20GHz
- RAM: 32 GB (2 x 16 Gb) DDR4 @ 2667 MHz
- GPU: Quadro P6000 with 24 Gb
- OS: Ubuntu 18.04.5 LTS
Our initial goal was to run each training session for 12 to 24 hours. The preliminary results showed that each training consisting of $50$ epochs with an epoch size of $50000$ would take between 12 and 30 h to complete. So, we chose this arrangement. This configuration allows the model to process a total of $2.5× 10^{6}$ equations, which is $2.5$ times the size of the dataset.
With this machine, model, and configuration, we can safely have inputs with up to 250 tokens. With more than that, we end up with a memory shortage.
5.2 Lambda Sets and Datasets
All the datasets generated for this work are simple text files with each line in the format
$$
\mathtt{BETA~{}M~{}N}
$$
For the OBR task, the pair of terms in BETA M N is interpreted as: $\lambda$ term $N$ results of a one-step reduction of $\lambda$ term $M$ following the normal order strategy. For the MBR task, BETA M N is interpreted as: $\lambda$ term $N$ is the normal form that results from a multi-step reduction of $\lambda$ term $M$ , following the normal order strategy.
To generate the datasets on which the models will train, we first generate Lambda Sets (LSs) containing only lambda terms. From these LSs, we generate the datasets needed for the training. We start generating the following three LSs:
- Random Lambda Set (RLS): This LS is generated as random and unbiased as possible. Thus, this LS can have terms that do not have a normal form, and also terms that are codifications of Boolean expressions. With the datasets generated from this LS, we want to assert that the model can learn $\beta$ -reduction, regardless of whether the input terms represent meaningful codifications or have a normal form.
- Closed Bool Lambda Set (CBLS): This LS has its terms representing closed Boolean expressions. Thus, all the terms in this LS have a normal form. With the datasets generated from this LS, we want to assert that the model can learn the $\beta$ -reductions from meaningful codifications. In addition, these datasets are useful to validate the models trained with the RLS datasets, i.e., to validate whether the model learned from random terms can perform computations on terms that are meaningful codification.
- Open Bool Lambda Set (OBLS): The terms in this LS are codifications of open Boolean expression, that is, with free variables in them. With the datasets generated from this LS, we want to assert that the model can learn $\beta$ -reduction from terms that are meaningful codifications, even if they have free variables.
For the One-Step Beta Reduction Task (OBR), we generate datasets based on the three LSs proposed. However, for the Multi-Step Beta Reduction task, we do not utilize the Random LS to generate datasets, as the terms produced randomly may not have a normal form and result in an infinite loop during the multi-step $\beta$ -reduction.
In addition to the LS mentioned above, we create an additional LS for each task, which we refer to as a Mixed Lambda Set (MLS). For OBR, the MLS comprises terms coming from RLS, CBLS, and OBLS in the same proportion. For the MBR, the MLS is formed by terms from CBLS and OBLS, which are in the same proportion. With these mixed LSs, we want to assert that the model can learn from a domain that considers several kinds of terms.
From each of the four lambda sets presented above, we generate three datasets (all in the prefix notation), one for each of the following schemes for variable-naming:
- De Bruijn: this variable naming convention, presented in Section 3.5 is a way of representing $\lambda$ -terms without naming the variables. It results in shorter terms and presents a factor that can be beneficial for our model.
- Traditional: Datasets following this convention are generated from the datasets in the de Bruijn notation by replacing the de Bruijn indexes by traditional variable names, such as $a$ , $b$ , $c$ , $x$ , $y$ , $z$ , etc, following alphabetical order. We utilize this convention because we want to compare the results of the learning process using the de Bruijn convention with those using the traditional convention
- Random Vars: This convention also uses the traditional convention for variable naming. However, for this version, we take the de Bruijn datasets and replace the de Bruijn indexes by traditional variable names chosen randomly. We utilize this approach because we want to check if the way we name the variables matters for the models’ accuracy.
In summary, for the OBR task, we ultimately have a total of 12 datasets, as illustrated in Figure 1, and for the MBR task, we have nine datasets, as shown in Figure 2. It should be noted that the same CBLS and OBLS are utilized by both the OBR and the MBR tasks, meaning that the initial $\lambda$ -terms for the datasets that employ these same LS are consistent across both tasks. These datasets provide us with a broad set of test cases to evaluate the performance of our models.
<details>
<summary>extracted/6501326/datasets_obr.jpeg Details</summary>
### Visual Description
## Flow Diagram: LS Types and Outputs
### Overview
The image is a flow diagram illustrating the relationship between different types of "LS" (likely referring to List or Logic Structure) and their corresponding outputs. The diagram shows four types of LS: Random LS, Closed Bool LS, Open Bool LS, and Mixed LS. Each LS type, except Mixed LS, branches out to three different outputs, labeled with prefixes "obr_rand_", "obr_cb_", "obr_ob_", and "obr_mix_" respectively, followed by suffixes "_db", "_trad", and "_rv". Open Bool LS also connects to Mixed LS.
### Components/Axes
* **Nodes:** The diagram consists of rectangular nodes with rounded corners, representing different LS types and their outputs.
* **Arrows:** Arrows indicate the flow of information or processing from one node to another.
* **Labels:** Each node is labeled with a descriptive name.
### Detailed Analysis
* **Random LS:** This node is located at the top of the diagram. It has three outputs:
* obr\_rand\_db
* obr\_rand\_trad
* obr\_rand\_rv
* **Closed Bool LS:** This node is located below the Random LS node. It also has three outputs:
* obr\_cb\_db
* obr\_cb\_trad
* obr\_cb\_rv
* **Open Bool LS:** This node is located below the Closed Bool LS node. It has three outputs:
* obr\_ob\_db
* obr\_ob\_trad
* obr\_ob\_rv
* Additionally, there is an arrow pointing from the Open Bool LS node to the Mixed LS node.
* **Mixed LS:** This node is located at the bottom of the diagram. It has three outputs:
* obr\_mix\_db
* obr\_mix\_trad
* obr\_mix\_rv
* There is also an arrow pointing from the Mixed LS node back to itself, suggesting a feedback loop or iterative process.
### Key Observations
* Each LS type (Random, Closed Bool, Open Bool, and Mixed) generates three distinct outputs, differentiated by the suffixes "_db", "_trad", and "_rv".
* The Open Bool LS type has a direct connection to the Mixed LS type, suggesting that the output of Open Bool LS influences or contributes to the Mixed LS.
* The Mixed LS has a self-referential connection, which might indicate a recursive or iterative process.
### Interpretation
The diagram illustrates a hierarchical structure where different types of LS are processed to generate specific outputs. The "obr" prefix likely stands for a common operation or module, while the suffixes "_db", "_trad", and "_rv" might represent different data formats, transformations, or result variations. The connection between Open Bool LS and Mixed LS suggests a dependency or integration between these two types. The self-referential connection in Mixed LS implies a feedback loop or iterative refinement process. The diagram provides a high-level overview of the relationships and flow between different LS types and their outputs, which could be useful for understanding the overall system architecture or data processing pipeline.
</details>
Figure 1: Scheme of how all the datasets for the OBR tasks are generated. It starts with the three Lambda Sets (RLS, CBLS, and OBLS) and ends with all 12 datasets available for the OBR task.
<details>
<summary>extracted/6501326/datasets_mbr.jpeg Details</summary>
### Visual Description
## Flow Diagram: LS Types and Members
### Overview
The image is a flow diagram illustrating the relationship between different types of "LS" (likely List or Logic Structure) and their members. The diagram shows three types of LS: Closed Bool LS, Open Bool LS, and Mixed LS. Each LS type is connected to three members, denoted as `_db`, `_trad`, and `_rv`. The Open Bool LS also connects to the Mixed LS.
### Components/Axes
* **Nodes:** The diagram consists of rectangular nodes with rounded corners. Each node contains a text label.
* **Arrows:** Arrows indicate the flow or relationship between the nodes.
* **LS Types (Left Column):**
* Closed Bool LS (top)
* Open Bool LS (middle)
* Mixed LS (bottom)
* **Members (Right Column):** Each LS type is connected to three members. The naming convention for the members is `mbr_[LS type abbreviation]_[suffix]`, where the suffix is either `db`, `trad`, or `rv`.
* For Closed Bool LS: `mbr_cb_db`, `mbr_cb_trad`, `mbr_cb_rv`
* For Open Bool LS: `mbr_ob_db`, `mbr_ob_trad`, `mbr_ob_rv`
* For Mixed LS: `mbr_mix_db`, `mbr_mix_trad`, `mbr_mix_rv`
### Detailed Analysis or Content Details
1. **Closed Bool LS:** This node is located at the top-left of the diagram. It has three outgoing arrows, each pointing to one of its members:
* `mbr_cb_db` (top-right)
* `mbr_cb_trad` (middle-right, top group)
* `mbr_cb_rv` (bottom-right, top group)
2. **Open Bool LS:** This node is located in the middle-left of the diagram. It has four outgoing arrows: three pointing to its members and one pointing to the Mixed LS node.
* `mbr_ob_db` (top-right, middle group)
* `mbr_ob_trad` (middle-right, middle group)
* `mbr_ob_rv` (bottom-right, middle group)
* Mixed LS (bottom-left)
3. **Mixed LS:** This node is located at the bottom-left of the diagram. It has three outgoing arrows, each pointing to one of its members:
* `mbr_mix_db` (top-right, bottom group)
* `mbr_mix_trad` (middle-right, bottom group)
* `mbr_mix_rv` (bottom-right, bottom group)
### Key Observations
* Both Closed Bool LS and Open Bool LS have three members each, with similar naming conventions.
* Open Bool LS has a direct relationship with Mixed LS.
* The suffixes `db`, `trad`, and `rv` are used consistently across all member types.
### Interpretation
The diagram illustrates a hierarchical relationship between different types of Logic Structures (LS) and their members. The "Open Bool LS" appears to influence or contribute to the "Mixed LS," suggesting a potential flow or transformation of data or logic from the "Open Bool LS" to the "Mixed LS." The consistent naming convention for the members (`_db`, `_trad`, `_rv`) suggests that these suffixes represent distinct categories or properties associated with each LS type. The diagram could represent a data processing pipeline, a class inheritance structure, or a logical decision tree.
</details>
Figure 2: Scheme of how all the datasets for the MBR tasks are generated. It starts with the two Lambda Sets (CBLS, and OBLS), and ends with all nine datasets that are available for the MBR task.
Each dataset contains around one million examles (pairs of terms BETA M N), and we further divide each dataset into training, validation, and test sets. Keeping with the methodology described by [18], we allocate approximately ten thousand examples for both the validation and the test sets. This division of the datasets into training, validation, and test sets allows us to effectively train our models, tune their parameters, and evaluate their performance on independent data. Using a large number of examples in each dataset and following established best practices, we want to ensure that our results are robust and representative of the underlying task.
5.2.1 Term Sizes
As mentioned in Section 5.1.1, the maximum number of tokens that our configuration allows is 250. With this restriction, we were able to generate the terS sizes listed in Table 1. Although we calculated these sizes using the datasets with terms in the traditional variable-naming convention, we expect similar results for the other datasets (with the exception of the de Bruijn convention, which should produce smaller term sizes).
| OBR closed bool open bool | random $9$ $5$ | $5$ $193$ $181$ | $249$ $97.6± 26.76$ $66.46± 21.73$ | $127.2± 64.99$ |
| --- | --- | --- | --- | --- |
| mixed | $5$ | $249$ | $86.93± 46.56$ | |
| MBR | closed bool | $9$ | $193$ | $97.55± 26.75$ |
| open bool | $5$ | $181$ | $66.46± 21.72$ | |
| mixed | $5$ | $181$ | $77.96± 28.02$ | |
Table 1: Table showing the minimum, maximum, and average sizes of the input $\lambda$ -terms for each dataset. The datasets considered were the ones that use traditional variable naming.
5.2.2 Number of Reductions
For certain Lambda sets, we iteratively generate the reductions until a normal form is reached for each term. Thus, another important metric we consider is the number of reductions each term had to undergo to reach its normal form. This number can be seen as the number of computational steps necessary to evaluate a given term. Table 2 shows the average number of reductions that the terms of each Lambda Set have undergone to generate their respective datasets for the OBR and MBR tasks.
| closed bool open bool mixed | $3$ $1$ $2$ | $100$ $100$ $100$ | $18.8± 12.22$ $18.88± 10.42$ $18.82± 11.32$ |
| --- | --- | --- | --- |
Table 2: Table showing the minimum, maximum, and average number of reductions that the terms of each Lambda Set have undergone The Mixed Lambda Set considered here is the one with terms coming only from the closed bool and open bool Lambda Sets.
5.3 Code and Implementation
In this work, we used two distinct pieces of code. The first piece of code, adapted from [18], was responsible for generating what we call intermediate $\lambda$ -terms. These intermediate lambda terms follow the syntax given by the grammar in Definition 1. This piece of code also handled the learning process.
The second piece of code is responsible for generating, from the intermediate lambda terms, the lambda terms in the formats required for the lambda sets, as described in Section 5.2. It also implements a simulator that performs reductions of these lambda terms. From the simulation results, it generates the datasets with pairs $\mathtt{BETA~{}M~{}N}$ where the lambda term $N$ is the result of the lambda term $M$ reduction.
We observe that after generating the datasets, they must first be cleaned by (i) deleting repeated pairs, and (ii) because we want all pairs to represent $\beta$ -reductions, we also delete all pairs $\mathtt{BETA~{}M~{}N}$ with the first component $M$ in normal form.
5.4 Accuracy and Similarity
To evaluate the performance of the model, its accuracy in predicting the data in the test data set is calculated and recorded after each epoch. This accuracy metric measures how well the model can make correct predictions on the data it has seen during training. For each of the models trained, we display a graph showing the evolution of the model’s accuracy (y-axis) over the epochs (x-axis).
The accuracy of the model determines whether the predicted string matches the expected output. However, accuracy may not be the only relevant metric for evaluating the performance of a model in text generation or other similar tasks. In some cases, it may be useful to measure the similarity between the predicted and expected strings, even if they are not identical. So, additionally, we used a string similarity metric to compare how close the predicted string is to the expected one. For this, we used a common string similarity metric, the Levenshtein distance, which measures the number of changes (insertions, deletions, or substitutions) needed to transform one string into the other [20]. This metric provides the absolute difference between the two strings, so we divide this distance by the maximum distance possible between the two strings (which is the length of the longer string) to generate a percentage of dissimilarity. Then, we subtract this value from 1 to get a percentage of similarity between the two strings. So, we also provide a string similarity value for each trained model. The formula used is as follows:
$$
\mathsf{str\_sim}\,(s_{1},s_{2})=~{}~{}1-\frac{\mathsf{lev\_dist}\,(s_{1},s_{2%
})}{\mathsf{max}\,(\mathsf{len}(s_{1}),\mathsf{len}(s_{2}))}
$$
As part of our analysis, we also assessed the capacity of the models trained with each dataset to evaluate the other datasets. We achieve this by performing additional evaluations with each of the already trained models. For this, we use a model trained with one dataset to evaluate the other datasets that use the same notation and are designed for the same task. For example, we take the model that trained on the obr_rand_trad dataset and evaluate how it performs on the obr_cb_trad, obr_ob_trad and obr_mix_trad datasets with respect to accuracy and similarity.
By evaluating a model on the other datasets, which it did not train on, we can better understand its strengths and weaknesses and its ability to generalize to new data. If the model performs well on other datasets of the same type, it may be a good sign that it has learned meaningful patterns in the data and can be applied to new, unseen data. If the model performs poorly on other datasets, it may indicate that the model has, for instance, overfit to the original training data or the data was not adequate.
6 Experimental Results
Some trainings experienced an oscillation in accuracy, indicating that the initial learning rate ( $1× 10^{-4}$ ) was too high. So, we had to adjust the learning rate for these trainings. We initially used the same value for all trainings, but decreased it based on the degree of accuracy oscillation. Table 3 shows the final learning rates for each training performed. Although the learning rate was adjusted for different trainings, we kept it consistent for the three conventions in each dataset for comparison purposes. It is important to note that we did not thoroughly search for the optimal learning rate; instead, we selected a parameter that resulted in satisfactory and converging accuracy.
| One-Step Beta Reduction | random | $1× 10^{-4}$ |
| --- | --- | --- |
| closed bool | $6× 10^{-5}$ | |
| open bool | $8× 10^{-5}$ | |
| mixed | $1× 10^{-4}$ | |
| Multi-Step Beta Reduction | closed bool | $3× 10^{-5}$ |
| open bool | $5× 10^{-5}$ | |
| mixed | $5× 10^{-5}$ | |
Table 3: Values for the learning rate hyperparameter chosen for each of the tasks and lambda sets trained. The value started with $1× 10^{-4}$ , and it was lowered as the trained showed an unacceptable oscillation, indicating the learning would not converge.
6.1 Training Results
This section presents graphs that illustrate the training results for every model trained. The graphs display the model’s accuracy for the test dataset of the respective training dataset as it evolves over the training epochs. Each graph presents the results for all three variable naming conventions utilized in this study: the traditional convention, the random vars convention, and the de Bruijn convention.
For the OBR task, the training for the random datasets can be seen in Figure 3, the closed bool datasets in Figure 4, the open bool datasets in Figure 5, and the mixed datasets in Figure 6. For the MBR task, the training for the closed bool datasets can be seen in Figure 7, the open bool datasets in Figure 8, and the mix datasets in Figure 9.
In addition to the graphs, tables 4 and 5 show the final accuracies, i.e. the accuracy of the last epoch for all the models trained for both the OBR and MBR tasks. The table also shows the average percentage of similarity of the strings, calculated using the Levenshtein distance shown in Section 5.4.
<details>
<summary>extracted/6501326/training_obr_random.jpeg Details</summary>
### Visual Description
## Line Chart: Accuracy vs. Epochs for Different Methods
### Overview
The image is a line chart comparing the accuracy of three different methods ("de Bruijn", "Random Vars", and "Traditional") over 50 epochs. The chart displays accuracy (in percentage) on the y-axis and the number of epochs on the x-axis.
### Components/Axes
* **X-axis:** Epochs, labeled from 0 to 50, with tick marks every 10 epochs.
* **Y-axis:** Accuracy (%), labeled from 0 to 100, with tick marks every 5%.
* **Legend:** Located in the bottom-right corner, it identifies the three methods:
* Green line: "de Bruijn"
* Dark Blue line: "Random Vars"
* Purple line: "Traditional"
### Detailed Analysis
* **de Bruijn (Green):**
* Trend: The accuracy increases rapidly from 0 to approximately 10 epochs, then plateaus with minor fluctuations.
* Data Points:
* Epoch 0: ~5%
* Epoch 5: ~50%
* Epoch 10: ~58%
* Epoch 20: ~64%
* Epoch 30: ~67%
* Epoch 40: ~67%
* Epoch 50: ~68%
* **Random Vars (Dark Blue):**
* Trend: Similar to "de Bruijn," the accuracy increases rapidly initially, then plateaus with minor fluctuations.
* Data Points:
* Epoch 0: ~5%
* Epoch 5: ~58%
* Epoch 10: ~62%
* Epoch 20: ~64%
* Epoch 30: ~69%
* Epoch 40: ~69%
* Epoch 50: ~69%
* **Traditional (Purple):**
* Trend: The accuracy increases rapidly in the beginning, surpasses the other two methods, and then plateaus with some fluctuations.
* Data Points:
* Epoch 0: ~2%
* Epoch 5: ~73%
* Epoch 10: ~78%
* Epoch 20: ~82%
* Epoch 30: ~84%
* Epoch 40: ~89%
* Epoch 50: ~88%
### Key Observations
* The "Traditional" method consistently outperforms the other two methods in terms of accuracy across all epochs.
* Both "de Bruijn" and "Random Vars" methods show similar performance, with "Random Vars" slightly edging out "de Bruijn" after approximately 20 epochs.
* All three methods exhibit a rapid increase in accuracy during the initial epochs, followed by a plateau, indicating diminishing returns with further training.
### Interpretation
The chart demonstrates the performance of three different methods over a series of epochs. The "Traditional" method appears to be the most effective, achieving higher accuracy compared to "de Bruijn" and "Random Vars." The initial rapid increase in accuracy for all methods suggests that the models learn quickly in the early stages of training. The subsequent plateau indicates that further training yields less significant improvements in accuracy. The data suggests that the "Traditional" method may have a better initial configuration or learning algorithm that allows it to achieve higher accuracy levels.
</details>
Figure 3: Graph displaying the progression for the training of the One-Step Beta Reduction task, for the random dataset, over the three different conventions.
<details>
<summary>extracted/6501326/training_obr_closed_bool.jpeg Details</summary>
### Visual Description
## Line Chart: Accuracy vs. Epochs for Different Methods
### Overview
The image is a line chart comparing the accuracy of three different methods ("de Bruijn", "Random Vars", and "Traditional") over 50 epochs. The chart displays how the accuracy of each method changes as the number of epochs increases.
### Components/Axes
* **X-axis:** Epochs, ranging from 0 to 50 in increments of 10.
* **Y-axis:** Accuracy (%), ranging from 0 to 100 in increments of 5.
* **Legend:** Located in the bottom-right corner, identifying each method by color:
* Green: "de Bruijn"
* Dark Blue: "Random Vars"
* Purple: "Traditional"
### Detailed Analysis
* **"de Bruijn" (Green):**
* The line starts at approximately 15% accuracy at epoch 0.
* It rapidly increases to approximately 90% accuracy by epoch 5.
* It plateaus around 97% accuracy after epoch 20, with minor fluctuations.
* **"Random Vars" (Dark Blue):**
* The line starts at approximately 10% accuracy at epoch 0.
* It rapidly increases to approximately 80% accuracy by epoch 5.
* It reaches approximately 95% accuracy by epoch 20.
* It plateaus around 97% accuracy after epoch 30, with minor fluctuations.
* **"Traditional" (Purple):**
* The line starts at approximately 5% accuracy at epoch 0.
* It rapidly increases to approximately 90% accuracy by epoch 3.
* It plateaus around 98% accuracy after epoch 20, with minor fluctuations.
### Key Observations
* All three methods show a rapid increase in accuracy during the initial epochs.
* The "Traditional" method reaches a high accuracy level slightly faster than the other two methods.
* After approximately 20-30 epochs, all three methods plateau, with only minor improvements in accuracy.
* The "Random Vars" method shows more fluctuations in accuracy compared to the other two methods.
### Interpretation
The chart demonstrates the learning curves of three different methods, showing how their accuracy improves over time (epochs). The rapid initial increase in accuracy suggests that the methods quickly learn the underlying patterns in the data. The plateauing of accuracy after a certain number of epochs indicates that the methods have reached their maximum performance level on the given dataset, and further training does not lead to significant improvements. The "Traditional" method appears to converge slightly faster, but all three methods achieve similar levels of accuracy in the end. The fluctuations in the "Random Vars" method might indicate a higher sensitivity to the specific training data or a less stable learning process.
</details>
Figure 4: Graph displaying the progression for the training of the One-Step Beta Reduction task, for the closed bool dataset, over the three different conventions.
<details>
<summary>extracted/6501326/training_obr_open_bool.jpeg Details</summary>
### Visual Description
## Line Chart: Accuracy vs. Epochs for Different Methods
### Overview
The image is a line chart comparing the accuracy of three different methods ("de Bruijn", "Random Vars", and "Traditional") over 50 epochs. The chart displays accuracy (in percentage) on the y-axis and the number of epochs on the x-axis. All three methods show a rapid increase in accuracy in the initial epochs, followed by a plateauing effect as the number of epochs increases.
### Components/Axes
* **X-axis:** Epochs, ranging from 0 to 50, with tick marks at intervals of 10.
* **Y-axis:** Accuracy (%), ranging from 0 to 100, with tick marks at intervals of 5.
* **Legend:** Located in the bottom-right corner, it identifies the three methods:
* Green line: "de Bruijn"
* Dark Blue line: "Random Vars"
* Purple line: "Traditional"
* **Gridlines:** Present in the background to aid in reading the values.
### Detailed Analysis
* **de Bruijn (Green):**
* Trend: Rapid increase in accuracy from epoch 0 to approximately epoch 5, followed by a gradual increase and plateauing.
* Approximate values: Starts around 52% at epoch 0, reaches approximately 90% by epoch 5, and fluctuates between 90% and 98% from epoch 20 onwards.
* **Random Vars (Dark Blue):**
* Trend: Rapid increase in accuracy from epoch 0 to approximately epoch 5, followed by a gradual increase and plateauing.
* Approximate values: Starts around 12% at epoch 0, reaches approximately 85% by epoch 5, and fluctuates between 92% and 98% from epoch 20 onwards.
* **Traditional (Purple):**
* Trend: Rapid increase in accuracy from epoch 0 to approximately epoch 5, followed by a gradual increase and plateauing.
* Approximate values: Starts around 45% at epoch 0, reaches approximately 82% by epoch 5, and fluctuates between 92% and 99% from epoch 20 onwards.
### Key Observations
* All three methods exhibit a similar trend: a rapid initial increase in accuracy followed by a plateau.
* The "Traditional" method appears to achieve slightly higher peak accuracy values compared to the other two methods, especially after epoch 20.
* The "Random Vars" method starts with the lowest initial accuracy but catches up to the other methods relatively quickly.
* After approximately 20 epochs, the accuracy of all three methods fluctuates within a narrow range (90% to 99%).
### Interpretation
The chart suggests that all three methods are effective in achieving high accuracy, but they differ in their initial learning rates. The "Traditional" method might have a slight advantage in terms of peak accuracy, but the differences become less significant as the number of epochs increases. The rapid increase in accuracy during the initial epochs indicates that the models learn quickly, and the plateauing effect suggests that further training beyond a certain number of epochs may not significantly improve performance. The fluctuations in accuracy after the plateau could be due to the inherent variability in the training data or the learning process.
</details>
Figure 5: Graph displaying the progression for the training of the One-Step Beta Reduction task, for the open bool dataset, over the three different conventions.
<details>
<summary>extracted/6501326/training_obr_mix.jpeg Details</summary>
### Visual Description
## Line Chart: Accuracy vs. Epochs for Different Methods
### Overview
The image is a line chart comparing the accuracy of three different methods ("de Bruijn", "Random Vars", and "Traditional") over 50 epochs. The chart displays accuracy (in percentage) on the y-axis and epochs on the x-axis.
### Components/Axes
* **Title:** There is no explicit title on the chart.
* **X-axis:**
* Label: "Epochs"
* Scale: 0 to 50, with tick marks at intervals of 10 (0, 10, 20, 30, 40, 50).
* **Y-axis:**
* Label: "Accuracy (%)"
* Scale: 0 to 100, with tick marks at intervals of 5 (0, 5, 10, ..., 100).
* **Legend:** Located in the bottom-right corner.
* "de Bruijn" - Green line
* "Random Vars" - Dark Blue line
* "Traditional" - Purple line
### Detailed Analysis
* **"de Bruijn" (Green Line):**
* Trend: Initially increases rapidly, then plateaus around 85-90% after approximately 20 epochs.
* Data Points:
* Epoch 0: ~15%
* Epoch 10: ~80%
* Epoch 20: ~85%
* Epoch 30: ~85%
* Epoch 40: ~88%
* Epoch 50: ~88%
* **"Random Vars" (Dark Blue Line):**
* Trend: Initially increases rapidly, then plateaus around 85-90% after approximately 30 epochs. Shows more fluctuation than the other two methods.
* Data Points:
* Epoch 0: ~10%
* Epoch 10: ~75%
* Epoch 20: ~85%
* Epoch 30: ~80%
* Epoch 40: ~80%
* Epoch 50: ~85%
* **"Traditional" (Purple Line):**
* Trend: Initially increases rapidly, then plateaus around 85-90% after approximately 15 epochs.
* Data Points:
* Epoch 0: ~5%
* Epoch 10: ~80%
* Epoch 20: ~90%
* Epoch 30: ~90%
* Epoch 40: ~90%
* Epoch 50: ~90%
### Key Observations
* All three methods show a rapid increase in accuracy during the initial epochs.
* The "Traditional" method appears to reach a stable accuracy level slightly faster than the other two.
* The "Random Vars" method exhibits more fluctuation in accuracy compared to the other two methods after reaching its plateau.
* All three methods converge to a similar accuracy range (85-90%) after a certain number of epochs.
### Interpretation
The chart suggests that all three methods are effective in achieving high accuracy, but they differ in their convergence speed and stability. The "Traditional" method might be preferred if a faster convergence is desired, while the "de Bruijn" method appears to be more stable than "Random Vars" after convergence. The choice of method may depend on the specific application and the trade-off between convergence speed and stability.
</details>
Figure 6: Graph displaying the progression for the training of the One-Step Beta Reduction task, for the mixed dataset, over the three different conventions.
<details>
<summary>extracted/6501326/training_mbr_closed_bool.jpeg Details</summary>
### Visual Description
## Line Chart: Model Accuracy vs. Epochs
### Overview
The image is a line chart comparing the accuracy of three different models ("de Bruijn", "Random Vars", and "Traditional") over 50 epochs. The chart displays the accuracy percentage on the y-axis and the number of epochs on the x-axis.
### Components/Axes
* **X-axis:** Epochs, labeled from 0 to 50 in increments of 10.
* **Y-axis:** Accuracy (%), labeled from 0 to 100 in increments of 5.
* **Gridlines:** Present on both axes, aiding in value estimation.
* **Legend:** Located in the bottom-right corner, identifying each model by color:
* Green: "de Bruijn"
* Dark Blue: "Random Vars"
* Purple: "Traditional"
### Detailed Analysis
* **de Bruijn (Green):**
* Trend: Initially increases rapidly, then plateaus around 80-83% after approximately 10 epochs.
* Approximate Values:
* Epoch 0: ~58%
* Epoch 5: ~75%
* Epoch 10: ~79%
* Epoch 50: ~82%
* **Random Vars (Dark Blue):**
* Trend: Increases rapidly initially, then plateaus around 73-76% after approximately 20 epochs.
* Approximate Values:
* Epoch 0: ~52%
* Epoch 5: ~68%
* Epoch 10: ~72%
* Epoch 50: ~75%
* **Traditional (Purple):**
* Trend: Increases rapidly initially, then plateaus around 80-83% after approximately 15 epochs.
* Approximate Values:
* Epoch 0: ~57%
* Epoch 5: ~70%
* Epoch 10: ~77%
* Epoch 50: ~83%
### Key Observations
* All three models show a rapid increase in accuracy during the initial epochs.
* The "de Bruijn" and "Traditional" models achieve similar accuracy levels, slightly outperforming the "Random Vars" model.
* The "Random Vars" model plateaus at a lower accuracy compared to the other two.
* After the initial increase, all models exhibit relatively stable accuracy with minor fluctuations.
### Interpretation
The chart demonstrates the learning curves of three different models. The "de Bruijn" and "Traditional" models converge to a higher accuracy level compared to the "Random Vars" model, suggesting they may be better suited for the task. The rapid initial increase in accuracy for all models indicates effective learning during the early epochs. The plateauing suggests that further training beyond a certain number of epochs may not significantly improve the accuracy of these models. The similar performance of "de Bruijn" and "Traditional" suggests they may share similar underlying mechanisms or be optimized for similar features in the data.
</details>
Figure 7: Graph displaying the progression for the training of the Multi-Step Beta Reduction task, for the closed bool dataset, over the three different conventions.
<details>
<summary>extracted/6501326/training_mbr_open_bool.jpeg Details</summary>
### Visual Description
## Line Chart: Accuracy vs. Epochs for Different Methods
### Overview
The image is a line chart comparing the accuracy of three different methods ("de Bruijn", "Random Vars", and "Traditional") over 50 epochs. The chart displays accuracy (in percentage) on the y-axis and the number of epochs on the x-axis.
### Components/Axes
* **X-axis:** Epochs, labeled from 0 to 50 in increments of 10.
* **Y-axis:** Accuracy (%), labeled from 0 to 100 in increments of 5.
* **Legend:** Located in the bottom-right corner, it identifies the three methods:
* "de Bruijn" (Green line)
* "Random Vars" (Dark Blue line)
* "Traditional" (Purple line)
* **Grid:** The chart has a grid for easier value reading.
### Detailed Analysis
* **de Bruijn (Green):**
* Trend: Rapid initial increase in accuracy, followed by stabilization around 90-95% after approximately 10 epochs.
* Data Points: Starts around 22% at epoch 0, reaches approximately 87% by epoch 8, and fluctuates between 90% and 98% from epoch 10 onwards.
* **Random Vars (Dark Blue):**
* Trend: Gradual increase in accuracy over the epochs, reaching a plateau around 75-80% after approximately 40 epochs.
* Data Points: Starts around 15% at epoch 0, reaches approximately 58% by epoch 8, 70% by epoch 20, and fluctuates between 75% and 82% from epoch 40 onwards.
* **Traditional (Purple):**
* Trend: Very rapid initial increase in accuracy, reaching a plateau around 95% after approximately 10 epochs.
* Data Points: Starts around 15% at epoch 0, reaches approximately 85% by epoch 6, and fluctuates between 92% and 98% from epoch 10 onwards.
### Key Observations
* The "Traditional" method and "de Bruijn" method achieve significantly higher accuracy compared to the "Random Vars" method.
* The "Traditional" method and "de Bruijn" method converge to high accuracy much faster than the "Random Vars" method.
* The "Traditional" method shows a slightly faster initial increase in accuracy compared to the "de Bruijn" method.
* All three methods show some fluctuations in accuracy after reaching their respective plateaus.
### Interpretation
The chart demonstrates the performance of three different methods in terms of accuracy over a series of epochs. The "Traditional" and "de Bruijn" methods are superior to the "Random Vars" method, achieving higher accuracy and faster convergence. The "Random Vars" method, while improving over time, plateaus at a significantly lower accuracy level. The fluctuations observed after the initial convergence suggest that further training may not significantly improve the accuracy of these methods. The data suggests that the "Traditional" and "de Bruijn" methods are more effective for the task being evaluated.
</details>
Figure 8: Graph displaying the progression for the training of the Multi-Step Beta Reduction task, for the open bool dataset, over the three different conventions.
<details>
<summary>extracted/6501326/training_mbr_mix.jpeg Details</summary>
### Visual Description
## Line Chart: Accuracy vs. Epochs for Different Methods
### Overview
The image is a line chart comparing the accuracy of three different methods ("de Bruijn", "Random Vars", and "Traditional") over 50 epochs. The chart displays accuracy (in percentage) on the y-axis and the number of epochs on the x-axis.
### Components/Axes
* **X-axis:** Epochs, ranging from 0 to 50, with tick marks at intervals of 10.
* **Y-axis:** Accuracy (%), ranging from 0 to 100, with tick marks at intervals of 5.
* **Legend:** Located in the bottom-right corner, it identifies the three methods:
* Green line: "de Bruijn"
* Dark Blue line: "Random Vars"
* Purple line: "Traditional"
### Detailed Analysis
* **"de Bruijn" (Green):** The accuracy increases rapidly from approximately 45% at epoch 0 to around 75% at epoch 10. It then continues to increase, but at a slower rate, reaching approximately 82% at epoch 20, 85% at epoch 30, and finally plateaus around 88-89% at epoch 50.
* **"Random Vars" (Dark Blue):** The accuracy starts at approximately 35% at epoch 0 and increases steadily to about 65% at epoch 10. The rate of increase slows down after epoch 10, reaching approximately 72% at epoch 20, 74% at epoch 30, and plateaus around 77-78% at epoch 50.
* **"Traditional" (Purple):** The accuracy increases sharply from approximately 38% at epoch 0 to about 83% at epoch 10. It continues to increase, but at a slower rate, reaching approximately 93% at epoch 20, 96% at epoch 30, and plateaus around 97% at epoch 50.
### Key Observations
* The "Traditional" method consistently outperforms the other two methods in terms of accuracy across all epochs.
* All three methods show a rapid increase in accuracy during the initial epochs (0-10), followed by a gradual plateauing as the number of epochs increases.
* The "Random Vars" method has the lowest accuracy among the three methods throughout the entire range of epochs.
### Interpretation
The chart demonstrates the performance of three different methods in terms of accuracy over a series of epochs. The "Traditional" method appears to be the most effective, achieving the highest accuracy and plateauing at a higher level compared to the other two methods. The "de Bruijn" method performs better than "Random Vars," but not as well as "Traditional." The plateauing effect suggests that increasing the number of epochs beyond a certain point may not significantly improve the accuracy of any of the methods. The initial rapid increase in accuracy indicates that the models learn quickly in the early stages of training.
</details>
Figure 9: Graph displaying the progression for the training of the Multi-Step Beta Reduction task, for the mixed dataset, over the three different conventions.
| random random vars de Bruijn | trad $69.30$ $67.84$ | $88.89$ $99.51$ $99.34$ | $99.83$ |
| --- | --- | --- | --- |
| closed bool | trad | $99.73$ | $100.00$ * |
| random vars | $98.10$ | $99.98$ | |
| de Bruijn | $98.16$ | $99.99$ | |
| open bool | trad | $98.82$ | $99.99$ |
| random vars | $94.88$ | $99.95$ | |
| de Bruijn | $97.94$ | $99.97$ | |
| mixed | trad | $92.88$ | $99.89$ |
| random vars | $88.52$ | $99.77$ | |
| de Bruijn | $87.93$ | $99.73$ | |
Table 4: Accuracy and the average string similarity for the evaluation of the models trained for the OBR task. * Rounded from $0.998$ .
| closed bool | trad | $82.75$ | $97.97$ |
| --- | --- | --- | --- |
| random vars | $76.08$ | $97.06$ | |
| de Bruijn | $82.20$ | $96.49$ | |
| open bool | trad | $97.70$ | $99.92$ |
| random vars | $80.92$ | $98.19$ | |
| de Bruijn | $97.02$ | $99.77$ | |
| mixed | trad | $97.63$ | $99.89$ |
| random vars | $76.58$ | $98.15$ | |
| de Bruijn | $89.99$ | $98.64$ | |
Table 5: Accuracy and the average string similarity for the evaluation of the models trained for the MBR task.
6.2 Evaluation Across Datasets
In this section, we show the results obtained by some additional evaluations with the already trained models for the OBR and MBR tasks. We use a model trained with one dataset to evaluate the other datasets that use the same convention and are designed for the same task. For example, we take the model that trained on the obr_cb_db dataset and evaluate how it performs on the obr_rand_db, obr_ob_db and obr_mix_db datasets. We use test datasets to perform these evaluations.
Tables 6 and 7 show the values found for the evaluations with the trained models for the OBR and MBR tasks, respectively.
| traditional closed bool open bool | random 0.00 0.04 | 88.89 99.73 80.01 | 63.69 7.73 98.82 | 72.66 35.92 63.79 | 80.47 35.85 60.67 | 76.43 |
| --- | --- | --- | --- | --- | --- | --- |
| mixed | 72.26 | 97.42 | 99.62 | 92.88 | 90.55 | |
| random vars | random | 69.30 | 22.17 | 42.27 | 64.65 | 49.60 |
| closed bool | 0.05 | 98.10 | 18.82 | 39.26 | 39.06 | |
| open bool | 0.17 | 77.24 | 94.88 | 61.53 | 58.46 | |
| mixed | 65.77 | 83.90 | 85.92 | 88.52 | 81.03 | |
| de Bruijn | random | 67.84 | 47.15 | 58.35 | 61.14 | 58.62 |
| closed bool | 0.00 | 98.16 | 10.96 | 36.87 | 36.50 | |
| open bool | 0.01 | 77.93 | 97.94 | 58.59 | 58.62 | |
| mixed | 65.70 | 96.39 | 98.71 | 87.93 | 87.18 | |
Table 6: Accuracy (%) for the evaluation of the models over different datasets, for the task of one-step beta reduction. For each of the three different conventions (trad, random vars, and De Bruijn), the model trained with each dataset (rows) was evaluated with each dataset (columns). The last column indicates the average accuracy of the model over the different datasets.
| traditional open bool mixed | closed bool 92.21 96.20 | 82.75 97.70 93.28 | 15.85 96.86 97.63 | 49.66 95.59 95.70 | 49.42 |
| --- | --- | --- | --- | --- | --- |
| random vars | closed bool | 76.08 | 24.79 | 50.98 | 50.62 |
| open bool | 75.23 | 80.92 | 84.25 | 80.13 | |
| mixed | 72.72 | 50.68 | 76.58 | 66.66 | |
| de Bruijn | closed bool | 82.20 | 20.20 | 57.83 | 53.41 |
| open bool | 90.02 | 97.02 | 95.37 | 94.14 | |
| mixed | 88.43 | 78.64 | 89.99 | 85.69 | |
Table 7: Accuracy (%) for the evaluation of the models over different datasets, for the task of multi-step beta reduction. For each of the three different conventions (trad, random vars, and De Bruijn), the model trained with each dataset (rows) was evaluated with each dataset (columns). The last column indicates the average accuracy of the model over the different datasets.
7 Discussion
In this section, the results obtained from the experiments carried out in the study are discussed in detail. The results are analyzed and interpreted to draw conclusions about the objectives of the study.
7.1 Training
In this section, we discuss the results of the trainings presented in Section 5. With these results, we are able to determine which datasets and conventions performed better and try to conjecture some hypotheses about what happened in the trainings.
7.1.1 One-Step Beta Reduction
In the training of the models for the OBR task, it was found that each model achieved an accuracy of at least $67.84\%$ . However, when only the best conventions were considered, each model achieved a minimum accuracy of $88.89\%$ . Furthermore, a model achieved remarkable accuracy $99.73\%$ . These findings, which can be seen in Table 4, highlight the high level of accuracy and effectiveness of the models, particularly when utilizing optimal conventions, which supports hypothesis H1.
The similarity metric for the strings can also be seen in Table 4 and indicates that, despite incorrectly predicting some terms, the model was able to accurately predict a significant portion of those terms, with all similarities being at least $99.34\%$ . If we take only the best conventions, this number goes up to $99.83\%$ . In addition, some models achieved an outstanding performance of more than $99.99\%$ for this metric. For example, the model trained with the random dataset with the de Bruijn convention got a final accuracy of $67.84\%$ . However, the string similarity metric for the same training was $99.34\%$ . This illustrates how much closer to the correct answers were the incorrect answers obtained by the model.
Upon analyzing the performance of the models on different datasets, it is evident that the closed bool and open bool datasets were easier to learn compared to other datasets, as we can see in Figures 3, 4, 5 and 6. The Boolean datasets achieved good accuracies in a shorter span of time and presented similar results between themselves. The random dataset was the hardest to learn, as shown in Fgurie 3. We think this is due to the absence of more defined patterns among the terms. The mixed dataset, as expected, fell between random and boolean data sets in terms of difficulty to learn. However, its accuracy surprised us, since it was the most diverse dataset, which means that it learned to perform the OBR task both for random and Boolean terms, with high accuracies ( $92.88\%$ for the optimal convention, as shown in Table 4).
It should be noted that, although the accuracies for the random and mixed data sets were comparatively lower than those of the Boolean datasets, the graphs illustrating their performance present a growing pattern, as illustrated in Figures 3 and 6. This indicates that further training with more epochs could yield higher accuracies for these datasets.
Analyzing the performance of the models that use different conventions in Table 4, it can be observed that the traditional convention consistently outperformed the other two conventions, which exhibited similar levels of performance. However, the only training that the convention really made a difference was in the random dataset, which we saw was the hardest to learn. We suppose that for the other datasets, the difference in convention did not matter because it was so easy for the model to learn that even the “harder” conventions were not a problem.
We also think that the traditional convention performed overall better than the other two conventions because for the de Bruijn convention, despite being based on a simpler notation, the beta reduction is more intricate, and consequently, harder to learn. Furthermore, compared to the random-vars convention, the traditional convention, with its ordered naming rule, tends to provide the model with more predictable outcomes.
7.1.2 Multi-Step Beta Reduction
For the training of the models for the MBR task, every model achieved a minimum accuracy of $76.08\%$ . However, when considering only the best conventions, each model exhibited an accuracy of at least $82.75\%$ . Furthermore, one model achieved an exceptional $97.70\%$ accuracy. These results, which can be seen in Table 5, emphasize the effectiveness and high accuracy of the models, especially when using the optimal conventions, which supports hypothesis H2.
The similarity metric for the strings, found in Table 5, again indicates that, even though the model made incorrect predictions for some terms, it accurately predicted a significant portion of those terms, with all similarities no less than $96.49\%$ . Considering only the best conventions, this number increases to $97.97\%$ . Furthermore, some models performed exceptionally well, achieving up to $99.92\%$ for this metric. Again, the models that did not obtain a good accuracy exhibited outstanding performance in this metric. For example, the model trained with the mixed dataset, using the random vars convention, obtained an accuracy of $76.58\%$ . However, the string similarity metric for the same training was $98.15\%$ . This shows that for this task, the models also got the wrong predictions very close to the correct ones.
For the closed bool dataset in the MBR task, it is important to note that the set of possible terms that the model should predict is small (namely, true and false). For the traditional convention and, especially, for the random vars convention, the true and false terms are not always the same term, since there are many alpha-equivalent terms for true and false using the English alphabet. But in the DB case, there are only 2 distinct terms for the true and false (“ L L 2 ” and “ L L 1 ”, respectively). Thus, one might expect that the closed bool dataset would be easier to learn since there are only a few possible terms for the model to predict (only two in the DB case), while the open bool, on the other hand, had output terms that differ dramatically from one another.
However, the opposite was actually observed, as we can see in Figures 7 and 8. The closed bool dataset was found to be harder to learn than the open bool dataset, with the model that trained on it having significantly lower accuracy than the open bool model, which seems counter-intuitive. Our hypothesis is that, precisely because the terms were so similar in the closed bool dataset, the model resorted to guessing the output term from a limited set of possibilities, based on some features of the inputs, instead of learning to perform the reductions. But, since this was not possible for the open bool dataset, the model was forced to actually learn to perform the multi-step beta reduction on the input terms. The fact that the closed bool model already starts the training with around $55\%$ accuracy also corroborates to our hypothesis that the model is learning to guess from a limited set instead of learning the reductions.
The model trained with the mixed dataset seems to have overcome this issue, as we can see in Figure 9. Considering the traditional convention, the accuracy of the model was similar to the accuracy of the model trained on the open bool dataset, even with half of its terms having come from the closed bool dataset. This actually supports our previous hypothesis, since we think that having more variability on the terms forced the model to learn the reductions instead of only guessing between a small set of possible outcomes.
For the trainings on different conventions, Table 5 shows that the random vars convention had the worst accuracies for the three datasets. However, only the models trained on the open bool and on the mixed datasets presented a large gap between different conventions. We suppose that the naming convention did not change the guessing factor on the learning process for the models that trained on the closed bool. What is interesting is that the de Bruijn convention led to accuracies as good as the traditional convention and significantly better than the random vars convention for the models trained on the open bool and closed bool datasets. This was unexpected since the $\beta$ reduction in the de Bruijn notation is more intricate than in the traditional notation, which the other two conventions use. For the model trained on the mixed dataset, the order of the different conventions was more aligned with the expected, with the traditional being the best convention, followed by the other two. However, this result, although expected, was unusual, since the other models did not follow this order.
7.2 Evaluations Across Datasets
In this section, we discuss the results of the evaluations in the datasets presented in Section 6.2. These evaluations can give us some insight into whether the model really learned the reductions or whether it just learned the reductions for that specific set of terms.
7.2.1 One-Step Beta Reduction
Evaluations of this task have yielded promising results, especially for models trained with the mixed dataset. It produced better average accuracies for all models in the OBR tasks, as seen in Table 6. This shows that, as expected, these models were able to better capture the diversity of terms present in the different datasets.
The models trained with both Boolean datasets performed poorly for the evaluation with the random dataset, with accuracies close to $0\%$ , as we can see in Table 6. We suppose that this happened because the terms in the random data set are very distinct from the terms in the Boolean datasets. Also, since the opposite did not happen, we think that the random dataset contains terms that are actually harder to learn, as we presumed in the previous section.
As expected, almost every model had better accuracy in the evaluation with the dataset in which it was trained than with the others, as shown in Table 6. But one result that may be seen as counterintuitive is the evaluation of the model trained with the mixed dataset. It had better accuracy for the open bool and closed bool datasets for the traditional and de Bruijn conventions. We again suppose that this happened because the random dataset is the hardest to learn. Thus, since the mixed dataset has 1/3 of its terms from the random dataset, it ends up being harder than the closed bool and open bool datasets. So, it ends up evaluating those two datasets better than the dataset it was trained with, which contains terms from the random dataset.
Another interesting result is that the model trained on the open bool dataset was able to extrapolate and obtain good accuracies for the evaluation of the closed bool dataset, with a minimum accuracy of $77.24\%$ . But the opposite did not happen, with accuracies as low as $7.73\%$ , as we can see in Table 6.
Aside from what was mentioned, the different conventions did not present a significant difference between the evaluations.
7.2.2 Multi-Step Beta Reduction
The evaluations for this task have again yielded good results, particularly for the models trained with the open bool dataset. As shown in Table 7, the use of the open bool dataset led to better average accuracies for almost all models in the MBR task.
Table 7 shows that, as expected, the majority of models performed better in the evaluations using the dataset they were trained on, as opposed to the other datasets. However, the models trained with the open bool dataset had accuracies quite close to one another for the three datasets evaluated. In fact, it presented better accuracy for the mixed dataset rather than on the dataset on which it was trained. We presume that this happened because the model trained with the open bool dataset was able to generalize better than the others.
Again, the models trained with the closed bool did not extrapolate and obtained good accuracies for the other datasets, especially the closed bool, with accuracies as low as $15.85\%$ , as seen in Table 7. But the opposite happened, with the open bool models getting a minimum of $75.23\%$ of accuracy for the closed bool dataset. We think that this happened for the same reason discussed in Section 7.1.2, which is that the model trained on the closed bool dataset just learned to guess the output from a limited set of possible terms, not actually learning the $\beta$ -reduction. Apart from what was stated, the different conventions did not present any main differences between the evaluations.
8 Conclusions and Further Work
Through comprehensive experimentation and analysis, it was demonstrated that the Transformer model is capable of capturing the syntactic and semantic features of $\lambda$ -calculus, allowing for accurate and efficient predictions. The results obtained were positive, with overall good accuracies for both tasks at hand. For the One-Step Beta Reduction, we got accuracies up to $99.73$ %, and string similarity metric of over $99.99$ %. For the Multi-Step Beta Reduction, we obtained accuracies of up to $97.70$ %, and string similarity metric exceeding $99.90$ %. In addition to that, the models presented a good generalization performance across different datasets.
Due to limitations of hardware and time, our models trained for just 50 epochs. Considering that is a pretty low number compared with substantial trainings of large models and that we did not do a search for the optimal hyperparameters, we can assure that the accuracy of our models can be even higher than what was presented here. Addressing the technological limitations of our work would provide a way for further advancements.
These results illustrate the effectiveness of the model in learning the desired tasks and support the two hypotheses raised in this study and, subsequently, the proposed research question. In addition, these results showed that the Transformer self-attention mechanism is well suited for capturing the dependencies between variables and functions in the $\lambda$ -Calculus.
We believe that the methods and results presented in this work have yielded some significant results for future research. The main contributions that have resulted from this research can be summarized as follows.
- Lambda calculus learning: The outcomes from learning the reductions of Lambda Calculus are promising and hold potential implications for future research in the field of AI and computer programs.
- Dataset generation: Since datasets for lambda terms and reductions did not exist, we implemented the generation for these datasets from scratch. These datasets and generation methods can be used in future research in the Lambda Calculus domain.
- Functional programming learning: The results obtained in this study can be taken into account to shift the programming paradigm from imperative to functional in future research in the field of learning to compute.
Of course, our contributions are mainly in the proposal of a novel neural Lambda Calculus, and the experiments we carried out serve to illustrate the potential of our approach in AI and programming languages. Furthermore, although our research was limited to one formalism, the $\lambda$ -calculus, this opens the possibility of further analyzes of other computational calculi. Thus, with respect to future research, we propose the following. 1. Further training experiments: The current study trained the model for a limited number of epochs. Further research could aim to train the best notation for more epochs to see if performance can be improved. 2. Hyperparameter optimization: The study used a set of predefined hyperparameters for the transformer model. A thorough search for the optimal hyperparameters could be conducted to find the best set of hyperparameters for learning Lambda Calculus. 3. Improved error analysis: The study provided a preliminary error analysis, but more work could aim to conduct a more in-depth error analysis to better understand the types of mistakes the model is making and to identify areas for improvement. 4. Incorporating other formalisms: This study focused on learning Lambda Calculus, but there are other formalisms such as Combinatorial Logic and Turing Machines that could be trained by the model and compared with the current work. 5. Solve typing problems: Learn how to solve some typing problems (well-typedness, type assignment, type checking, and type inhabitation [26]) that can be uncomputable for some typed $\lambda$ -Calculus 6. Learn more complex versions of the $\lambda$ -Calculus: Learn the non-pure $\lambda$ -Calculus, with numbers and arithmetical and Boolean operations already embedded. 7. Learn to compute a functional programming language: Learn a functional programming language based on $\lambda$ -Calculus, such as Haskell or Lisp [31]. 8. Learn to detect loops: Use the same methods for training, but instead of learning to perform the computations, learn to identify if a $\lambda$ -term does not have a normal form, i.e., if it is going to enter a loop when applying the reductions. 9. The Curry-Howard isomorphism [1] establishes a relationship between intuitionistic logic and the typed $\lambda$ -calculus. As already advocated by [9], it would be relevant to further exploit this relationship with respect to the connectionist model presented in [9, 8].
These future work suggestions have the potential to bring further advancements in the application of machine learning models to the field of symbolic learning. In particular, with respect to programming languages in general and in particular regarding the use of functional programming as the base paradigm. In summary, we believe that a neurosymbolic approach in which a neural lamda calculus is a foundation can contribute to a deeper understanding of the underlying computational processes in AI.
Declarations
L.C. Lamb and J.M. Flach contributed for this work in the conceptualization of the study. J.M. Flach performed the experiments. A.F. Moreira contributed to the aspects of Lambda Calculus. All authors contributed to the writing and revision. All authors read and approved the final manuscript. The authors declare that they have no competing interests. This research was supported in part by CAPES Finance Code 001 and the Brazilian Research Council CNPq. The datasets generated during the current study are available at https://bit.ly/lambda_datasets. The repository for the code generated during the current study is available at https://github.com/jmflach/SymbolicLambda
References
- [1] Henk Barendregt. The impact of the lambda calculus in logic and computer science. Bulletin of Symbolic Logic, 3(2):181–215, 1997.
- [2] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland Linguistic Series. North-Holland, 1984.
- [3] Tarek R Besold, Artur d’Avila Garcez, Sebastian Bader, Howard Bowman, Pedro Domingos, Pascal Hitzler, Kai-Uwe Kühnberger, Luis C Lamb, Daniel Lowd, Priscila Machado Vieira Lima, et al. Neural-symbolic Learning and Reasoning: A survey and interpretation. Neuro-Symbolic Artificial Intelligence: The State of the Art, 2022.
- [4] Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. Advances in neural information processing systems, 33:1877–1901, 2020.
- [5] Felice Cardone and J Roger Hindley. History of lambda-calculus and combinatory logic. Handbook of the History of Logic, 5:723–817, 2006.
- [6] Junyoung Chung, Caglar Gulcehre, KyungHyun Cho, and Yoshua Bengio. Empirical evaluation of gated recurrent neural networks on sequence modeling. arXiv preprint arXiv:1412.3555, 2014.
- [7] Alonzo Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):345–363, 1936.
- [8] Artur S. d’Avila Garcez, Luís C Lamb, and Dov Gabbay. Neural-Symbolic Cognitive Reasoning. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009.
- [9] Artur S. d’Avila Garcez, Luís C. Lamb, and Dov M. Gabbay. Connectionist computations of intuitionistic reasoning. Theor. Comput. Sci., 358(1):34–55, 2006.
- [10] Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381–392, 1972.
- [11] Thomas G Dietterich. Steps toward robust artificial intelligence. AI Magazine, 38(3):3–24, 2017.
- [12] Artur d’Avila Garcez and Luis C. Lamb. Neurosymbolic AI: The 3rd Wave. Artificial Intelligence Review, pages 1–20, 2023.
- [13] Ian Goodfellow, Yoshua Bengio, and Aaron Courville. Deep learning, volume 29. MIT Press, 2016.
- [14] Alex Graves, Greg Wayne, and Ivo Danihelka. Neural turing machines. arXiv preprint arXiv:1410.5401, 2014.
- [15] Łukasz Kaiser and Ilya Sutskever. Neural gpus learn algorithms. arXiv preprint arXiv:1511.08228, 2015.
- [16] Henry Kautz. The Third AI Summer: AAAI Robert Engelmore memorial lecture. AI Magazine, 43(1):105–125, 2022.
- [17] Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014.
- [18] Guillaume Lample and François Charton. Deep learning for symbolic mathematics. CoRR, abs/1912.01412, 2019.
- [19] Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. Deep learning. Nature, 521(7553):436, 2015.
- [20] V.I. Levenshtein. Binary codes capable of correcting deletions, insertions, and reversals. Soviet physics doklady, 10(8):707–710, 1966.
- [21] Zachary C Lipton, John Berkowitz, and Charles Elkan. A critical review of recurrent neural networks for sequence learning. arXiv preprint arXiv:1506.00019, 2015.
- [22] Chris Maddison and Daniel Tarlow. Structured generative models of natural source code. In International Conference on Machine Learning, pages 649–657. PMLR, 2014.
- [23] Gary Marcus and Ernest Davis. Rebooting AI: Building artificial intelligence we can trust. Vintage, 2019.
- [24] G. Michaelson. An Introduction to Functional Programming Through Lambda Calculus. Dover books on mathematics. Dover Publications, 2011.
- [25] Lili Mou, Ge Li, Yuxuan Liu, Hao Peng, Zhi Jin, Yan Xu, and Lu Zhang. Building program vector representations for deep learning. arXiv preprint arXiv:1409.3358, 2014.
- [26] Benjamin C Pierce. Types and programming languages. MIT press, 2002.
- [27] Kevin Roose. The brilliance and weirdness of chatgpt. The New York Times, 2022.
- [28] D. E. Rumelhart and J. L. McClelland. Parallel Distributed Processing: Explorations in the Microstructure of Cognition, Vol. 1: Foundations. MIT Press, 1986.
- [29] Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Pearson Series, 2021.
- [30] Ilya Sutskever, Oriol Vinyals, and Quoc V. Le. Sequence to sequence learning with neural networks. Advances in Neural Information Processing Systems, 4:3104–3112, 2014.
- [31] Simon Thompson. Haskell: the craft of functional programming. Addison-Wesley, 2011.
- [32] Andrew Trask, Felix Hill, Scott E Reed, Jack Rae, Chris Dyer, and Phil Blunsom. Neural arithmetic logic units. Advances in neural information processing systems, 31, 2018.
- [33] Leslie Valiant. What needs to be added to machine learning? In Proceedings of ACM Turing Celebration Conference - China, TURC ’18, page 6, New York, NY, USA, 2018. Association for Computing Machinery.
- [34] Leslie G. Valiant. Three problems in computer science. J. ACM, 50(1):96–99, jan 2003.
- [35] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. Advances in neural information processing systems, 30, 2017.
- [36] Wojciech Zaremba and Ilya Sutskever. Learning to execute. arXiv preprint arXiv:1410.4615, 2014.