In this work, we introduce a new approach how to normalize lambda terms. We have defined and researched two randomized reduction strategies and compared their efficiency with the normal and applicative strategies for uniformly randomly generated lambda terms. In addition, we have developed a framework that allows us to find a randomized reduction strategy that will almost surely be normalized and the efficiency will be no worse than the efficiency of the existing reduction strategies for normalizing the given set of lambda terms. strategy, functional programming lambda-calculus, reduction strategies, uniformly random reduction strategy, mixed reduction 2nd International Workshop of IT-professionals on Artificial Intelligence (ProfIT AI 2022), December 2-4, 2022, Łódź, Poland (G. Zholkevych) ORCID: 0000-0002-3551-6942 (V. Shramenko); 0000-0003-3882-1333 (V. Kuznietcova); 0000-0002-7515-2143 (G. Zholkevych)
1. Introduction terms; • • • • • disadvantages;
Functional programming has its roots in academia, evolving from the lambda calculus, a formal system of computation based only on functions [1]. Functional programming languages use lambda calculus as a low- level programming language.
Functional programming is widely used to solve applied problems of artificial intelligence, such as parallel processing of large data streams [2], modeling of large data arrays [3], big data analysis [4], working with machine learning models [5], decentralized systems and blockchain [6], advanced applications with interactive interfaces [7] and more. Therefore, with the development of the sphere of high-tech information technologies, functional programming becomes relevant not only for solving specialized problems but also for classical projects.
Compilers of functional programming languages perform a reduction process to obtain normal forms of lambda terms. Various reduction strategies differ in the efficiency of the normalizing process. For large programs, the compilation process can take a long time. Thus, there is a desire to optimize the process of normalizing lambda terms.
The object of the study is the process of reducing lambda terms to obtain the normal form of a lambda term.
The subject of the study is lambda term reduction strategies.
The aims of the study: to develop more sophisticated lambda term reduction strategies for normalizing lambda terms; to study the impact of randomness in the process of normalizing randomly generated lambda to develop a framework that searches for a reduction strategy that will find the normal forms of a given class of lambda terms as quickly as possible.
To achieve the aim the following tasks were formulated: to analyze the existing reduction strategies for lambda terms, their advantages and to define a randomized reduction strategy; EMAIL: (V. Shramenko); (V. Kuznietcova);
2022 Copyright for this paper by its authors. , → |( )|( ), where is a metavariable used for referring to elements of and , are lambda terms.
We denote the set of lambda terms as Λ.
Definition 2. The lambda term is called β-reducible term or β-redex if include the term (
) , where , ∈ Λ, ∈ .
We denote the set of β-reducible lambda terms as Λ ⊆ Λ.
Definition 3. We denote the { } as lambda term ∈ Λ that include ∈ Λ. The relation of βreduction → ⊆ Λ → Λ is defined as
→ = {( {( , ) }, { ( ≔ )})| ∈ , , ∈ }.
We denote by ↠ the reflexive and transitive closure of → .
Definition 4. The lambda term is in normal form if does not contain any β-redex, i.e. ∉ Λ . We denote by Λ ⊆ Λ the set of lambda terms that have normal form.
Definition 5. Reduction strategy R is mapping Λ → Λ, that • • • • • to define a uniformly random reduction strategy; to define a mixed reduction strategy; to implement reduction strategies as program code; to find the best reduction strategy for normalizing randomly generated lambda terms; to conduct simulation experiments to compare reduction strategies.
∀ ∈ : ↠ ( ). (4)
We denote the mapping R as → and by ↠ the reflexive and transitive closure of → . 2.2.
A given term can contain several redexes, hence several different β-reductions could be applied. The reduction strategy chooses between different methods of term reduction. Each strategy has its advantages and disadvantages and different computational efficiency. In addition, depending on the (1) (2) (3) lambda term, the efficiency of reduction strategies is different. Also, for some terms, one reduction strategy turns out to be more efficient, and for others, another reduction strategy.
The normalizing process can consist of a different number of steps, depending on the chosen strategy. The main types of reduction strategies are defined below [11].
Definition 6. Reduction strategy R is called one-step strategy, if Otherwise, it is a many-step strategy.
Definition 7. Reduction strategy R is called deterministic strategy, if
∀ ∈ : → ( ). ∀ ∈ ∃ ∈ : ↠ .
(5) (6) Otherwise, it is a nondeterministic strategy.
Definition 8. Reduction strategy R is called normalized strategy, if a lambda term has a normal form, then reduction strategy R will eventually reach it.
∀ ∈ , = , ∉ : ↠ .
(7)
Definition 9. Reduction strategy R is called efficient if ∀ ∈ Λ: → and can be computed in polynomial time.
One-step strategies for term reducing include [12]: • leftmost-innermost (LI): in each step the leftmost of the innermost redexes is reduced, where an innermost redex is a redex not containing any redexes; • leftmost-outermost (LO): in each step, the leftmost of the outermost redexes is reduced, where an outermost redex is a redex not contained in any redex; • rightmost-innermost (RI): in each step, the rightmost of the innermost redexes is reduced, where an innermost redex is a redex not contained in any redexes; • rightmost-outermost (RO): in each step the rightmost of the outermost redexes is reduced, where an outermost redex is a redex not contained in any redex.
Many-step reduction strategies include [12]: • parallel-innermost: reduces all innermost redexes simultaneously. This is well-defined because the redexes are pairwise disjoint; • parallel-outermost: reduces all outermost redexes simultaneously. This is well-defined because the redexes are pairwise disjoint; • Gross-Knuth reduction, also called full substitution or Kleene reduction: all redexes in the term are simultaneously reduced.
The most commonly used reduction strategies in compilers for functional programming languages are LO (Normal order) and RI (Applicative order).
The normal order reduction strategy is normalized which ensures that the normal form can be obtained in a finite number of reductions if it exists. In addition, the LO strategy avoids doing useless work and reduces needed redexes only. Although this strategy reduces the same redexes multiple times, doing duplicating work. For compilers of functional programming languages, the LO strategy turns out to be not optimal in terms of the number of reduction steps.
The applicative order reduction strategy is generally considered more efficient than the LO strategy for compiling functional programs because programs often need to copy their arguments.[13] So, the RI strategy avoids duplicating work and does not reduce the same redexes. However, the RI strategy reduces redexes that will not be included in the resulting reduced lambda term. Also, in contrast to normal order, applicative order reduction may not terminate, even when the term has a normal form.
Definition 10. Let mapping F is the reduction strategy R. Then we denote the function ( ) as the number of reduction steps to obtain the normal form of the term M using the reduction strategy R.
Definition 11. Let F, G are reduction strategies. ≤ if
∀ ∈ : ( )≤ ( ). (8)
Definition 12. Reduction strategy F is called L-optimal if F is normalized strategy and ∄ strategy : ≤ .
There are many various reduction strategies. The question arises as to which reduction strategy to choose in order to get the normal form of the lambda term as quickly as possible. The problem of choosing a redex leading to a minimal-length reduction sequence is undecidable for the lambda calculus. It has been proven that there is no efficient L-optimal strategy and there is an L-optimal strategy [11]. 2.4.
We will measure the efficiency of reduction strategy R as the expected value of a random variable whose values are the outcome of the function of uniformly random generated lambda terms of the same size. We will use the Boltzmann model to uniform generate random lambda terms.
A Boltzmann generator for a class Λ is built according to a recursive specification of the class Λ. The recurrence relation for , (the number of lambda terms of size n with at most m distinct free variables) allows us to define the function generating lambda terms. More precisely, we construct bijections, called unranking functions, between all non-negative integers not greater than , and binary lambda terms of size n with at most m distinct free variables. This approach is known as the recursive method, originating with Nijenhuis and Wil [14].
Using the algorithm for the uniform generation of random lambda terms, described in [14], we generated lambda terms with the number of vertices in the tree representation of lambda terms in the range from 50 to 60. From the generated terms, we select 100 terms that have a normal form. We determine the existence of a normal form using the normal reduction strategy. To do this, we reduce the lambda terms and count the number of reduction steps. If the reduction process is not completed in a limited number of steps, then we will assume that this term does not have a normal form.
Let's denote the set of the generated lambda terms as S.
It is known that there is no strategy that will be optimal for all lambda terms at the same time. However, there is a strategy that is optimal for a certain class of terms. Therefore, there is a desire to look for optimal strategies for a certain class of lambda terms. Thus, the found strategy should quickly normalize the group of terms to the normal form.
A similar situation arises in game theory. Optimal strategies do not always exist among pure strategies. This problem is solved by introducing mixed strategies, we use each pure strategy with some probability. So, there is an element of randomness in the mixed strategy. As a result, it is guaranteed that the player's average payoff will be maximized [15].
Randomized algorithms are algorithms that make random choices during their execution. In practice, a randomized program would use values generated by a random number generator to decide the next step at several branches. Randomized algorithms are typically used to reduce the running time, time complexity; or the memory used, or space complexity, in a standard deterministic algorithm. For many problems, a randomized algorithm is the simplest, the fastest, or both [16].
There are two main types of randomized algorithms: Las Vegas algorithms and Monte-Carlo algorithms. In Las Vegas algorithms, the algorithm may use randomness to speed up the computation, but the algorithm must always return the correct answer to the input. Monte-Carlo algorithms do not have the former restriction, that is, they are allowed to give wrong return values. However, returning a wrong return value must have a small probability, otherwise, the Monte-Carlo algorithm would not be of any use [17].
Adding randomness may improve the efficiency of the lambda-term reduction process. We can also use machine learning or genetic algorithms to match the probabilities of using different reduction strategies for a given class of lambda terms. This will combine the advantages of various reduction strategies in one strategy in the best way.
Definition 13. Random reduction strategy R is mapping (Λ, ℕ) → Λ, that ∀ ∈ , ∈ ℕ:
↠ ( , ).
Definition 14. Let R is the random reduction strategy. Then we denote the function , ( ) as the average of n times calculated the number of reduction steps to obtain the normal form of the term M using the reduction strategy R n times.
∃ ∈ ℝ ∀M ∈ : ( )≥ . where V is extended to partial distribution as follows ( ( ))= ∑ ( )ℙ(
→ ).
∈ 3.2.
The basic QuickSort algorithm has ( 2) running time for an array of n elements when we always choose the leftmost element in the array as the pivot. In the randomized sorting algorithm QuickSort, when we choose a random element in an array as a pivot, we achieve that the expected time of this algorithm is ( log ) [18]. So, we can use randomness in a reduction strategy by reducing an arbitrary redex. The easiest way is to use uniform distribution and select uniformly random redex for reduction from all redexes in the given term.
Definition 15. Uniformly random reduction strategy UR is mapping (Λ, ℕ) → Λ, that R reduces a redex that is uniformly randomly selected from all redexes in the term.
∀ ∈ , ∈ ℕ: → ( , ).
The implementation of the uniformly random reduction strategy consists in: 1. 2. 3.
Count the number of β-redexes in given lambda term. Let's denote the number of redexes by N; Generate а random natural number R in the range [1, N];
Reduce the R-th redex.
The asymptotic of this algorithm is O(V), where V is the number of vertices of the lambda term tree representation. Hence the uniformly random reduction strategy is efficient. 3.3.
Various reduction strategies have their advantages and disadvantages. For different lambda terms, different strategies turn out to be optimal. As in game theory, we can introduce mixed strategies, which means that we use each pure strategy with some probability. This can significantly increase the average rate of reduction of lambda terms from a given set.
Definition 16. Let
= { 1, 2, … , } is set of reduction strategies and = ( 1, 2, … , ) and ∑ =1 = 1. Mixed reduction strategy , is mapping (Λ, ℕ) → Λ, that , is applying one of the reduction strategies from R – to reduce a redex where is the probability to choose from R.
Definition 17. For given reduction strategy define a function : Λ → ℝ as Lyapunov if: (9) (10) (11) (12) (13)
Foster's theorem [19]. If we can define for reduction strategy a Lyapunov function , then is normalized and the average derivation length ∈ : ( )≤ (
is the normal order reduction strategy and > 0. Then, mixed
The LO reduction strategy satisfies the inequality ( ) ≤ ( ), where → . Therefore
( ) ≤ ( ) , ∈ [1, ]. ( )= ∑ ( )= ( ( )− 1)+ ∑ ( )+ ∑ ( )= = ( )− + ( )(1 − )= ( )− . ( )≤ ( )− ⇒ ∃ϵ = > 0: ( )≥ ( , ( ))+ .
So = is Lyapunov function for the given reduction strategy , .
Hence, by the Foster's theorem the mixed reduction strategy , is normalized.
The implementation of the mixed reduction strategy , consists in:
Apply reduction strategy. 1. 3.
Generate а random float number r in the range [0, 1];
2. Find the smallest index i for which ≤ ∑ =1 ;
If all reduction strategies from = { 1, 2, … , } are efficient then the mixed reduction strategy , is also efficient.
The mixed reduction strategy
, involves choosing a probability vector , which is the hyperparameter of the
, reduction strategy. In this regard, the question arises of how to choose a probability vector for the maximum efficiency of reducing lambda terms from S⊆ Λ to normal forms. In this case we need to solve the optimization problem: minimize the sum of the number of required reduction steps for the lambda terms from S by finding the as best as possible probability vector for the reduction strategy , : ( )= ∑ ∈
A common way to find good combinations of hyperparameters is a grid search. The main disadvantage of searching on a grid is the need for a complete enumeration of all combinations, which can take a very long time. Any search on a grid is limited by a subset of hyperparameters that we have defined. The genetic algorithm allows us to find the best combination in less time than in the case of an exhaustive search on the grid. Genetic algorithms can be used not only as an efficient way to search on a grid but also for direct search in the entire parameter space [20].
The basis of genetic algorithms is based on the hypothesis that the optimal solution to a problem can be assembled from small structural elements. Individuals that contain some of the desirable structural elements are assigned a higher score. Repeated operations of selection and crossing lead to the emergence of ever better individuals, passing these structural elements to the next generation, perhaps combined with other successful structural elements. This creates a genetic pressure that di rects the population towards the emergence of an increasing number of individuals with structural elements that form the optimal solution. As a result, each generation is better than the previous one and contains more individuals close to the optimal solution.
Consider mixed reduction strategy { ,RI,}, , = ( , ) is probability vector, where = 1 − . For various values ∈ [0, 1], we calculate the efficiency of the obtained reduction strategies { ,RI,}, . The results are shown in Fig. 1, which shows the dependence of the efficiency of the mixed reduction strategy { ,RI,}, on the probability of using the normal strategy . { ,RI}, on the probability
As seen from the figure 1, the most optimal values of the probabilities of using normal and applicative strategies of the mixed reduction strategy { ,RI}, are { = 0.85 = 0.15 for normalizing uniformly random generated lambda terms.
The expected value of reduction steps number to normalize the uniformly random generated lambda term:
{ , },(0.85,0.15) = 8.45.
The expected value of this distribution is ( , , )=
1 √2 2 − ( 1 ln( )− )2
= + 22 = 9.14.
In addition, the mixed reduction strategy
{ ,RI},(0.85,0.15) is almost surely normalized by Theorem 1. Thus, we have found a mixed reduction strategy that is more efficient than applicative and normal reduction strategies for normalizing uniformly random generated lambada terms, and it is almost surely normalized.
Consider mixed reduction strategy 5 { ,RI,LI,RO, }, , where = ( 1, 2, 3, p4, p5) and ∑ =1 = 1.
We used a genetic algorithm to find the best as possible probability vector . We defined an individual as a list of decimal numbers that will be the desired probability vector. The fitness function for an individual p was the efficiency criterion of the mixed strategy which was described in section 2.4. As a genetic selection, crossover, and mutation operator, we used tournament selection of size 2 in combination with elitism [21], Simulated Binary Crossover [22], and Polynomial Bounded Mutation [23], respectively.
As the result, we found the probability vector
= (0.72, 0.02, 0.02, 0.17, 0.7).
Let's denote the obtained mixed strategy { ,RI,LI,RO, }, as opt.
The mixed reduction strategy
opt is almost surely normalized by Theorem 1.
We can generalize this algorithm to an arbitrary set R of reduction strategies. Thus, we have developed a framework that allows us to find the mixed reduction strategy that will normalize a given class of lambda terms with almost the greatest efficiency. In addition, if our mixed strategy is using the normal strategy with non-zero probability then it is almost surely normalized for lambda terms having a normal form. 3.4.
We want to compare the efficiency of the most common reduction strategies LO (normal order) and RI (applicative order) with UR (uniformly random) and opt (mixed strategy obtained in the previous section) reduction strategies for uniformly random generated lambda terms.
Based on the generated lambda terms S in section 1.4, we construct histograms of the distributions of the required number of reduction steps to obtain the normal form by using LO, RI, UR, and opt reduction strategies respectively (Fig. 2-5).
Hypotheses about the laws of distribution of the values of the functions , , ,100 and
{ ,RI,LI,RO, }, ,100 for uniformly random generated lambda terms from S are checked. The following distribution laws were taken for comparison: normal, Cauchy, 2, exponential, generalized normal (exponential power), gamma, log-normal and Rayleigh. Graphs of distribution laws that best describe the values of the functions , , ,100 and opt,100 for lambda terms from S are shown on Fig. 25.
It is determined that the values of the functions of the uniform generated lambda terms is distributed according to the log-normal distribution law with the = 1.65, = 1.06 parameters: (16) (17) (18) (19)
It is determined that the values of the functions of the uniformly random generated lambda terms is distributed according to the log-normal distribution law with the = 2.04, = 0.68 parameters of (18). The expected value of this distribution is (20)
In addition, the 4 lambda terms were not normalized, although they have a normal form. The use of the applicative strategy for these terms turned out to be incessant. It is determined that the values of the functions ,100 of the uniformly random generated lambda terms is distributed according to the lognormal distribution law with the = 1.92, = 0.8 parameters of (18). The expected value of this distribution is . for uniform generated lambda terms of the same size.
We can see that the efficiency of the uniformly random reduction strategy is commensurate with the efficiency of normal and applicative strategies. Thus, the uniformly random strategy can be used for the lambda term reduction process the same as the normal or applicative strategies.
The mixed strategy turned out to be the worst among the considered strategies. In addition, the opt strategy is almost surely normalized and all lambda terms were normalized by using this strategy.
There is no universal strategy that has been the most efficient for reducing any lambda term. All existing reduction strategies have various advantages and disadvantages. The efficiency of reduction strategies essentially depends on the lambda terms for which it is used.
We defined a randomized reduction strategy for lambda terms. Two randomized reduction strategies have been defined and implemented as a program code: a uniformly random and a mixed reduction strategy.
A mixed reduction strategy is investigated. It is proved that a mixed reduction strategy for which the normal strategy is used with a probability greater than 0 is almost surely normalized.
A framework has been developed that allows us to find a mixed reduction strategy that will almost surely be normalized and the efficiency will be no worse than the efficiency of the existing reduction strategies for normalizing the existing class of lambda terms.
Simulation experiments to normalize uniformly random generated lambda terms using the mixed, uniformly random, normal, and applicative reduction strategies have been conducted.
The uniformly random reduction strategy is proposed for use since it is comparable in efficiency with the normal and applicative strategies. Also, the uniformly random reduction strategy turned out to be better than the applicative one in terms of the number of normalized lambda terms.
The efficiency of the mixed reduction strategy is significantly better than the efficiency of the other considered reduction strategies for normalizing randomly generated lambda terms. The mixed reduction strategy combines the advantages of several reduction strategies in the best way.
To sum up, randomized reduction strategies may be more efficient than standard non-randomized reduction strategies.
[1] Z. Hu, J. Hughes, and M. Wang, “How functional programming mattered,” National Science
Review, vol. 2, no. 3, pp. 349–370, Sep. 2015, doi: 10.1093/nsr/nwv042. [2] J. Arora, S. Westrick, and U. A. Acar, “Provably space-efficient parallel functional programming,” Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, pp. 1–33, Jan. 2021, doi: 10.1145/3434299. [3] K. Bazilevych, et. al., “stochastic modelling of cash flow for personal insurance fund using the cloud data storage,” International Journal of Computing, vol. 17, no. 3, pp. 153–162, Sep. 2018, doi: 10.47839/ijc.17.3.1035. [4] L. Belcastro, R. Cantini, F. Marozzo, A. Orsino, D. Talia, and P. Trunfio, “Programming big data analysis: principles and solutions,” Journal of Big Data, vol. 9, no. 1, Jan. 2022, doi: 10.1186/s40537-021-00555-2. [5] D. Chumachenko, et al., “Investigation of Statistical Machine Learning Models for COVID-19 Epidemic Process Simulation: Random Forest, K-Nearest Neighbors, Gradient Boosting,” Computation, vol. 10, no. 6, 86, 2022, doi: 10.3390/computation10060086. [6] Q. Pan and X. Koutsoukos, “Building a Blockchain Simulation using the Idris Programming Language,” Proceedings of the 2019 ACM Southeast Conference, Apr. 2019, doi: 10.1145/3299815.3314456. [7] S. Yakovlev et al., “The Concept of Developing a Decision Support System for the Epidemic
Morbidity Control.” CEUR Workshop Proceedings, vol. 2753, pp. 265-274, 2022. [8] S. L. Peyton Jones, “Parallel Implementations of Functional Programming Languages,” The
Computer Journal, vol. 32, no. 2, pp. 175–186, 1989, doi: 10.1093/comjnl/32.2.175. [9] P. Sestoft, “Demonstrating Lambda Calculus Reduction,” Electronic Notes in Theoretical
Computer Science, vol. 45, pp. 424–432, 2001, doi: 10.1016/s1571-0661(04)80973-3. [10] D. Wright, “Reduction Types and Intensionality in the Lambda-Calculus,” 1992. [11] E. Engeler, “H. P. Barendregt. The lambda calculus. Its syntax and semantics. Studies in logic and foundations of mathematics” Journal of Symbolic Logic, vol. 49, no. 1, pp. 301–303, 1984, doi: 10.2307/2274112. [12] J. Klop, “Term Rewriting Systems.” 2021, 77 p. [13] G. Mazzola, G. Milmeister, and J. Weissmann, Comprehensive Mathematics for Computer Scientists 2: Calculus and ODEs, Splines, Probability, Fourier and Wavelet Theory, Fractals and Neural Networks, Categories and Lambda Calculus. Springer Science & Business Media, 2004. [14] K. Grygiel, P. Lescanne, “Counting and Generating Terms in the Binary Lambda Calculus (Extended version) Counting and Generating Terms in the Binary Lambda Calculus (Extended version),” 2015. [15] S. Tadelis, Game Theory. 2013. [16] M. Mitzenmacher and E. Upfal, “Probability and Computing: Randomized Algorithms and
Probabilistic Analysis,” undefined, 2005. [17] D. Fucci et al., “A Longitudinal Cohort Study on the Retainment of Test-Driven Development” [18] H. J. Karloff and P. Raghavan, “Randomized algorithms and pseudorandom numbers,” Journal of the ACM, vol. 40, no. 3, pp. 454–476, 1993, doi: 10.1145/174130.174132. [19] P. Bremaud, “Markov chains”, 1999. [20] Eyal Wirsansky, Hands-on genetic algorithms with Python : applying genetic algorithms to solve real-world deep learning and artificial intelligence problems / Eyal Wirsansky. Birmingham, Uk: Packt Publishing Ltd, 2020. [21] M. Yusoff and A. A. Othman, “Genetic Algorithm with Elitist-Tournament for Clashes-Free Slots of Lecturer Timetabling Problem,” Indonesian Journal of Electrical Engineering and Computer Science, vol. 12, no. 1, p. 303, 2018, doi: 10.11591/ijeecs.v12.i1.pp303-309. [22] K. Deb and R. B. Agrawal, “Simulated Binary Crossover for Continuous Search Space Kalya nmoy
D eb’ Ram B hushan A gr awal,” 2014. [23] K. Deb and ayan Deb, “Analysing mutation schemes for real-parameter genetic algorithms,” International Journal of Artificial Intelligence and Soft Computing, vol. 4, no. 1, p. 1, 2014, doi: 10.1504/ijaisc.2014.059280.