Харківський національний університет імені В. Н. Каразіна  

Міністерство освіти і науки України 

 

Кваліфікаційна наукова праця 

На правах рукопису 

 

 

 

ДЕЙНЕГА ОЛЕКСАНДР АНДРІЙОВИЧ 

УДК 004.4`6:004.4`4 

 

ДИСЕРТАЦІЯ 

 

ОПТИМІЗАЦІЯ ФУНКЦІОНАЛЬНИХ МОВ ПРОГРАМУВАННЯ НА ОСНОВІ 

МЕТОДІВ ШТУЧНОГО ІНТЕЛЕКТУ 

 

 

Спеціальність 122 – Комп’ютерні науки 

Галузь знань 12 – Інформаційні технології 

 

Подається на здобуття ступеня доктора філософії 

Дисертація містить результати власних досліджень. Використання ідей, результатів 
і текстів інших авторів мають посилання на відповідне джерело.  
______________________ О. А. Дейнега 
 

Науковий керівник: Жолткевич Григорій Миколайович доктор технічних наук, 

професор  

 

 

Харків – 2024  



 
 

2 

АНОТАЦІЯ 

 

Дейнега О. А. Оптимізація функціональних мов програмування на 

основі методів штучного інтелекту. – Кваліфікаційна наукова праця на правах 

рукопису. 

Дисертація на здобуття ступеня доктора філософії за спеціальністю 122 – 

Комп’ютерні науки (Галузь знань 12 – Інформаційні технології). – Харківський 

національний університет імені В. Н. Каразіна, Міністерства освіти і науки 

України, Харків, 2024. 

Дисертація присвячена оптимізації функціональних мов програмування, на 

основі методів штучного інтелекту, що є складною та важливою задачею з багатьма 

проблемами та викликами. В дисертації розглянуто лямбда-числення як приклад 

відносно простої репрезентації функціональних мов програмування, що дозволяє 

показати процеси компіляції та інтерпретації функціональних мов програмування 

шляхом редукції лямбда-термів. 

У першому розділі описано теоретичну частину дослідження. Представлено 

функціональні мови програмування, як інструмент верифікації програмного 

забезпечення. Описано переваги функціональних програм, такі як простота 

тестування та надійність коду, а також їх недоліки, основним з яких є низька 

продуктивність. Далі постає описання лямбда-числення, як одного з найпростіших 

варіантів представлення функціональних мов програмування. Пояснюється 

можливість переходу від роботи з функціональними мовами програмування до 

лямбда-числення. Далі представлені підходи для оптимізації лямбда-числення, 

основним із яких є удосконалення стратегій редукції лямбда-термів. 

Далі текст заглиблюється в зв’язок між лямбда-численням і верифікацією 

програм в контексті паралельного програмування. Підкреслюється, як лямбда-

числення служить основою для аналізу та розуміння поведінки паралельних 

програм. Використовуючи властивості лямбда-числення, розробники можуть 

застосовувати формальні методи перевірки, щоб переконатися, що паралельні 



 
 

3 

програми виконуються правильно та відповідають призначеним специфікаціям. Це 

включає перевірку таких властивостей, як безпека, живучість і правильність у 

різних сценаріях виконання. 

Описано важливість формальної перевірки для паралельних програм, 

особливо з огляду на потенційні складності та проблеми, пов’язані з одночасним 

виконанням. Використовуючи формальні методи, засновані на лямбда-численні, 

розробники можуть отримати впевненість у надійності та правильності свого 

паралельного програмного забезпечення. 

Далі у першому розділі розглянуті бібліотеки Python для роботи з лямбда 

численням, виведені їх недоліки та для усунення виявлених недоліків розроблено 

власну бібліотеку Lambda Calculus Environment. Показано класову архітектуру 

розробленої бібліотеки та зазначено функції, що виконують зазначені класи. Також 

зазначено вимоги яким задовольняє розроблена бібліотека і вимоги до 

функціонування розробленого програмного забезпечення. Згідного вимог до 

розробленого програмного забезпечення визначено багатоетапну процедуру 

верифікації. Процедура визначає певний набір лямбда-термів із ключовими 

умовами які мають бути виконані й враховані при виконанні на них доступних 

операції. Також процедура визначає перевірку виконання кожного із зазначених 

пунктів при додаванні нового функціоналу, та перевизначення множини лямбда-

термів для тестування.  

У другому розділі представлений підхід до оптимізації стратегій редукції, 

що базується на змішуванні стратегій та використанні рандомізованих стратегій. 

Ідея даного підходу відноситься до теорії ігор, де в деяких випадках використання 

стратегій в чистому вигляді не може призвести до перемоги. Описані результати, 

що показують ефективність даного підходу, та можливість заміни чистих стратегій 

змішаними, що дозволяють зберегти існуючу продуктивність, проте підвищити 

загальну вірогідність успішного редукування термів.  

Далі у розділі була розглянута концепція обчислювальної нерівнозначності 

редексів лямбда-термів, що є ключовими точками у виборі стратегії редукції. 



 
 

4 

Нерівнозначність була оцінена з використанням методів машинного навчання для 

вирішення задачі регресії. Ціллю регресії була оцінка часу виконання операції 

редукції для даного редексу по параметрам терму, що відображають його деревну 

структуру. В результаті було отримано відхилення від очікуваного логарифму часу 

в 0.28 для регресійної моделі на базі штучної нейронної мережі та в 0.28 для 

лінійної регресії, варто зазначити також незначне падіння точності на тестовому 

наборі, що свідчило про достатню спроможність зазначених методів вилучати 

необхідні характеристики для оцінки часу редукції. Застосування методів дерев 

рішень та опорних векторів для вирішення цієї задачі також не показали високих 

результатів точності. 

Далі у розділі розглядається використання даних про стан терму до і після 

процесу редукції для оцінки часу, проте без значних покращень у підвищенні 

точності оцінки часу редукції. Показано, що подальші дослідження цих аспектів 

можуть збільшити точність оцінки обчислювальних витрат. Також показано, що 

точна оцінка обчислювальних витрат може допомогти розробити жадібну 

стратегію з мінімізацію витраченого часу на процес редукції проте без урахування 

кількості кроків редукції. 

У третьому розділі була перевірена можливість оцінки кількості кроків 

редукції лямбда-термів за заданою стратегією із застосуванням методів глибинного 

навчання. Для цього було використано спрощене текстове представлення лямбда 

термів із видаленням інформації про змінні. Аналіз проводився з використанням 

методів глибинного навчання для аналізу послідовностей. Показано, що точних 

результатів оцінки можливо досягти при визначенні 0-2 кроків редукції проте із 

збільшенням очікуваних кроків редукції зростала помилка в оцінці. Це свідчило 

про втрату важливої інформації при використанні спрощеного представлення 

лямбда-термів та недостатньої спроможності використаних моделей до глибинного 

аналізу термів. 

Далі було досліджено можливість використання вбудовувань для 

репрезентації різниці в редукції лямбда термів різними стратегіями. Для цього було 



 
 

5 

розглянуто чотири моделі LLM для генерації вбудовувань з текстових представлень 

лямбда-термів. Це дозволяє проаналізувати можливість використання вбудовувань, 

отриманих з LLM, для вилучення характеристик, що впливають на редукцію термів 

та в перспективі можуть допомогти розробити компілятори та інтерпретатори 

функціональних мов програмування.  

Згенеровані вбудовування були використані для створення восьми наборів 

даних для кожної розглянутої моделі LLM та для стратегій редукції термів LO та 

RI. Ці набори даних містять вбудовування по обраній LLM та кількість кроків 

редукції для кожного з розглянутих термів за обраною стратегією редукції. Для 

оцінки якості репрезентації інформації у вбудовуваннях були використані моделі 

ШНМ, що вирішували проблему класифікації відносно кроків редукції від 0 до 30.  

Далі навчені моделі ШНМ були оцінені з показниками для оцінки точності 

регресії MAE, RMSE. Ці коефіцієнти було порівняно з найкращими результатами, 

досягнутими для того самого завдання та набору даних зі спрощеним 

представлення термів. Результати вказують на покращення прогнозування 

кількості кроків, особливо значних покращень було досягнуто в прогнозуванні 

кількості кроків LO, що збільшило точність на 23% для показника MAE та на 30% 

для показника RMSE. Проте прогнози щодо кількості кроків для стратегії RI мали 

незмінно низький рівень помилок із незначними покращеннями показників MAE та 

RMSE. Такі результати вказують на те, що код і загальні LLM можуть допомогти 

отримати інформацію з лямбда-термів і використовувати цю інформацію для 

вибору оптимальної стратегії редукції. Спеціально навчені LLM можуть ще більше 

підвищити точність вилучення даних із лямбда-термів. Отже, метод вилучення 

ознак із використанням LLM може бути реалізований в реальних інтерпретаторах 

функціональних мов програмування, а вилучені дані можуть бути використані для 

оптимізації. 

У четвертому розділі лямбда-терми були перетворені в усереднені вектори 

вбудовувань розміром 768, що були отримані в результаті застосування 

попередньонавченої моделі ШНМ для задач пов’язаних із аналізом програмного 



 
 

6 

коду Microsoft CodeBERT та подальшої обробки виходів середніх рівнів цієї моделі 

за принципом об’єднання слів у значущі вектори Word2Vec. Завдяки аналізу PCA 

та t-SNE візуалізацій цих усереднених векторних вбудовувань виявлено, що 

представлення лямбда-термів у цих усереднених вбудовуваннях можливо 

візуально чітко розрізнити. Це дозволило підтвердити гіпотезу можливості 

виділення значущих кластерів в цьому наборі вбудовувань. Також виходи 

CodeBERT моделі були оброблені із застосуванням автокодувальника проте це не 

дало бажаної точності візуального розділення даних. 

Тому далі було досліджене формування кластерів даних із застосуванням 

методу DBSCAN, що використовує як евклідову, так і косинусну метрику, окрім 

методу агломеративної кластеризації з використанням евклідової, косинусної, L1 і 

L2 метрики. Ці зусилля з кластеризації підкреслили ефективність моделі CodeBERT 

у вилученні значущих характеристик із лямбда-термів. Незважаючи на це, 

універсальність Microsoft CodeBERT, навченого різними мовами програмування, 

вносить рівень складності в досягнення точного представлення термів лямбда-

числення в матрицях вбудовувань. Ця складність поширюється на процес 

перетворення цих матриць у зрозумілі усереднені вбудовування або вектори 

прихованого простору, особливо при використанні автокодувальників. 

Далі була оцінена інформативність змінних усереднених вбудовувань із 

застосуванням моделі ШНМ навченої на результатах кластеризації та градієнтного 

методу оцінки інформативності моделі ШНМ. Цей аналіз дозволяє краще зрозуміти 

вплив певних змінних на результати кластеризації, пропонуючи пояснення 

основного значення цих змінних у контексті лямбда-термів і мінливості результатів 

кластеризації. 

Крім того, далі було запроваджено коефіцієнт перекриття, що полегшило 

оцінку взаємозалежності між кластерами та застосованими стратегіями. Ця оцінка 

виявила відсутність кореляції між попередньо визначеними пріоритетами стратегії 

та фактично досягнутою дискримінацією термів, що вказує на потенційну потребу 



 
 

7 

в тонкому налаштуванні моделі CodeBERT та вказує на необхідність розгляду 

альтернативних моделей, більш придатних для аналізу даних у цій області. 

Також було продовжено ідею трансформації лямбда-термів у вектори 

вбудовувань з використанням моделей OpenAI з розміром векторів 1536, та 3072. 

Дані вектори були так само проаналізовані з застосуванням методів PCA та t-SNE 

для візуалізації цих векторів. Так само було виявлено можливість візуального 

розділення цих даних. Далі також було розглянуто формування кластерів даних із 

застосуванням методу DBSCAN з евклідовою метрикою. Також підкреслено 

здатність моделей OpenAI Embeddings вилучати важливі характеристики з лямбда-

термів. Однак, навчання OpenAI Embeddings моделей проводилось не на 

представленнях лямбда-термів, а здебільшого на людському тексті та коді, що 

ускладнило точне зображення термів лямбда-числення в матрицях вбудовування. 

В наступній частині четвертого розділу представлено підхід для 

використання LLM безпосередньо для проведення процесу редукції лямбда-термів. 

В даному підході на вхід моделі подаються лямбда-терм, а на виході очікується 

наступний крок редукції лямбда терму за обраною стратегію. Результати показали, 

що використання LLM для вирішення цієї задачі не є достатньо ефективним.  

В останньому розділі дисертації представлено можливий варіант 

імплементації описаних методів для використання у компіляторах для підвищення 

їх продуктивності. Описано можливі ризики, що мають бути враховані при 

використанні даного підходу. Також у даній частині представлено варіант 

використання великих мовних моделей у якості засобу верифікації лямбда-термів, 

та функціональних програм в цілому. Оскільки великі мовні моделі мають великий 

потенціал з точки зору аналізу коду та можуть бути розвинені для забезпечення 

його надійності.   

Сукупність результатів, викладених у дисертації, разом із підтвердженою 

науковою та практичною актуальністю демонструють досягнення поставленої мети 

щодо оптимізації функціональних мов програмування на базі методів штучного 

інтелекту. Цей успіх пояснюється впровадженням сучасних моделей і методів 



 
 

8 

машинного навчання та штучного інтелекту, що показали високі результати у 

вирішенні задач даного класу. Крім того, наукові та практичні результати, 

представлені в дисертації, у поєднанні з перевіркою їх достовірності та значущості, 

демонструють, що проблема оптимізації функціональних програм за допомогою 

методів штучного інтелекту була ефективно вирішена, і поставлена мета була 

досягнута. 

Ключові слова: штучний інтелект, великі мовні моделі, кластеризація, 

глибинне навчання, інформативність характеристик, машинне навчання, нейронні 

мережі, профілювання процесу редукції, графове представлення, моделювання 

лямбда-числення, функціональні мови програмування, автоматизація вибору 

стратегії редукції, симуляція процесу редукції, верифікація програмного 

забезпечення. 

  



 
 

9 

ABSTRACT 

 

Deineha O. A. Optimization of functional programming languages based on 

artificial intelligence methods. – Qualification scholarly paper: a manuscript. 

The dissertation submitted for obtaining the Doctor of Philosophy degree in 

Technical Science: Speciality 122 – Computer science. V. N Karazin Kharkiv National 

University, Ministry of Education and Science of Ukraine, Kharkiv, 2023. 

The dissertation is devoted to the optimization of functional programming 

languages based on artificial intelligence methods, which is a complex and important task 

with many problems and challenges. The thesis examines lambda calculus as an example 

of a relatively simple representation of functional programming languages, which allows 

us to show the processes of compilation and interpretation of functional programming 

languages by reducing lambda terms. 

The first chapter describes the theoretical part of the research. Functional 

programming languages are presented as an effective tool for solving many problems 

including program verification. The advantages of functional programs, such as ease of 

testing and code reliability, are described, as well as their disadvantages, the main of 

which is low performance. Next comes the description of lambda calculus, as one of the 

simplest options for representing functional programming languages. The possibility of 

transition from working with functional programming languages to lambda calculus is 

explained. Next, approaches for optimizing the lambda calculus are presented, the main 

of which is the improvement of strategies for the reduction of lambda terms. 

Later in this section, the text delves into the connection between lambda calculus 

and program verification in the context of parallel programming. It highlights how lambda 

calculus serves as a foundation for analyzing and understanding the behavior of parallel 

programs. By leveraging the properties of lambda calculus, developers can apply formal 

verification techniques to ensure that parallel programs execute correctly and adhere to 

their intended specifications. This includes verifying properties such as safety, liveness, 

and correctness in various execution scenarios. 



 
 

10 

 

The section emphasizes the importance of formal verification for parallel programs, 

especially given the potential complexities and challenges associated with concurrent 

execution. By using formal methods based on lambda calculus, developers can gain 

confidence in the reliability and correctness of their parallel software. 

Further, in the first chapter, the Python libraries for working with lambda calculus 

are considered, their shortcomings are deduced, and Lambda Calculus Environment 

library was developed to eliminate the identified shortcomings. The class architecture of 

the developed library is shown and the functions performed by the specified classes are 

indicated. The requirements that the developed library satisfies are also indicated and the 

functioning requirements for the developed software are also indicated. According to the 

functioning requirements, a multi-stage verification procedure is defined. The procedure 

defines a certain set of lambda terms with key conditions that must be fulfilled and 

considered when performing available operations on them. Also, the procedure 

determines the verification of each execution of each of the specified points when adding 

new functionality, and the redefinition of a lambda terms set for testing. 

The second chapter presents an approach to optimization of reduction strategies 

based on mixing strategies and using randomized strategies. The idea of this approach 

refers to the theory of games, where in some cases the use of strategies in their pure form 

cannot lead to victory. The results are described, showing the effectiveness of this 

approach and the possibility of replacing pure strategies with mixed ones, which allow 

maintaining the existing performance, but increasing the overall probability of successful 

term reduction. 

Further in the section, the concept of computational inequality of lambda-term 

redexes, which are key points in choosing a reduction strategy, was considered. The 

disparity was estimated using machine learning techniques to solve the regression 

problem. The purpose of the regression was to estimate the time of the reduction operation 

for a given redex based on the parameters of the term reflecting its tree structure. As a 

result, a deviation from the expected logarithm of time was obtained in 0.28 for the 



 
 

11 

regression model based on an artificial neural network and 0.28 for linear regression, it is 

also worth noting a slight drop in accuracy on the test set, which indicated the sufficient 

ability of the specified methods to extract the necessary characteristics for estimating the 

reduction time. The use of decision tree and support vector methods to solve this problem 

also did not show high accuracy results. 

Next, the section examines the use of term state data before and after the reduction 

process to estimate the time, but without significant improvements in the accuracy of the 

reduction time estimate. It is shown that further studies of these aspects can further 

increase the accuracy of the estimation of computational costs. It is also shown that an 

accurate estimate of the computational cost can help to develop a greedy strategy to 

minimize the time spent on the reduction process, however, regardless of the reduction 

steps number. 

In the third chapter, the possibility of estimating the number of lambda term 

reduction steps according to a given strategy using deep learning methods was tested. For 

this, a simplified textual representation of lambda terms was used, with information about 

variables removed. The analysis was carried out using deep learning methods for 

sequence analysis. It is shown that accurate estimation results can be achieved when 

determining 0–2 reduction steps, however, with the increase of the expected reduction 

steps, the error in the estimation increased. This indicated the loss of important 

information when using a simplified representation of lambda terms and the insufficient 

capacity of the used models for in-depth analysis of terms. 

Next, the possibility of using embeddings to represent the difference in the 

reduction of lambda terms by different strategies was investigated. For this, four LLM 

models were considered for generating embeddings from text representations of lambda 

terms. This allows us to analyze the possibility of using the embeddings obtained from 

LLM to extract characteristics that affect the reduction of terms and in the future can help 

to develop compilers and interpreters of functional programming languages. 

The generated embeddings were used to generate eight datasets for each LLM 

model considered and for the LO and RI term reduction strategies. These datasets contain 



 
 

12 

observations on the selected LLM and the number of reduction steps for each of the 

considered terms on the selected reduction strategy. ANN models were used to assess the 

quality of information representation in embeddings, which solved the classification 

problem with respect to reduction steps from 0 to 30. 

Next, the trained ANN models were evaluated with indicators for assessing the 

accuracy of regression MAE, RMSE. These coefficients were compared with the best 

results achieved for the same task and data set with a simplified term representation. The 

results indicate an improvement in step count prediction, particularly significant 

improvements were achieved in LO step count prediction, which increased the accurate 

by 23% for the MAE indicator and by 30% for the RMSE indicator. However, the number 

of step predictions for the RI strategy had consistently low error rates, with slight 

improvements in MAE and RMSE. Such results indicate that the code and general LLMs 

can help extract information from lambda terms and use this information to select an 

optimal reduction strategy. Specially trained LLMs can further improve the accuracy of 

data extraction from lambda terms. Therefore, the feature extraction method using LLM 

can be implemented in real interpreters of functional programming languages, and the 

extracted data can be used for optimization. 

In the fourth chapter, lambda terms were transformed into averaged embedding 

vectors of size 768, which were obtained as a result of applying a pre-trained ANN model 

for tasks related to the analysis of Microsoft CodeBERT software code and further 

processing of the outputs of the average levels of this model according to the principle of 

combining words in significant Word2Vec vectors. Through PCA and t-SNE analysis of 

visualizations of these averaged vector embeddings, it is found that the representation of 

lambda terms in these averaged embeddings can be visually clearly distinguished. This 

made it possible to confirm the hypothesis of the possibility of identifying significant 

clusters in this set of embeddings. Also, the outputs of the CodeBERT model were 

processed using an autoencoder, which did not give the desired accuracy of visual data 

separation. 



 
 

13 

Therefore, the formation of data clusters using the DBSCAN method using both 

Euclidean and cosine metrics, in addition to the agglomerative clustering method using 

Euclidean, cosine, L1 and L2 metrics, was further investigated. This clustering effort 

highlighted the effectiveness of the CodeBERT model in extracting meaningful features 

from lambda terms. Despite this, the versatility of Microsoft CodeBERT, trained in 

various programming languages, introduces a level of complexity in achieving an 

accurate representation of lambda calculus terms in embedding matrices. This complexity 

extends to the process of transforming these matrices into understandable averaged 

embeddings or hidden space vectors, especially when using autoencoders. 

Next, the informativeness of the averaged embedding variables was evaluated using 

the ANN model trained on the results of clustering and the gradient method of assessing 

the informativeness of the ANN model. This analysis provides a better understanding of 

the effect of certain variables on the clustering results by offering an explanation of the 

underlying meaning of these variables in the context of lambda terms and the variability 

of the clustering results. 

In addition, an overlap coefficient was further introduced, which facilitated the 

assessment of interdependence between clusters and applied strategies. This evaluation 

found no correlation between the predefined strategy priorities and actual term 

discrimination achieved, indicating a potential need for fine-tuning of the CodeBERT 

model and indicating the need to consider alternative models more suitable for data 

analysis in this area. 

The idea of transforming lambda terms into embedding vectors was also continued 

using OpenAI models with vector sizes of 1536 and 3072. These vectors were also 

analyzed using PCA and t-SNE methods to visualize these vectors. The possibility of 

visual separation of these data was also discovered. Further, the formation of data clusters 

using the DBSCAN method with the Euclidean metric was also considered. The ability 

of OpenAI Embeddings models to extract important features from lambda terms is also 

highlighted. However, OpenAI Embeddings models were not trained on representations 



 
 

14 

of lambda terms, but mostly on human text and code, which made it difficult to accurately 

represent lambda terms in embedding matrices. 

The next part of the fourth chapter presents an approach for using the LLM directly 

to perform the lambda term reduction process. In this approach, lambda terms are fed to 

the input of the model, and the next step of lambda term reduction according to the chosen 

strategy is expected at the output. The results showed that using LLM to solve this 

problem is not efficient enough. 

The last chapter of the dissertation presents a possible implementation option. 

Possible risks that must be taken into account when using this approach are described. 

Also, this part presents the option of using large language models with full verification of 

lambda terms and functional programs in general. Because large language models have 

great potential in terms of code analysis and can be developed to ensure its reliability. 

The set of results presented in the dissertation, together with the confirmed 

scientific and practical relevance, demonstrate the achievement of the set goal of 

optimizing functional programming languages based on artificial intelligence methods. 

The success is explained by the implementation of modern models and methods of 

machine learning and AI, which has shown its success in solving the tasks of this class. 

In addition, the scientific and practical results presented in the thesis, combined with the 

verification of their reliability and significance, demonstrate that the problem of 

optimizing functional programs using artificial intelligence methods was effectively 

solved, and the goal was achieved. 

Keywords: artificial intelligence, LLMs, clustering, deep learning, informativeness 

of features, machine learning, neural networks, profiling of reduction process, graph 

representation, lambda-calculus simulation, functional programming languages, 

automation of reduction strategy selection, simulation of reduction process, verification 

of programs.  



 
 

15 

СПИСОК ПУБЛІКАЦІЙ ЗДОБУВАЧА ЗА ТЕМОЮ ДИСЕРТАЦІЇ 

 

Статті у наукових фахових виданнях,  

що входять до міжнародних наукометричних баз 

1. Deineha, O., Donets, V., & Zholtkevych, G. (2024). The approach development 

of data extraction from lambda terms. Eastern-European Journal of Enterprise 

Technologies. 

(Особистий внесок здобувача: розробка основних ідей підходу екстракції 

даних з лямбда термів, проведення експериментів, написання частини тексту та 

його переклад.  

Особистий внесок Volodymyr Donets проведення експериментів та аналіз 

підходу екстракції даних з лямбда термів, написання частини тексту та його 

переклад. 

Особистий внесок Grygoriy Zholtkevych розробка основних ідей підходу та 

концепції дослідження, аналіз отриманих результатів.) 

2. Deineha, O. (2024). Supervised data extraction from transformer representation 

of Lambda-terms. Radioelectronic and Computer Systems, 2024(2), 19-29. 

(Особистий внесок: розробка ідей підходу екстракції даних з лямбда термів, 

дослідження існуючих моделей трансформерів, проведення експериментів, аналіз 

отриманих результатів, написання тексту та його переклад) 

Статті у наукових фахових виданнях України 

3. Deineha O. The Clustering of Lambda Terms by Using Embeddings. Вісник 

Харківського національного університету імені В.Н. Каразіна, сер. «Математичне 

моделювання. Інформаційні технології. Автоматизовані системи управління». 

2023. вип. 59. С.16-23. 

(Особистий внесок здобувача: аналіз підходів кластеризації лямбда термів 

за допомогою вбудовувань, проведення експериментів, дослідження типів 

вбудовувань, написання тексту та його переклад). 



 
 

16 

4. Deineha, O. (2024). Lambda calculus term reduction: Evaluating LLMS’ 

predictive capabilities. Information Technology and Society, 1(12), 51-55. 

 (Особистий внесок: розробка та дослідження підходів оцінки прогнозивних 

здатностей LLM в розрізі роботи за лямбда-численням, аналіз існуючих моделей, 

написання тексту та його переклад).  

 

Наукові праці, які засвідчують апробацію матеріалів дисертації: 

5. Deineha, O., Donets, V., Zholtkevych, G. (2023). On Randomization of 

Reduction Strategies for Typeless Lambda Calculus. In: Antoniou, G., et al. Information 

and Communication Technologies in Education, Research, and Industrial Applications. 

ICTERI 2023. Communications in Computer and Information Science, vol 1980. 

Springer, Cham. (Scopus) 

6. Deineha, O., Donets, V., & Zholtkevych, G. (2023). Estimating Lambda-Term 

Reduction Complexity with Regression Methods. International Conference "Information 

Technology and Interactions". (Scopus) 

7. Deineha, O., Donets, V., & Zholtkevych, G. (2023). Deep Learning Models for 

Estimating Number of Lambda-Term Reduction Steps. International Workshop of IT-

professionals on Artificial Intelligence. (Scopus) 

 

  



 
 

17 

ЗМІСТ 

 

ПЕРЕЛІК УМОВНИХ ПОЗНАЧЕНЬ 19 

ВСТУП 21 

РОЗДІЛ 1. БЕЗТИПОВЕ ЛЯМБДА ЧИСЛЕННЯ 31 

1.1. Функціональне програмування 31 

1.2. Лямбда-числення 36 

1.3. Історія лямбда-числення 44 

1.4. Редукція 46 

Висновок до розділу 1 65 

РОЗДІЛ 2. ЗМІШУВАННЯ СТРАТЕГІЙ ТА ПРОГНОЗУВАННЯ ЧАСУ ОДНОГО 

КРОКУ РЕДУКЦІЇ 68 

2.1. Змішування стратегій 68 

2.2. Генерація датасету лямбда-термів 70 

2.3. Аналіз продуктивності рандомізованих стратегій 71 

2.4. Прогнозування часу одного кроку редукції 77 

Висновок до розділу 2 94 

РОЗДІЛ 3. ОЦІНКА КІЛЬКОСТІ КРОКІВ РЕДУКЦІЇ ЗА ПЕВНОЮ 

СТРАТЕГІЄЮ МЕТОДАМИ МАШИННОГО НАВЧАННЯ 96 

3.1. Постановка проблеми оцінки кількості кроків редукції лямбда-термів за 

заданою стратегією 96 

3.2. Моделі машинного навчання для прогнозування кількості кроків редукції 

терму 100 

3.3. Проведення експериментів із оцінки кількості кроків редукції лямбда-термів 

за заданою стратегією 108 

3.4. Використання вбудовувань для прогнозування кількості кроків редукції за 

обраною стратегією 114 

Висновок до розділу 3 122 

РОЗДІЛ 4. НЕІНФОРМОВАНЕ НАВЧАННЯ 127 



 
 

18 

4.1. Розробка підходу до вилучення даних лямбда-термів 127 

4.2. Кластеризація лямбда-термінів за допомогою вбудовувань 141 

4.3. Редукція термів лямбда-числення: оцінка прогнозивних здатностей LLM 143 

4.4. Опис можливої імплементації методу 150 

Висновок до розділу 4 155 

ВИСНОВКИ 157 

СПИСОК ВИКОРИСТАНИХ ДЖЕРЕЛ 161 

Додаток А. СПИСОК ПУБЛІКАЦІЙ ЗДОБУВАЧА ЗА ТЕМОЮ ДИСЕРТАЦІЇ

 173 

 

 

 

 

 

 

  



 
 

19 

ПЕРЕЛІК УМОВНИХ ПОЗНАЧЕНЬ 

 

API – Application Programming Interface, Інтерфейс програмування 

застосунків (прикладний програмний інтерфейс) 

BERT – Bidirectional Encoder Representations from Transformers, тип ШНМ 

CBN – Call By Name, виклик за ім’ям 

CBV – Call By Value, виклик за значенням 

CHI – Calinski-Harabasz Index, індекс Калінського-Харабаша 

CNN – Convolutional Neural Network, згорткові нейронні мережі, клас 

глибоких штучних нейронних мереж 

DBI – Davies–Bouldin Index, індекс Девіса-Болдіна 

DBSCAN – Density-based spatial clustering of applications with noise, алгоритм 

кластеризації заснований на щільності 

GMM – Gaussian Mixture Model, метод кластеризації 

GRU – Gated Recurrent Unit, тип ШНМ 

HAC – Hierarchical Agglomerative Clustering, метод кластеризації 

HMM – Hidden Markov Models, приховані моделі Маркова 

IoT – Internet of Thing 

JVM – Java Virtual Machine 

kNN – k-Nearest Neighbors 

LI – Leftmost Innermost 

LLM – Large Language Model, велика мовна модель 

LLVM – Low Level Virtual Machine, віртуальна машина низького рівня 

LO – Leftmost Outermost, найбільш лівий найбільш зовнішній 

LSTM – Long short-term memory, довга короткочасна пам’ять, архітектура 

рекурентних нейронних мереж 

MAE – Mean Absolute Error, середня абсолютна похибка 

MIRACL – Multilingual Information Retrieval Across a Continuum of Languages 



 
 

20 

ML – Machine Learning, машинне навчання 

MSE – Mean Square Error, середньоквадратична помилка 

MTEB – Massive Text Embedding Benchmark, тест вбудовування масивних 

об'ємів тексту 

NLP – Natural Language Processing, розділ науки присвячений обробці 

природного мовлення 

PCA – Principal Component Analysis, Метод головних компонентів, способів 

зменшення розмірності даних 

RBF – Radial Basis Function 

RI – Rightmost Innermost, найбільш правий найбільш внутрішній  

RMSE – Root Mean Square Error, корінь середньоквадратичної помилки 

RNN – Recurrent Neural Network, Рекурентні нейронні мережі, клас штучних 

нейронних мереж 

RO – Rightmost Innermost 

SVM – Support Vector Machine, метод опорних векторів 

SVR – Support Vector Regression, регресія опорних векторів  

t-SNE – t-distributed Stochastic Neighbor Embedding, T-розподілене вкладення 

стохастичної близькості, метод візуалізації даних 

UR – Uniformly Random, стратегія редукції лямбда-термів 

WCSS – Within cluster sum of squares, внутрішньо кластерна сума квадратів  

ШІ – Штучний Інтелект 

ШНМ – Штучна Нейронна Мережа 

  



 
 

21 

ВСТУП 

 

Обґрунтування вибору теми дослідження. Вибір теми дослідження в галузі 

функціонального програмування та оптимізації стратегій редукції в безтиповому 

лямбда-численні зумовлений як теоретичною значущістю, так і практичним 

значенням у сучасному ландшафті розробки програмного забезпечення. 

Верифікація програмного забезпечення. Постійно зростаюча складність 

програмних систем призвела до зростаючої потреби в надійному коді, який можна 

перевірити. У той час як традиційні імперативні мови програмування домінували в 

галузі протягом десятиліть, функціональне програмування набуло значної 

популярності у сфері верифікації програм завдяки своїм притаманним 

математичним властивостям. 

Розвиток функціонального програмування як інструменту для верифікації 

програм насамперед пов’язаний з його формальними основами в математиці та 

логіці. Багато мов функціонального програмування, таких як Haskell, OCaml і Scala, 

ґрунтуються на лямбда-численні, формальній системі визначення функцій, яка, 

природно, піддається формальним системам міркувань і доказів. 

Функціональні мови програмування невід'ємно пов'язані з процесом 

верифікації програм через їхню основу в математичних функціях і формальній 

логіці. На відміну від імперативних мов, де зміни стану та побічні ефекти можуть 

ускладнити розуміння поведінки програми, функціональні мови підкреслюють 

незмінність та оцінку виразів, засновану виключно на вхідних значеннях. Таке 

узгодження з формальними системами, такими як лямбда-числення, полегшує 

перевірку правильності програми за допомогою математичних доказів. Оскільки 

функціональні програми часто складаються з чистих функцій, вони природно 

піддаються формальним методам верифікації, включаючи індуктивні докази, 

теорію типів і рівняння. Крім того, сильний акцент у функціональних мовах на 

рекурсії, функціях вищого порядку та системах типів забезпечує більш 

передбачувану та аналізовану поведінку, що додатково полегшує автоматизовані 



 
 

22 

процеси перевірки. Декларативний характер функціонального програмування 

створює чіткий шлях для встановлення правильності програми, що робить його 

цінною парадигмою в розробці систем, де надійність і математична точність є 

критичними. 

Вирішення фундаментального виклику функціонального програмування. 

Функціональне програмування стає все більш важливим у сучасній розробці 

програмного забезпечення, відомого своїм внеском у підвищення надійності 

програмного забезпечення, верифікації, валідації та масштабованості. Однак воно 

стикається зі значними проблемами, особливо з точки зору низької продуктивності 

та неефективного використання пам’яті. 

Розвиток розуміння лямбда-числення. Дослідження зосереджено на методах 

оцінки складності редукції лямбда-термів з точки зору часу кожного з кроків, що 

традиційно розглядаються однаковими, та загальної кількості кроків. Це 

дослідження сприяє глибшому розумінню процесу редукції в лямбда-численні, що 

є основою функціонального програмування. 

Інтеграція машинного навчання в оптимізацію функціональних програм та 

компіляторів. Це дослідження поєднує передові статистичні методи та методи 

машинного навчання, такі як лінійна регресія та моделі регресії ШНМ, щоб 

передбачити час редукції на основі характеристик термів. Інтеграція машинного 

навчання пропонує новий підхід до оптимізації компіляторів та інтерпретаторів 

функціональних мов програмування, що робить їх більш продуктивними та 

ресурсоефективними. 

Внесок в еволюцію мов програмування. Оскільки індустрія програмного 

забезпечення все більше використовує парадигми функціонального 

програмування, це дослідження надає критичні висновки та інструменти для 

вирішення деяких ключових проблем. Покращуючи обчислювальну 

продуктивність функціональних програм за допомогою оптимізованих стратегій 

редукції, дослідження робить внесок у ширшу область розробки та оптимізації мов 

програмування. 



 
 

23 

Нові підходи до скорочення обчислень. Дослідження різноманітних 

характеристик, що впливають на час редукції терму, сучасними методами 

машинного навчання, є новим підходом в цій галузі. Ці методи відкривають 

можливості для автоматизованої оптимізації стратегій редукції, потенційно 

призводячи до значного прогресу функціональних програм. 

Підсумовуючи, вибір теми дослідження обумовлений її потенціалом 

значного впливу на сферу функціонального програмування. Дослідження не тільки 

розглядає ключові проблеми в парадигмі, але й впроваджує нові підходи, які 

можуть призвести до значного покращення ефективності та результативності 

функціональних мов програмування та їх компіляторів. 

Отже, все це визначає актуальність рішення науково-прикладної задачі 

удосконалення існуючих або розробки нових методів машинного навчання для 

екстракції характеристик із програмного коду функціональних мов програмування, 

що впливають на обчислювальні витрати на їх компіляцію чи інтерпретацію. 

Вирішити поставлену задачу стає можливим із вибором в якості 

функціональної мови програмування лямбда-числення, що є найпростішим їх 

представником з обмеженнями по існуючим операціям, проте без обмежень в 

реалізації можливих програм. 

Мета дослідження – підвищення продуктивності функціональних програм 

за критерієм часу виконання за рахунок прогнозованого удосконалення процесів 

редукції лямбда-термів на основі методів штучного інтелекту. 

Завдання дослідження. 

1. Розробка експериментального середовища лямбда-числення, що дозволяє 

генерувати терми та імітувати процес редукції, що представляє собою виконання 

функціональних програм. 

2. Розробка та аналіз продуктивності параметричної рандомізованої стратегії 

в безтиповому лямбда-численні для можливості налаштування порядку процесу 

редукції під конкретні підмножини термів. 



 
 

24 

3. Оцінка складності одного кроку редукції з точки зору часу виконання для 

подальшої можливості вибору найпростіших кроків редукції під час виконання 

функціональних програм. 

4. Кластерний аналіз термів, для виявлення існуючих підмножин термів зі 

схожими характеристиками, що дозволить подальшу роботу з окремими 

кластерами. 

5. Оцінка кількості кроків редукції терму за обраною стратегією для 

подальшої можливості вибору найбільш продуктивної для конкретного терму. 

6. Оцінка прогнозивних здатностей LLM в розрізі передбачення наступного 

кроку редукції, для розуміння їх потенціалу для подальших досліджень. 

Об’єкт дослідження – процес редукції лямбда-термів, що забезпечує 

інтерпретацію та компіляцію функціональних мов програмування. 

Характеристиками цього процесу є кількість кроків та час виконання.   

Предмет дослідження – методи наближеної оптимізації функціональних 

мов програмування за рахунок підвищення продуктивності процесів редукції на 

основі використання методів штучного інтелекту, а саме штучних нейронних 

мереж для обробки текстової інформації, методів кластерного аналізу, методів 

аналізу чутливості.     

Методи дослідження. У роботі використовувався комплексний підхід із 

використанням широкого спектру архітектур моделей штучного інтелекту методів 

імітаційного та математичного моделювання, теорії графів, та методів кластерного 

аналізу для вирішення проблем редукції термів у безтиповому лямбда-численні.  

Дослідження включає застосування передових архітектур штучних 

нейронних мереж як LSTM, CNN і Transformer, кожна з яких має унікальні 

можливості для аналізу і прогнозування в контексті лямбда-числення, зокрема в 

оптимізації процесів редукції.  

 

 

 



 
 

25 

Наукова новизна отриманих результатів полягає в наступному. 

1. Вперше розроблено параметричну випадкову однокрокову стратегію 

редукції, що відрізняється від існуючих можливістю налаштування ймовірності 

вибору редексу для скорочення. Варіація параметрів дозволяє керувати процесом 

редукції лямбда-термів з метою підвищення його продуктивності для конкретних 

підмножин термів. 

2. Удосконалено метод оцінки складності кроку редукції лямбда терму, що 

відрізняється від існуючих використанням методів машинного навчання. Це 

дозволило підвищити точність прогнозування обчислювальної складності кроку 

редукції довільного лямбда-терму. 

3. Удосконалено експериментальне середовище емуляції лямбда-числення 

завдяки впровадженню процедури багатоетапної верифікації розробленого 

програмного забезпечення та автоматичної генерації лямбда-термів. Це дозволило 

забезпечити коректну реалізацію цього програмного забезпечення та створювати 

набори даних лямбда-термів для забезпечення теоретично необхідного покриття 

контрольованими конфігураціями лямбда-термів. 

4. Дістали подальшого розвитку методи представлення лямбда-термів у 

вигляді вбудовувань (embeddings), що на відміну від існуючих представлень 

забезпечує використання штучних нейронних мереж архітектури типу Transformer. 

Це дозволило збільшити глибину аналізу коду лямбда-термів та підвищити 

точність екстрації характеристик, що впливають на процес редукції. 

5. Дістав подальшого розвитку комплексний метод оптимізації стратегії 

редукції, що на відміну від існуючих поєднує моделі штучного інтелекту для оцінки 

часу (в кількості кроків) редукції з процедурою вибору стратегії нормалізації терму. 

Цей комплексний підхід є новим і в має потенціал скоротити загальний час 

нормалізації, що суттєво сприяє оптимізації програм, реалізованих 

функціональними мовами програмування. 

 



 
 

26 

Особистий внесок здобувача. Дослідження, зосереджене на оптимізації 

процесу редукції функціональних мов програмування, що представлені лямбда-

численням, початково концептуалізовано та керовано науковим керівником 

здобувача. Однак, в подальшому дослідження було виконане здобувачем 

самостійно. Всі результати наведені в дисертації були обґрунтовані особистими 

дослідженнями автора. Також окремі положення були аргументовані з 

використанням робіт інших науковців та мають посилання в тексті дисертації. В 

індивідуальних наукових роботах були розглянуті тільки авторські розробки та ідеї. 

Розробка ключових ідей та реалізація. Незважаючи на те, що головна тема 

дослідження була окреслена науковим керівником, здобувач особисто 

концептуалізував (доповнив) і розвинув основні ідеї, що лежать в основі 

впровадження дослідження.  

Моделі штучного інтелекту. Значною частиною внеску здобувача було 

проектування та розробка підходів використання моделей штучного інтелекту, 

включаючи моделі лінійної регресії та глибинних нейронних мереж. Здобувач 

самостійно взявся за завдання побудови підходів використання цих моделей, 

налаштування параметрів і адаптації, для вирішення задач даного дослідження. 

Кодування та виконання експериментів. Кодування і виконання 

експериментів проводилися в рамках командної роботи. У цьому аспекті здобувач 

відігравав центральну роль, включаючи практичне та теоретичне проектування 

експериментів, аналіз даних та інтерпретацію результатів. Здобувач активно 

співпрацював з членами команди, щоб забезпечити надійність та ефективність 

процесів дослідження. 

Постійне обговорення та вдосконалення. Впродовж дослідження здобувач 

брав участь у постійних дискусіях з науковим керівником. Цей спільний діалог був 

вирішальним для вдосконалення підходу та узгодження його з теоретичною 

структурою, встановленою науковим керівником.  



 
 

27 

Автор дисертаційної роботи активно брав участь у наукових дискусіях, 

написанні наукових статей за темою дисертації та доповідях результатів на 

міжнародних наукових конференціях. 

В роботі [1, 2] показано результати розробки основних ідей підходу 

екстракції даних з лямбда термів із застосуванням методів машинного навчання. В 

роботі [3] проаналізовано підходи до кластеризації вбудовувань лямбда термів, що 

були отримані із застосуванням штучних нейронних мереж на базі архітектури 

Transformer. В роботі [4] автором було показано основні підходи до оцінки 

прогнозивних здатностей великих мовних моделей щодо вибору оптимальної 

стратегії редукції лямбда термів. В наукових працях [5–7] автором було показано 

результати розробки випадкової стратегії редукції лямбда-термів та результати 

оцінки обчислювальної складності редукції лямбда-термів після аналізу деревної 

структури лямбда-термів. 

Підсумовуючи, особистий внесок здобувача в це дослідження був значним, 

особливо в області генерації ідей, розробки моделей, алгоритмічного кодування та 

виконання експериментів. Здобувач відігравав важливу роль у просуванні 

досліджень у напрямку досягнення поставлених цілей, кульмінацією яких стали 

цікаві ідеї та внесок у сферу функціонального програмування та оптимізації 

функціональних мов програмування. 

Зв’язок роботи з науковими програмами, темами, планами.  

Дисертаційна робота виконана відповідно до:    

1. Закону України No 2623-III «Про прiоритетнi напрями розвитку науки i 

техніки» редакція від 20.02.2021 р., зокрема за напрямом «Iнформацiйнi та 

комунiкацiйнi технології̈»;    

2. Закону України No 3715-VI «Про прiоритетнi напрями iнновацiйної 

діяльності в Українi» редакція від 05.12.2012 р., зокрема за напрямом «Розвиток 

сучасних iнформацiйних, комунікаційних технологій, робототехніки»;    



 
 

28 

Науковi дослідження, викладені в дисертації̈, виконані згідно з напрямом 

наукової̈ роботи кафедри Теоритичної та прикладної інформатики Харківського 

національного університету iм. В.Н. Каразіна.    

Практичне значення отриманих результатів.  

Дослідження, проведені в рамках цієї роботи, хоча переважно теоретичні, 

пропонують значні практичні наслідки у сфері функціонального програмування та 

оптимізації компіляторів. Практичне значення дисертації визначення далі. 

Підвищення ефективності мов функціонального програмування. Розробка 

параметричної однокрокової випадкової стратегії для редукції в лямбда-численні 

безпосередньо впливає на ефективність функціональних програм. Відходячи від 

детермінованих алгоритмів до стратегій, заснованих на випадковому пошуку, 

дослідження створює основу для компіляторів, які можуть динамічно обирати 

оптимальні стратегії редукції, тим самим покращуючи продуктивність. 

Покращення використання обчислювальних ресурсів. Пропонуючи методи 

прогнозування часу редукції певних редексів та загальної кількості кроків редукції, 

дослідження допомагає оптимізувати розподіл обчислювальних ресурсів. Це 

особливо корисно в середовищах, де ефективність використання ресурсів має 

вирішальне значення, наприклад у платформах хмарних обчислень. 

Оптимізація в функціональних мовах програмування. Отримані результати 

розширюють сферу оптимізації в функціональних мовах програмування за межі 

традиційних методів. Завдяки інтеграції моделей машинного навчання для 

прогнозування кількості кроків редукції та оцінки вимог до обчислювальних 

ресурсів дослідження пропонує нові підходи до оптимізації всього процесу 

нормалізації термів у функціональних мовах програмування. 

Основа майбутніх досліджень і розробок. Незважаючи на деякі обмеження в 

точності моделі, дослідження забезпечує основу для майбутніх досліджень. 

Ідентифікація характеристик, що впливають на час редукції терму можуть 

вплинути на визначення більш ефективних стратегій оптимізації. 



 
 

29 

Ефективність використання ресурсів у редукції лямбда-термів. Здатність 

передбачити кількість кроків редукції для лямбда-термів за допомогою навчених 

моделей має практичне значення для автоматизації пошуку оптимальних стратегій 

редукції. Цей підхід не тільки дозволяє скоротити обчислювальні ресурси, але й 

час, необхідний для процесів нормалізації термів. 

Застосування в складних програмних системах. Результати дослідження 

можуть бути застосовані в розробці складних програмних систем, де ефективність 

і швидкість мають першорядне значення. Розуміння поведінки редукції термів і 

оптимізації стратегії може бути особливо корисним у системах, які широко 

використовують парадигми функціонального програмування. 

Внесок у теоретичну та прикладну інформатику. Окрім функціонального 

програмування, дослідження встановлює зв’язки між різними галузями, такими як 

теорія лямбда-числення, машинне навчання та розробка програмного забезпечення. 

Цей міждисциплінарний підхід збагачує як теоретичну базу, так і практичне 

застосування в інформатиці. 

Підсумовуючи, хоча дослідження зберігає теоретичну спрямованість, його 

результати мають значні практичні застосування, зокрема у підвищенні 

ефективності та результативності компіляторів функціонального програмування та 

оптимізації продуктивності програмного забезпечення за допомогою передових 

стратегій редукції. 

Апробація результатів дисертації. Основні теоретичні положення, 

висновки і пропозиції, які містяться в дисертації, обговорювалися та були схвалені 

на засіданнях кафедри теоретичної та прикладної інформатики факультету 

математики та інформатики Харківського національного університету імені В.Н. 

Каразіна. Ключові положення дослідження оприлюднені у доповідях на науково-

технічних конференціях всеукраїнського та міжнародного рівнів: 

– Міжнародній науково-технічній конференції ICTERI 2023 (Україна, м. 

Івано-Франківськ, Прикарпатський національний університет імені Василя 

Стефаника, 2023 р.).  



 
 

30 

– Міжнародній науково-технічній конференції «Information Technology and 

implementation» IT&I-2023 (Україна, м. Київ, Київський національний університет 

імені Тараса Шевченка, 2023 р.)  

– Третій міжнародній науково-технічній конференції «International Workshop 

of IT-professionals on Artificial Intelligence» ProfIT AI 2023 (Канада, м. Ватерлоо, 

Університет Ватерлоо, 2023 р).  

Публікації. Основні теоретичні положення і висновки дисертації викладені у 

7 наукових працях, з яких 2 статті у наукових фахових виданнях, що входять до 

міжнародних наукометричних баз [1, 2] та 2 у наукових фахових виданнях України 

[3,4], та 3 тез наукових доповідей [5–7]. 

Структура та обсяг дисертації. Дисертаційна робота складається з вступу, 

чотирьох розділів, висновків, списку використаних джерел і одного додатку. 

Загальний обсяг дисертації становить 174 сторінок: у тому числі анотації на 13 

сторінках, зміст на 2 сторінках, основний текст на 143 сторінках, список 

використаних джерел із 105 найменувань на 11 сторінках та один додаток на 2 

сторінках. Робота містить 16 таблиць, 30 рисунків, з яких 1 на окремій 1 сторінці.  



 
 

31 

     РОЗДІЛ 1. 

БЕЗТИПОВЕ ЛЯМБДА ЧИСЛЕННЯ 

 

1.1. Функціональне програмування 

В останні роки індустрія програмного забезпечення стала свідком значного 

зсуву в бік прийняття парадигми функціонального програмування. Ця тенденція, 

ретельно проаналізована в основоположних роботах, таких як [1–7], що відображає 

оцінку унікальних переваг, які пропонує функціональне програмування в процесах 

розробки програмного забезпечення. Функціональні мови програмування 

забезпечують основу для верифікації програм завдяки їх узгодженню з 

математичною логікою, формальними системами та передбачуваною поведінкою. 

Функціональні мови програмування слугують інструментами для перевірки 

програмного забезпечення. Ці переваги, підкреслені ключовими дослідниками в цій 

галузі [2, 3, 7], що включають підвищену простоту структури коду, покращену 

можливість тестування компонентів програмного забезпечення, покращену 

можливість повторного використання коду та масштабованість проектування 

програмних систем. Ці особливості разом сприяють розробці надійних та 

ефективних програмних рішень, що задовольняють постійно зростаючій складності 

сучасного програмного забезпечення [2, 7].  

У фінансовому секторі функціональне програмування цінується за його 

сильний фокус на незмінності та чистих функціях, що може призвести до більш 

передбачуваних, відмовостійких систем. Такі мови, як Haskell і Scala, зазвичай 

використовуються для розробки фінансових моделей, систем управління ризиками 

та торгових платформ, які потребують високої точності та надійності [8–11]. 

Функціональні мови програмування застосовуються в різних областях та 

галузях завдяки їх здатності до управління складними системами, забезпечуючи 

при цьому високу надійність і зручність обслуговування [4–7]. Функціональне 

програмування відоме тим, що створює код, який легше тестувати, налагоджувати 

та підтримувати. Воно часто використовується в корпоративних середовищах, де 



 
 

32 

великі програмні системи вимагають високої стабільності, надійності та простоти 

обслуговування. Функціональні мови, як-от Haskell і Erlang, використовуються для 

розробки як невеликих інструментів, так і великомасштабних програм [7]. 

У фінансовому секторі функціональне програмування цінується за його 

сильний фокус на незмінності та чистих функціях, що може призвести до більш 

передбачуваних, відмовостійких систем. Такі мови, як Haskell і Scala, зазвичай 

використовуються для розробки фінансових моделей, систем управління ризиками 

та торгових платформ, які потребують високої точності та надійності [8–11]. 

Erlang, функціональна мова, розроблена Ericsson для використання в 

телекомунікаційних системах, є прикладом корисності функціонального 

програмування в цій галузі. Здатність обробляти численні одночасні дії робить її 

ідеальним для таких додатків, як сервери та бази даних, які потребують високої 

доступності та сталої продуктивності [12]. 

Методи функціонального програмування все частіше використовуються у 

веб-розробці для керування складним станом і побічними ефектами, які 

спостерігаються в сучасних веб-додатках. Такі мови, як Elixir (створена на 

віртуальній машині Erlang) і Scala, використовуються для створення 

масштабованих веб-сервісів, які можна відносно легко підтримувати. 

Функціональні концепції також поширені у фреймворках JavaScript, таких як React, 

де принципи функціонального програмування допомагають більш передбачувано 

керувати станом інтерфейсу користувача [13]. 

Функціональне програмування також підходить для завдань із інтенсивним 

використанням даних завдяки потужній підтримці незмінних структур і виразному 

синтаксису для обробки списків та інших колекцій. Такі мови, як Scala, особливо 

популярні в додатках для великих даних, головним чином завдяки їхній сумісності 

з Apache Spark, швидкою інфраструктурою для кластерних обчислень загального 

призначення [14]. 

Слід також зазначити, що функціональне програмування може спростити 

реалізацію алгоритмів, які використовуються в ШІ (штучному інтелекті) та 



 
 

33 

машинному навчанні. Математична чистота функціональних мов добре 

узгоджується з потребою алгоритмів у точності та продуктивності. Clojure, 

наприклад, використовується завдяки його потужним можливостям 

маніпулювання даними та перевагам у продуктивності, що випливають із JVM 

(Java Virtual Machine) [15]. 

Однією із частих областей застосування функціональних мов програмування 

є паралельне обчислення. Природна сумісність функціонального програмування з 

моделями одночасного та паралельного виконання робить його ідеальним для 

додатків, які потребують високого рівня паралелізму. Це пояснюється тим, що 

незмінність усуває проблеми, пов’язані зі спільним змінним станом, поширеним 

джерелом помилок у паралельних системах. Haskell і Erlang, наприклад, 

пропонують вбудовану підтримку паралелізму [7]. 

В сучасному світі пристроїв функціональне програмування може внести 

значний внесок у область IoT (Internet of Things), дозволяючи розробляти надійні, 

масштабовані та зручні в обслуговуванні системи, які можуть обробляти велику 

кількість з’єднань і одночасних завдань, таких як мережеві датчики та 

телекомунікаційне обладнання. Erlang і Elixir є відомими виборами в цій галузі 

завдяки їхній здатності обробляти багато з’єднань одночасно [16]. 

Функціональні мови програмування використовуються в різних сферах, де 

переваги чистих функцій, незмінності та експресивного паралелізму є особливо 

цінними. Ця зміна парадигми сприяє створенню більш надійного, керованого та 

стійкого до помилок коду, що робить його дуже корисним для сучасних складних 

систем у різних галузях. 

Незважаючи на переваги парадигми функціонального програмування 

можливо виділити значні недоліки такого підходу. В роботі [3] визначені основні 

недоліки, які перешкоджають більш широкому застосуванню парадигми. З них 

можна виділити проблеми з неефективним використанням пам’яті та нижчою 

продуктивністю порівняно з імперативними парадигмами. 



 
 

34 

Крім того, функціональне програмування обмежене нестачею фреймворків та 

інструментів, яких більше в імперативних середовищах. Ця прогалина в наявних 

засобах розробки ще більше ускладняється малою спільнотою експертів і 

користувачів, що обмежує доступність і еволюцію даного підходу [2, 17, 18]. 

Нижче детально наведено проблеми функціональних мов програмування на 

вирішенні яких сфокусоване дане дослідження: 

I. Низька продуктивність обчислення – це є найбільш гострою проблемою 

функціонального програмування. Обчислювальний процес у функціональній 

парадигмі характеризується застосуванням трьох ключових механізмів: альфа-

конверсії, бета-редукції та ета-конверсії [2, 17]. 

Кумулятивні витрати на обчислення програми, таким чином, є сукупністю 

витрат, пов’язаних з кожним із цих підпроцесів, разом із додатковими витратами, 

такими як розпізнавання редексу. Оцінка внеску кожного підпроцесу в загальну 

вартість обчислення визначається різними моделями для оцінки продуктивності 

обчислення функціональних програм. 

II. Визначення стратегії редукції. Неоднозначність процесу редукції 

потребує розробки стратегій, які можуть ефективно подолати цю складність. Однак 

визначення ефективної стратегії редукції є тонкою проблемою. Як показано в статті 

[17], не існує універсальної оптимальної стратегії редукції, що ускладнює завдання 

оптимізації функціональних програм для кращої продуктивності. 

Робота з існуючими функціональними мовами програмування може бути 

складною з точки зору оптимізації, тому для цього дослідження було обрано 

лямбда-числення як найпростіший варіант для представлення функціональних мов 

програмування загального застосування.  

Лямбда-числення та функціональне програмування глибоко взаємопов’язані 

між собою, причому лямбда-числення є основоположною теоретичною основою 

для розробки та розуміння мов функціонального програмування [19].  

Кажучи про спільну теоретичну основу, лямбда-числення, розроблене 

Алонзо Черчем у 1930-х роках, є формальною системою, призначеною для 



 
 

35 

дослідження визначення функції, застосування функції та рекурсії. Воно 

забезпечує теоретичну базу для опису функцій та їх обчислень. Ця система є суто 

функціональною, тобто вона розглядає функції як громадян першого класу, даний 

концепт є центральним для функціонального програмування [19, 20]. 

Мови функціонального програмування знаходяться під сильним впливом 

концепцій і структур, отриманих з лямбда-числення. Такі мови включають Haskell, 

Scheme, OCaml, Erlang та багато інших. У цих мовах функції можна передавати як 

аргументи, повертати з інших функцій і призначати змінним, що безпосередньо 

відображає те, як лямбда-числення розглядає функції як дані. 

Незмінність. Спільною ключовою концепцією для лямбда числення та 

функціональних мов програмування є незмінність. У лямбда-численні після 

визначення функції її зв’язок вводу-виводу не змінюється, що відображає 

незмінність даних у функціональному програмуванні, де об’єкти даних не можна 

змінювати після їх створення [19, 20]. 

Функції першого порядку. Лямбда-числення допускає функції, які працюють 

над іншими функціями та повертають їх. Ця концепція є основною у 

функціональному програмуванні, уможливлюючи потужні методи, такі як 

відображення, зменшення та фільтрування, які є фундаментальними для обробки 

списків і масивів [19, 20].  

Чистота функцій. Функції лямбда-числення є чистими функціями, тобто 

вони завжди дають однаковий результат для того самого входу без побічних 

ефектів. Функціональне програмування також наголошує на чистоті, щоб 

забезпечити передбачуваність і полегшити налагодження [19, 20]. 

Рекурсія. Лямбда-числення покладається на рекурсію для повторюваних або 

циклічних операцій, оскільки воно за своєю суттю не має циклічних конструкцій 

або ітераційних операторів. Це схоже у функціональному програмуванні, де 

рекурсія часто використовується замість циклів для повторюваних операцій. Крім 

того, лямбда-числення представило концепцію кодування Черча, яке представляє 

дані й оператори, використовуючи лише функції. Функціональні мови 



 
 

36 

програмування часто використовують подібні кодування та абстрактні 

представлення даних [19, 20]. 

Обчислення виразів. Стратегії оцінки, отримані з лямбда-числення, такі як 

звичайний порядок (Call by Name) і аплікативний порядок (Call by Value), мають 

безпосередній вплив на функціональне програмування [19, 20]. Наприклад, Haskell 

за замовчуванням використовує відкладене обчислення, відкладаючи обчислення 

до необхідного часу, тоді як такі мови, як ML і Scala, проводять обчислення 

аргументів в першу чергу. 

Таким чином, лямбда-числення не тільки надихнуло багато фундаментальних 

принципів функціонального програмування, але й продовжує впливати на його 

еволюцію. Його абстрактний підхід до функцій і обчислень забезпечує багату 

теоретичну базу, яка підвищує глибину та можливості функціональних мов 

програмування. Саме тому подальші експерименти та дослідження були проведені 

в рамках роботи з лямбда-численням.  

1.2. Лямбда-числення 

Лямбда-числення – це проста нотація для функцій та застосувань. Основна 

ідея застосування функцій до аргументів (application) та створення функцій за 

допомогою абстракцій (abstraction). Синтаксис базового лямбда-числення є доволі 

прозорим, роблячи його елегантним рішенням з фокусом нотації на репрезентації 

функцій. Функції та аргументи постійно перекликаються один з одним. В 

результаті була отримана нонекзистенціальна теорія функцій як правил для 

обчислення, на противагу екзистенціальній теорії, що розглядає функції як набори 

упорядкованих пар. Незважаючи на простий синтаксис, виразність та гнучкість 

лямбда-числення робить його ефективним інструментом для логіки та математики 

[19–21]. 

Лямбда-числення є елегантною нотацією для роботи із застосуванням 

функцій до аргументів. Розглянемо приклад математичного поліному 𝑥3 − 5𝑥 +  8 

у якості прикладу. Чому дорівнює значення зазначеного виразу при аргументі 𝑥 =

 3? Обчислення цього є досить очевидним, необхідно просто замість 𝑥 підставити 



 
 

37 

3, що призведе до отримання виразу 33 −  5 ∗ 3 +  8, що в подальшому 

обчислюється до значення 20. Представлення даного поліному у термінах лямбда-

числення можливе завдяки використанню символу λ, та матиме вигляд: 

 

𝑥3 − 5𝑥 +  8     (1.1). 

 

Оператор лямбда (λ) дозволяє абстрагуватися (to abstract) над змінною 𝑥. 

Інтуїтивно можна прочитати (𝜆𝑥. (𝑥3 − 5𝑥 +  8))𝑎 як вираз, що очікує на значення 

a для змінної x. Провівши таку заміну (як було у прикладі з числом 3), значення 

виразу стає 𝑎3  −  5𝑎 +  8. Символ λ сам по собі не має значення; він просто зв’язує 

змінну x, що вказана після символу λ, та дозволяє відокремити цю змінну від інших 

змінних x поза лямбда виразом. Термінологічно лямбда-числення полягає в 

застосування (або аплікації) виразу до його аргументу та отримати значення такого 

застосування. Вираз (𝑀𝑎) представляє собою застосування (application) функції M 

до аргументу a. Подовжуючи з даним прикладом ми отримуємо: 

 

(𝜆𝑥. (𝑥3 − 5𝑥 + 8)) 3 ⊳  33 −  5 ∗ 3 + 8 = 27 − 15 + 8 = 20 (1.2) 

 

Перший крок обчислення – це заміна 3 замість усіх входжень 𝑥 у виразі 𝑥3 −

5𝑥 + 8, це є переходом від терму абстракції до іншого терму за допомогою 

операції підстановки. Решта рівностей – є простими обчисленнями з цілими 

числами. Вираз 1.2 показує центральний принцип лямбда-числення, що 

називається β-редукцією (або β-reduction в оригіналі) або β-конверсія (або β-

conversion в оригіналі) [21–23]: 

 

(𝜆𝑥. 𝑀) 𝑁 ⊳  𝑀[𝑥: = 𝑁]    (1.3) 

 

Розуміння того, що можливо редукувати, або скоротити (⊳) терм аплікації 

(𝜆𝑥. 𝑀) 𝑁 терму абстракціі (ліву частину виразу, 𝜆𝑥. 𝑀) до чогось (праву частину 



 
 

38 

виразу, N) простою підстановкою N замість входжень x в M (це те, що нотація 

‘𝑀[𝑥: = 𝑁]’ представляє собою). β-редукція або β-конверсія – це основа лямбда-

числення. 

1.2.1. Синтаксис лямбда числення 

Оригінальний синтаксис лямбда-числення можна визначити за його 

алфавітом та використаними правилами, що показано у наступному визначенні. 

 

Визначення. Алфавіт лямбда-числення складається з символів: "(", ")", ".", 

"λ" та нескінченної кількості змінних. Тоді клас лямбда-терму можна визначити 

наступним чином [23]. 

1) Кожна змінна – це лямбда-терм. 

2) Якщо M та N це лямбда-терми, тоді (𝑀 𝑁) також лямбда-терм, що також 

називається термом аплікацією. 

3) Якщо M це лямбда-терм та x – це змінна, тоді (𝜆𝑥. 𝑀) – це лямбда-терм, що 

також називається термом абстракцією. 

 

Опущення символів дужок, як це притаманно формальним мовам із 

символами групування, також можливе, але за умови якщо це безпечно (тобто, коли 

їх можна повторно ввести лише одним способом) [21, 23]. Зіставлення більше ніж 

двох лямбда-термів є неможливим. Для уникнення перенавантаження виразів 

лямбда-термів береться правило асоціації зліва.  

 

Правило (асоціації зліва). Згідно з цим правилом [21, 23], якщо є деякий 

терм 𝑀1 𝑀2 𝑀3  … 𝑀𝑛 з опущеними дужками, то можна відновити усі дужки єдиним 

способом застосовуючи правило асоціації зліва, згідно з яким 𝑀1 та 𝑀2 можна 

об’єднати в (𝑀1 𝑀2)𝑀3  … 𝑀𝑛, далі об’єднати з 𝑀3 і отримати ((𝑀1 𝑀2)𝑀3) … 𝑀𝑛. 

Що в підсумку веде до єдиного способу відновлення всіх відсутніх дужок: 

(((𝑀1 𝑀2)𝑀3) … 𝑀𝑛).  

 



 
 

39 

Таким чином правило асоціації зліва дає можливість читання всіх 

послідовностей лямбда-термів довжина яких більша за 2 з опущеними дужками 

єдиним чином [21, 23]. 

 

1.2.2. Змінні, зв’язані та вільні 

Функція символу 'λ' в термі абстракції (𝜆𝑥. 𝑀) полягає в тому, що вона зв’язує 

появу змінної одразу після її появи в термі M. Таким чином 'λ' є аналогом 

універсального та екзистенціального кванторів ∀ та ∃ логіки першого порядку [21, 

23]. Аналогічно можна визначити поняття вільної та зв’язаної змінної. 

 

Визначення (вільної та зв’язаної змінних). Синтаксичні функції FV (вільна 

змінна, або free variable) та BV (зв’язана змінна, або bound variable) можна 

визначити за структурною індукцією лямбда термів [21, 23]: 

1) 𝐹𝑉(𝑥) = {𝑥}, 𝐵𝑉(𝑥) = ∅ 

2) 𝐹𝑉(𝑀 𝑁) = 𝐹𝑉(𝑀) ∪ 𝐹𝑉(𝑁), 𝐵𝑉(𝑥) = 𝐵𝑉(𝑀) ∪ 𝐵𝑉(𝑁) 

3) 𝐹𝑉(𝜆𝑥. 𝑀) = 𝐹𝑉(𝑀) − {𝑥}, 𝐵𝑉(𝜆𝑥. 𝑀) = 𝐵𝑉(𝑀) ∪ {𝑥} 

Якщо 𝐹𝑀(𝑀)  =  ∅, тоді 𝑀 називають комбінатором. 

 

Це в загальному підтверджує факт того, що 'λ' зв’язує змінні (тобто робить їх 

не вільними). Це є типовим для інших предметів із концептом логіки першого 

порядку, де потрібно зважати на можливі синтаксичні складності при виконанні 

операції підстановки [22]. Невимушену підстановку можна захистити узгодивши 

факт зацікавленості не в самих термах, а в певному класі еквівалентності термів. 

Тепер стає можливим визначити підстановку й конвенцію для уникнення 

складнощів перестановки. 

 

Визначення (підстановка). Визначити підстановку можна наступним чином 

𝑀[𝑥 ∶=  𝑁] як підстановку 𝑁 у всі вільні входження 𝑥 в 𝑀. Точне визначення [23] 



 
 

40 

за рекурсією на множині лямбда-термів полягає в наступному: для всіх термів A, B 

та M, та для всіх змінних x та y визначаються наступні правила: 

1) 𝑥[𝑥: = 𝑀] ≡ 𝑀 

2) 𝑦[𝑥: = 𝑀] ≡ 𝑦 (y відрізняється від x) 

3) (𝐴 𝐵)[𝑥: = 𝑀] ≡ 𝐴[𝑥: = 𝑀] 𝐵[𝑥: = 𝑀] 

4) (𝜆𝑥. 𝐴)[𝑥: = 𝑀] ≡ 𝜆𝑥. 𝐴 

5) (𝜆𝑦. 𝐴)[𝑥: = 𝑀] ≡ 𝜆𝑦. (𝐴[𝑥: = 𝑀]) (y відрізняється від x) 

 

Положення (1) визначення підставки вказує, що у разі заміни M на x і терм в 

якому відбувається заміна є x, тоді результатом буде просто M. Положення(2) 

вказує на те, що нічого не відбувається, коли терм представляє змінна, відмінна від 

x, але необхідно замінити x. Положення (3) зазначає, що підставка безумовно 

розподіляється по терму. Положення (4) і (5) стосуються абстрактних термінів і 

паралельних їм положень (2) і (1): якщо зв’язана змінна z абстрактного терму 

(𝜆𝑧. 𝐴) ідентична змінній x, для якої необхідно зробити заміну, тоді жодна 

підстановка не виконується (тобто підстановка зупиняється). Це узгоджується з 

наміром, що 𝑀[𝑥: = 𝑁] має позначати заміну N для вільних входжень x в M. Якщо 

M є абстрактним термом (𝜆𝑥. 𝐴), зв’язаною змінною якого є x, тоді x не входить 

вільно в M, тому нічого не потрібно робити. Це пояснює положення (4). Положення 

(5) вказує та те, що за умови якщо зв’язана змінна абстрактного терму відрізняється 

від x, то принаймні x має «шанс» вільно з’явитися в абстрактному термі, і заміна 

продовжується в тілі терму абстракції [21]. 

 

Визначення (заміна зв’язаних змінних, α-конвертованості) полягає, що 

терм N, отриманий з терму M згідно з заміною зв’язаної змінної якщо, приблизно, 

будь-який абстрактний терм (𝜆𝑥. 𝐴) всередині M був замінений на (𝜆𝑦. (𝐴[𝑥 ∶=

 𝑦])). Тоді терми M та N є α-конвертовані, якщо є послідовність замін зв’язаних 

змінних, що починається на термі M та закінчується на N [21, 23]. 

 



 
 

41 

Аксіома β-конвертованості (із застереженням про заборону захоплення) 

полягає в (𝜆𝑥. 𝑀) 𝑁 ⊳  𝑀[𝑥 ∶=  𝑁], зазначає, що жодна змінна, що була вільною в 

N не стає зв’язаною в M після підстановки [21, 23]. 

 

Існує необхідність тримати вільні змінні такими, навіть за умови, коли 

виникає можливість зв’язування змінної через підстановку необхідно виконати 

декілька α-перетворень, для уникнення зв’язування вільних змінних. Якщо 

враховувати це далі операції в лямбда-численні не призводять до синтаксичних 

складнощів. Так, наприклад, неможливо застосувати функцію λx. λy. (3𝑦 (𝑥 − 15)) 

для аргументу 3𝑦 адже підстановка 3𝑦 для x, та y в 3𝑦 буде зв’язано оператором 

зв’язування змінної 𝜆𝑦. Така підстановка може призвести до функції відмінної від 

запланованої. Але, якщо застосовуючи правило α-конвертованості до функції 

𝜆𝑥. 𝜆𝑦. (3𝑦 (𝑥 − 15)) отримаємо 𝜆𝑥. 𝜆𝑏. (3𝑏 (𝑥 − 15)), то застосування аргументу 

2𝑦 до цієї функції стає можливим. Тому, неможливо використати правило β-

конвертованості у виразі (𝜆𝑥. 𝜆𝑦. (3𝑦 (𝑥 − 15)))5𝑦 ⊳  𝜆𝑦. (15𝑦(𝑥 − 15)), але є 

можливим використати правило β-конвертованості у виправленому виразі 

(𝜆𝑥. 𝜆𝑦. (3𝑦(𝑥 − 15)))2𝑦 ⊳  𝜆𝑧. (15𝑦(𝑥 − 15)). 

Цей приклад допомагає побачити, чому застереження до β-конвертованості є 

важливим. Застереження нічим не відрізняється від того, що використовується у 

формулюванні аксіоми обчислення предикатів, а саме ∀𝑥𝜙 →  𝜙𝑥
𝜏, не надає жодної 

змінної, що є вільною в термі τ до того як виконана заміна, але стає зв’язаною після 

[24]. 

Синтаксис λ-числення є доволі гнучким. Присутня можливість 

формулювання будь-яких термів, навіть самозастосування, такого як (𝑥 𝑥). Такі 

терми видаються сумнівними, можна припустити, що використання таких термів 

може призвести до непослідовності, проте в будь-якому випадку можна знайти 

інструмент, що дозволяє позбутися таких термів. Якщо розглядати функції та 

множини впорядкованих пар певного типу, то x в (𝑥 𝑥) буде функцією множини 

впорядкованих пар, який містить як елемент пару (𝑥, 𝑦), першим елементом якої 



 
 

42 

буде сам x. Але жодна множина не може вмістити себе таким чином, аби не 

порушити аксіому регулярності. Виходить, з точки зору теорії множин такі терми 

є явно сумнівними. Але, в реальності, такі терми не призводять до неузгодженості 

та служать корисними у контексті лямбда-числення. Крім того, заборона таких 

термів, як це зроблено в теорії типів, не залишається без наслідків, як то втрата 

частини виразності нетипового лямбда-числення [21, 25]. 

1.2.3. Комбінатори 

Як було зазначено раніше комбінатори в лямбда-численні – це терми без 

вільних змінних. Інакше кажучи їх можна визначити як повністю визначені 

операції, оскільки в них немає вільних змінних. Існує певна кількість корисних 

комбінаторів лямбда-числення. Табл. 1.1 зазначає деякі з таких комбінаторів. Існує 

нескінченна кількість комбінаторів, проте наведені в табл. 1.1 комбінатори мають 

відносно короткі визначення й показали свою значимість в контексті лямбда 

числення [21]. 

 

Таблиця 1.1. 

Основні терми комбінатори лямбда-числення. 

Символ Визначення та застосування 

S 𝜆𝑥. 𝜆𝑦. 𝜆𝑧. (𝑥 𝑧 (𝑦 𝑧))  
Враховуючи, що (𝑥 𝑧 (𝑦 𝑧)) є термом ((𝑥 𝑧) (𝑦 𝑧)) аплікації (𝑥 𝑧) до 
(𝑦 𝑧). Тоді S – це оператор заміни та застосування: z втручається між x 
та y: замість застосування x до y застосовується (x z) до (y z) [23]. 

K 𝜆𝑥. 𝜆𝑦. 𝑥, де значення (𝐾 𝑀) є функцією константи, для будь якого 
значення аргументу є M. 

I 𝜆𝑥. 𝑥 – це функція ідентичності. 

B 𝜆𝑥. 𝜆𝑦. 𝜆𝑧 (𝑥 (𝑦 𝑧))  
Виклик (𝑥 𝑦 𝑧) що є не що інше як ((𝑥 𝑦) 𝑧), тому цей комбінатор не є 
тривіальною функцією ідентичності. 

C 𝜆𝑥. 𝜆𝑦 𝜆𝑧. 𝑥𝑧𝑦 – оператор заміни порядку аргументів. 

T 𝜆𝑥. 𝜆𝑦. 𝑥 – ідентичний до оператору K, також грає роль значення 



 
 

43 

Правди при використанні логіки в лямбда-численні. 

F 𝜆𝑥. 𝜆𝑦. 𝑦 – це оператор, що виконує роль Брехні при запровадженні 
логіки в лямбда-численні. 

ω 𝜆𝑥. (𝑥 𝑥) – це комбінатор самозастосування. 

Ω (𝜔 𝜔) – це комбінатор самозастосування до самозатостосування, що 
редукується в самого себе. 

Y 𝜆𝑦. ((𝜆𝑥. (𝑦 (𝑥 𝑥))) (𝜆𝑥. (𝑦 (𝑥 𝑥)))) – Парадоксальний комбінатор 
Каррі. Для кожного лямбда-терму X виконується: 
𝑌 𝑋 ⊳ ((𝜆𝑥. (𝑋 (𝑥 𝑥))) (𝜆𝑥. (𝑋 (𝑥 𝑥)))) ⊳
𝑋 ((𝜆𝑥. (𝑋 (𝑥 𝑥))) (𝜆𝑥. (𝑋 (𝑥 𝑥)))). 
Перший крок в редукції (𝑌 𝑋) призводить до терму аплікації 
((𝜆𝑥. (𝑋 (𝑥 𝑥))) (𝜆𝑥. (𝑋 (𝑥 𝑥)))), що повторюється в третьому кроці. 
Тому терм Y має властивість того що (𝑋 𝑌) та (𝑋 (𝑌 𝑋)) редукують до 
одного терму. 

Θ (𝜆𝑥. 𝜆𝑦. 𝑦 (𝑥 𝑥 𝑦)) (𝜆𝑥. 𝜆𝑦. 𝑦 (𝑥 𝑥 𝑦)) – це комбінатор фіксованої точки 
Тьюринга. Для кожного лямбда-терму X, (Θ X) редукується до X (Θ X). 

 

Нижче наведено табл. 1.2 [21–23] із позначеннями, що використовувалися в 

цій роботі для дослідження лямбда-числення . 

Таблиця 1.2. 

Позначення прийняті в дослідження для позначення виразів в лямбда-

численні. 

Позначення Значення 

M N Застосування функції M до аргументу N. Зазвичай дужки 
використовуються для розділення функції від аргументів, як це 
робиться в M(N). Проте, в лямбда-численні дужки є символом 
групування. Тому в лямбда-численні функція та аргумент 
пишуться поруч один з одним.  

P Q R Застосування (PQ) – терму аплікації до аргументу R. Використання 
правила лівого розкриття дозволяє однозначно визначити порядок 
застосувань в такому записі терму, що відповідає терму ((𝑃 𝑄) 𝑅). 

λx. M Символ λ зв’язує змінну x в тілі терму M. Такий синтаксис не є 
офіційним, проте він відображає підхід, що використовувався в 



 
 

44 

ранніх роботах логіки, де символ ‘.’ дозволяє виділити формулу ϕ 
у виразі ∀𝑥. 𝜙, як та що знаходиться під сферою впливу ∀x. 
Згідно з офіційною документацією запис терма абстракції має 
такий вид 𝜆𝑥[𝑀] або із додаванням дужок (𝜆𝑥[𝑀]). Було обрано 
запис терма абстракції через точку, адже це спрощує зображення 
термів. 

M[x := A] Це лямбда-терм, що був отриманий внаслідок півставки терму A на 
місце всіх вільних входжень x в терм M. 
Також можливі інші нотації, наприклад: 𝑀[𝑥/𝐴], 𝑀[𝐴/
𝑥], 𝑀𝑥

𝐴, 𝑀𝐴
𝑥, [𝑥/𝐴]𝑀. Вибір між ними є суто формальним рішенням. 

Було обрано запис 𝑀[𝑥 ∶=  𝐴], адже він представляє присвоєння 
значення змінній в деяких мовах програмування. 

M ≡ N Означає, що лямбда-терм M є ідентичний лямбда-терму N. Такий 
запис не є офіційною частиною документації лямбда-числення, 
проте дозволяє оцінювати відношення між лямбда-термами, що є 
теоретичною частиною лямбда-числення. Такий запис дозволяє 
визначати логічну рівність між термами, навіть за умови наявності 
відмінних змінних, тобто 𝜆𝑥. 𝑥 ≡  𝜆𝑦. 𝑦.  

 

1.3. Історія лямбда-числення 

Лямбда-числення походить з вивчення функція у якості правил. 

Основоположні складові лямбда-числення вже можуть бути знайдені вже в 

новаторській роботі Фреге (Frege, 1893) [26]. Фреге зазначив, що при вивченні 

функцій достатньо зосередитися лише на унарних функціях, тих що приймають 

рівно один аргумент на вхід. Процедура переходу від функції з однією змінною до 

функцій з декількома може бути проведена завдяки послідовному застосуванню 

декількох операцій абстракції, що видають на виході еквівалентну унарну 

операцію. Дана операція називається карування (curring). Або, можливо, з 

історичної точки зору її було б правильніше назвати фрегуванням (fregeing). В 

1920-х математику за ім'ям Мозес Шенфінкель вдалося просунути дану концепцію 

ще далі, завдяки його дослідженню так званих комбінаторів (combinators) [21]. Як 

це було прийнято на початку вивчення предмету, Шенфінкеля зацікавили 

трансформації, які можна спостерігати у формальній логіці, і його робота над 

комбінаторами була спрямована на внесення вкладу в основи формальної логіки. 



 
 

45 

Подібно до процесу редукції, що можна побачити в препозиційній логіці завдяки 

роботі Шеффера, Шенфінкель досяг видатних результатів, тим фактом, що всі 

функції (з точки зору всіх трансформацій) можуть бути представлені 

використанням всього двох комбінаторів K та S. 

Це було показано в теоремі Шенфінкеля, згідно з якою для будь-якого терму 

M, що побудований, завдяки двом комбінаторам K та S та змінній x, існує терм F 

(побудований тільки з комбінаторів K та S) такий, що можна вивести 𝐹𝑥 =  𝑀.  

Дана теорема доводиться послідовно, нехай існує такий алгоритм, що для 

даного M може побудувати необхідний F. Черч назвав даний алгоритм F ‘𝜆𝑥. 𝑀’ 

(Черч, 1932) [23]. З даної точки зору β-правило є виправданим, якщо ‘𝜆𝑥. 𝑀’ є 

функцією F, що задовольняє умові 𝐹𝑥 =  𝑀, тоді 𝜆𝑥. 𝑀𝑥 має спрощуватися до M. 

Це всього на всього конкретний випадок більш загального принципу, що для всіх 

N, (𝜆𝑥. 𝑀) 𝑁 має перетворюватися на 𝑀[𝑥: = 𝑁]. 

Незважаючи на те, що сьогодні наявна більш чітко визначена система 

абстракцій та переписування, в свої ранні роки лямбда-числення та комбінаторна 

логіка були тісно пов’язані з дослідженням основ математики. У руках Каррі, 

Черча, Кліні та Россера (одних із піонерів цієї галузі) основна увага була 

зосереджена на визначенні математичних об'єктів та виконанні логічних 

обґрунтувань у цих нових системах. В подальшому виявилося, що дані спроби в так 

званому заключному лямбда-численні та комбінаторній логіці були 

непослідовними та суперечливим. В свою чергу, Каррі ізолював себе та якісно 

пропрацював суперечливості, що в результаті стало відомим як парадокс Каррі [21]. 

Лямбда-числення заслуговує окреме місце в історії логіки, як джерело його 

перших нерозв’язних проблем. Задача: Для даних термів M та N визначити чи 𝑀 =

𝑁. (Теорія рівності щодо лямбда-термів ще не була визначена; визначення було 

надано пізніше.) Ця проблема також була показана як нерозвязна.  

Іншою ранньої проблемою лямбда-числення було питання, чи воно в цілому 

є не суперечливим (consistent). Під суперечливістю. мається на увазі, що всі терми 

рівні: можливою є редукція будь-якого лямбда-терму M до будь-якого іншого 



 
 

46 

лямбда-терму N. Те що це не так є результатом раннього лямбда числення. 

Початкові результати, що з’явилися були про те, що деякі терми, як от K та S, не 

можуть бути приведені один до одного. Пізніше був отриманий набагато більш 

значущий результат: теорема Черча-Россера, що дала змогу внести ясність в 

розуміння β-конверсії і може бути застосована для доведення незвідності між 

собою цілих класів лямбда-термів [21]. 

Початково лямбда-числення можна було назвати деяким видом формалізму, 

до 1960-х, коли останню семантику було затверджено. У той же час зв’язок лямбда-

числення з мовами програмування також був з’ясованим та окреслений. До того 

моменту всі моделі лямбда-числення були побудовані навколо ‘синтаксису’, в стилі 

Генкіна, та складалися з еквівалентності класів лямбда-термів (для зручності 

нотації). Завдяки застосуванням лямбда-числення у семантиці природних мов у 

роботах Монтегю та інших лінгвістів, відомості про даний предмет розійшлися 

світом. З тих часів лямбда-числення заслуговує почесне місце у таких областях як 

математична логіка, комп'ютерні науки , лінгвістика та багато інших [21]. 

1.4. Редукція 

Існують різноманітні визначення скорочення лямбда-термів, але основним є 

β-редукція. До цього вже було дано визначення β-редукції із використанням 

символу ⊳. Проте варто надати більш специфічне визначення. 

 

Визначення (однокрокова β-редукція). Однокрокова β-редукція 

(позначається як ⊳𝛽,1) для лямбда-термів A та B, що відрізняються одним кроком 

редукції можна записати як 𝐴 ⊳𝛽,1 𝐵, якщо існує підтерм C терму А, змінна x та 

лямбда терми M та N такі що С ≡  (𝜆𝑥. 𝑀) 𝑁. Та терм B є термом A за виключенням 

появи терму С в A, що замінений 𝑀[𝑥 ∶=  𝑁] [21, 23]. 

 

Далі наведено декілька прикладів β-редукції. 

1) Змінна x не може бути β-редукована у будь-що, оскільки це просто змінна, 

що не є аплікацією. 



 
 

47 

2) (𝜆𝑥. 𝑥)𝑎 ⊳𝛽,1  𝑎. 

3) Якщо x та y є відмінними змінними, то (𝜆𝑥. 𝑦)𝑎 ⊳𝛽,1 𝑦. 

4) Лямбда-терм (𝜆𝑥. ((𝜆𝑦. 𝑥 𝑦) 𝑎) ) 𝑏 можна β-редукувати в 2 різних лямбда-

терми, проте ще один крок редукції все одно веде до одного і того самого терму:  

(𝜆𝑥. ((𝜆𝑦. 𝑥 𝑦)𝑎)) 𝑏 ⊳𝛽,1 (𝜆𝑦. 𝑏 𝑦) 𝑎 ⊳𝛽,1 𝑏 𝑎  

(𝜆𝑥. ((𝜆𝑦. 𝑥 𝑦)𝑎)) 𝑏 ⊳𝛽,1 (𝜆𝑥. 𝑥 𝑎) 𝑏 ⊳𝛽,1  𝑏 𝑎  

Можливо визначити різні похідні поняття від запису β-редукції одного кроку 

⊳𝛽,1, що є притаманним для будь-яких бінарних відношень.  

 

Визначення. Так можна визначати послідовність β-редукції від терму A до 

терму B як скінченну послідовність 𝑠1, … , 𝑠𝑛, що починається з A і закінчується B, 

за суміжною умовою для (𝑠𝑘, 𝑠𝑘+1) задовольняють умови 𝑠𝑘  ⊳𝛽,1  𝑠𝑘+1.  

 

Або загально кажучи, будь-яка послідовність s – скінченна або нескінченна 

послідовність β-редукції, що починається з лямбда-терму A та задовольняє умови 

𝑠𝑘  ⊳𝛽,1  𝑠𝑘+1 для (𝑠𝑘, 𝑠𝑘+1) [21, 23]. 

1) Не існує послідовності β-редукцій для змінної x. 

2) Для терму ((𝜆𝑥. 𝑥) 𝑎) існує єдина послідновність β-редукцій, що є 

((𝜆𝑥. 𝑥) 𝑎), 𝑎. Оскільки в кінці послідовності стоїть змінна, то цю послідовність 

неможливо продовжити згідно з першим прикладом. 

3) Комбінатор Ω має цікаву властивість: 𝛺 ⊳𝛽,1  𝛺. Тому кожний терм Ω є 

частиною нескінченної послідовності β-редукцій терму Ω. 

4) Цікава властивість у терму (𝐾 𝑎 𝛺), що є початком нескінченної кількості 

варіантів β-редукцій:  

• (𝐾 𝑎 𝛺)  ⊳𝛽,1  𝑎  

• (𝐾 𝑎 𝛺)  ⊳𝛽,1  (𝐾 𝑎 𝛺)  ⊳𝛽,1  𝑎  

• (𝐾 𝑎 𝛺)  ⊳𝛽,1  (𝐾 𝑎 𝛺)  ⊳𝛽,1  (𝐾 𝑎 𝛺)  ⊳𝛽,1  𝑎  



 
 

48 

• (𝐾 𝑎 𝛺)  ⊳𝛽,1  (𝐾 𝑎 𝛺)  ⊳𝛽,1 …  

Якщо a – це змінна, то можна побачити, що всі послідовності скорочень терму 

(𝐾 𝑎 𝛺) починаються з (𝐾 𝑎 𝛺), та закінчуються з a. 

 

Визначення (β-редексу). Також можна визначити β-редекс лямбда-терму M 

як поява деякого субтерму M в формі (𝜆𝑥. 𝑃) 𝑄. Простіше кажучи β-редекс є 

кандидатом на β-редукцію в деякому лямбда-термі. Кажуть, що терм перебуває в β-

нормальній формі, якщо він не має β-редексів [21, 23]. 

 

Чи може терм мати декілька β-нормальних форм? Літерально кажучи “так”, 

проте по суті “ні”. Тобто якщо M та M' є β-нормальними формами деякого терму, 

тоді M є α-конвертованим до M'. Тому β-нормальна форма є унікально аж до зміни 

зв'язаних змінних. 

Було розглянуто одно-крокову β-редукцію, але можна поєднати декілька 

кроків β-редукцій в один шляхом транзитивного замикання відношення ⊳𝛽,1.  

 

Визначення (β-редукованості). Для лямбда-термів A та B можна сказати, що 

A β-редукується до B, що записується як 𝐴 ⊳𝛽,1  𝐵, якщо 𝐴 ≡  𝐵 або якщо існує 

скінченна послідовність β-редукцій від A до B [21, 23].  

 

Визначення (наявності β-нормальної форми). Терм M має β-нормальну 

форму якщо існує терм N такий, що N є в β-нормальній формі 𝑀 ⊳𝛽,1  𝑁. 

 

Як вже було визначено, редуктивність – це односторонній зв’язок, тому в 

загальному не вірно якщо 𝐴 ⊳𝛽,1  𝐵, то 𝐵 ⊳𝛽,1  𝐴. Проте, залежно від мети, 

можливо визначити еквівалентність термів A та B якщо A редукується до B чи B 

редукується до A. Це означає про можливість розгляду відношення ⊳𝛽,1 як 

рефлексивне, симетричне та транзитивне [21, 23]. 

 



 
 

49 

Визначення. Для лямбда-термів A та B, кажуть що 𝐴 =𝛽  𝐵, якщо 𝐴 ≡  𝐵 чи 

існує послідовність 𝑠1, … , 𝑠𝑛, що починається з A та закінчується з B та для 

послідовних термів (𝑠𝑘, 𝑠𝑘+1) виконується одна з умов 𝑠𝑘  ⊳𝛽,1  𝑠𝑘+1 чи 

𝑠𝑘+1  ⊳𝛽,1  𝑠𝑘. 

1.4.1. Стратегії редукції 

Терм називається β-нормальною формою, якщо в його тілі відсутні β-редекси, 

тобто підтерми форми (𝜆𝑥. 𝑀) 𝑁. Терм має β-нормальну форму, якщо його можна 

звести до терму в β-нормальній формі. Має бути інтуїтивно зрозуміло, що якщо 

терм має β-нормальну форму, то можливо знайти її шляхом вичерпної редукції всіх 

β-редексів терму, потім вичерпної редукції всіх β-редексів всіх наступних термів і 

так далі. Сказати, що лямбда-терм має β-нормальну форму, означає сказати, що цей 

сліпий пошук можливо закінчити [21, 23]. 

Сліпий пошук β-нормальних форм термів очевидно не є ефективним, через 

потребу у повному скороченні всіх β-редексів. Необхідна деяка стратегія редукції, 

бажано обчислювана, для знаходження β-нормальної форми. Проблема полягає в 

тому, щоб ефективно вирішити, чи існує певні підмножини β-редексів терму, які 

слід скоротити, а які можуть бути пропущені. 

Отже, визначати стратегію β-редукції можна як функцію де вхідними даними 

є усі лямбда-терми, значення яких на термі M не в β-нормальній формі, є редексним 

підтермом М, і значення на всіх термах M в β-нормальній формі є просто M [21, 23]. 

Простіше кажучи, стратегія β-редукції вибирає множину β-редексів які 

необхідно скоротити. Можна представити стратегію S як відношення ⊳𝑆 на лямбда-

термах, з розумінням того, що 𝑀 ⊳𝑆  𝑁 за умови, що N отримано з M за один крок, 

дотримуючись стратегії S. Якщо розглядати як відношення, стратегії редукції 

представляють субвіношення ⊳𝛽,1. 

 

Визначення. Стратегією редукції називають алгоритм, який приймає на вхід 

терм, що не є нормальною формою, а повертає один з його редексів для 

редукування. Стратегія редукції – це специфічний методичний підхід, який 



 
 

50 

використовується в лямбда-численні для вибору та застосування правил редукції 

до лямбда-виразів. Стратегія визначає, який редекс лямбда-терму має бути 

редукований на кожному кроці процесу обчислення.  

 

Стратегії β-редукції може мати, або не мати властивість того, що дотримання 

цієї стратегії зрештою забезпечує досягнення β-нормальної форми, якщо така існує 

[21, 23]. Вибір стратегії редукції може вплинути не лише на ефективність і 

результат обчислювального процесу, але й на те, чи завершиться процес або 

досягне нормальної форми [23]. 

Тому визначати стратегію β-редукції S як нормалізуючу якщо для всіх 

лямбда-термів M, якщо M має β-нормальну форму N, тоді послідовність 

𝑀, 𝑆(𝑀), 𝑆(𝑆(𝑀)), … закінчується на N. Деякі стратегії редукції є нормалізуючими, 

а інші – ні [21, 23]. 

Стратегії редукції у функціональному програмуванні визначають як і коли 

обчислюються аргументи функції та як виконується застосування функції. Ці 

стратегії є ключовими для розуміння операційної семантики мов програмування. 

Серед найвідоміших стратегій – Call by Name (CBN), Call by Value (CBV), Leftmost 

Outermost (LO) і Rightmost Innermost (RI) [23, 27–29]. Кожна має своє походження, 

визначення, алгоритми, переваги, недоліки та випадки використання. 

Call by Name(CBN) [23, 27–29]. 

– Походження та визначення: виклик за іменем – це стратегія редукції, де 

аргументи функції не оцінюються перед викликом функції. Натомість функція 

застосовується безпосередньо до виразів аргументів без оцінки. Щоразу, коли 

потрібен аргумент, вираз обчислюється . 

– Алгоритм: у CBN кожне входження параметра в тіло функції замінюється 

фактичним виразом аргументу. Якщо аргумент складний, він може бути 

переоцінений кілька разів, що призведе до потенційної неефективності. 



 
 

51 

– Переваги: може бути більш ефективною, коли аргументи не 

використовуються в тілі функції, оскільки уникають непотрібних оцінок. Стратегія 

також підтримує створення керуючих структур і операторів як звичайних функцій. 

– Недоліки: численні оцінки одного виразу можуть призвести до 

неефективності, особливо якщо вираз інтенсивно обчислюється. Це також може 

призвести до неприпинення, навіть якщо існує порядок припинення редукції. 

– Використання: CBN зазвичай використовується в мовах і сценаріях, де 

бажана відкладена оцінка, і дуже важливо відкладати обчислення до абсолютної 

необхідності. 

Call by Value (CBV) [23, 27–29]. 

– Походження та визначення: виклик за значенням є найпоширенішою 

стратегією редукції, коли аргументи функції повністю оцінюються перед викликом 

функції. Результат цієї оцінки потім передається у функцію. 

– Алгоритм: у CBV кожен вираз аргументу обчислюється один раз, а 

отримане значення прив’язується до відповідного параметра в тілі функції. 

– Переваги: це дозволяє уникнути потенційної неефективності 

багаторазового обчислення виразу. Даний підхід є передбачуваним і простим, що 

робить його типовим у багатьох мовах програмування. 

– Недоліки: може бути неефективним, якщо аргументи складні та не 

використовуються в тілі функції, оскільки обчислюються вирази, які ніколи не 

знадобляться. 

– Використання: CBV широко використовується в імперативних мовах 

програмування та сценаріях, де необхідне суворе оцінювання або де накладні 

витрати на потенційні численні оцінки занадто дорогі. 

Leftmost Outermost (LO) [23, 27–29]. 

– Походження та визначення: LO – це стратегія, яка часто асоціюється з 

ледачим оцінюванням у функціональних мовах. Вона завжди вибирає для оцінки 

крайній лівий, крайній зведений редекс. 



 
 

52 

– Алгоритм: стратегія проходить по дереву виразу, завжди вибираючи 

крайній лівий крайній редекс для редукції. Це часто відповідає «зовнішньому» 

виклику функції у вкладеному виразі. 

– Переваги: LO гарантує знаходження нормальної форми, якщо вона існує, 

що робить її вигідним для обчислень, де не потрібно оцінювати всі аргументи. Вона 

добре узгоджується з ледачим обчисленням, уникаючи непотрібних обчислень. 

– Недоліки: у деяких випадках дана стратегія може виконувати більше 

операцій редукції, ніж потрібно, порівняно з іншими стратегіями. Ця стратегія 

також може бути менш інтуїтивно зрозумілою для тих, хто знайомий з строгими 

парадигмами оцінювання. 

– Використання: зазвичай використовується в мовах, які підтримують 

відкладене обчислення, таких як Haskell, що допускає такі конструкції, як 

нескінченні структури даних. 

Rightmost Innermost (RI) [23, 27–29]. 

– Походження та визначення: RI – це стратегія, яка обирає крайній правий 

внутрішній редекс для скорочення, що є подібним до пошуку в глибину в дереві 

виразів починаючи справа. 

– Алгоритм: стратегія обходить дерево виразів, щоб знайти найбільш 

глибоко вкладений редекс, починаючи з правого боку. Після виявлення цей редекс 

редукується. 

– Переваги: у певних випадках, особливо з конкретними арифметичними 

обчисленнями або коли всі аргументи потрібно врешті-решт оцінити, RI може бути 

ефективнішим, ніж інші стратегії. 

– Недоліки: RI не гарантує знаходження нормальної форми, якщо вона існує, 

і може призвести до непотрібних обчислень, якщо деякі аргументи не 

використовуються в тілі функції. 

– Використання: це менш поширена стратегія, але її можна використовувати 

в певних сценаріях, де відомо, що її шаблон оцінки є корисним. 



 
 

53 

А також існують стратегії Leftmost Innermost (LI) та Rightmost Outermost 

(RO), що є відповідними модифікаціями LO та RI стратегій відповідно, проте не 

знайшли такого великого поширення. Згідно з визначенням LI є такою стратегією, 

що на кожному кроці крайній лівий із внутрішніх редексів редукується, де 

внутрішній редекс є редексом, який не містить жодних редексів. Та RO є такою 

стратегією, що на кожному кроці крайній правий із крайніх редексів скорочується, 

де крайній редекс є редексом, який не міститься в жодному редексі. 

Таким чином, CBN і CBV зосереджені на тому аби оцінювати аргументи при 

застосуванні функцій, причому CBN є ледачою стратегією на відміну від CBV. На 

відміну від цих стратегій, LO та RI стосуються вибору, яку частину виразу оцінити 

першою, причому LO надає перевагу крайнім лівим зовнішнім редексам, а RI – 

крайнім правим внутрішнім. Вибір між цими стратегіями залежить від конкретних 

вимог і характеристик завдання програмування, а також від природи мови, що 

використовується. Кожна з них має свої переваги та компроміси, що робить їх 

придатними для різних сценаріїв у величезному просторі функціонального 

програмування. 

 

Теорема (Барендрегта про неіснування оптимальної стратегії редукції): 

У безтиповому лямбда-численні не існує єдиної стратегії редукції, яка була б 

оптимальною для всіх лямбда-термів. Оптимальна стратегія редукції – це така 

стратегія, що мінімізує кількість кроків для досягнення нормальної форми для 

будь-якого лямбда-терму, за умови існування нормальної форми [23]. 

 

Пояснення: 

• Стратегія редукції в лямбда-численні визначає порядок і спосіб, у який 

виконуються редукції (зокрема бета-редукції) лямбда-термів. 

• Стратегія вважається оптимальною, якщо для кожного лямбда-члена, який 

має нормальну форму, вона знаходить нормальну форму, використовуючи 

найменшу можливу кількість кроків β-редукції. 



 
 

54 

• Теорема Барендрегта стверджує, що такої універсально оптимальної 

стратегії не існує. Це пов’язано з внутрішньою складністю та різноманітністю 

лямбда-термів, де різні терми можуть вимагати різних підходів для ефективного 

скорочення. 

• Доказ передбачає демонстрацію того, що для будь-якої запропонованої 

оптимальної стратегії завжди можна побудувати конкретний лямбда-терм, де 

альтернативна стратегія досягає нормальної форми за меншу кількість кроків. 

1.4.2.Методи підвищення ефективності процесу редукції 

Оптимізація стратегій редукції в лямбда-численні – це складна тема, яка 

перетинає теорію інформатики, реалізацію мови програмування та обчислювальну 

логіку [30–34]. Мета полягає в тому, щоб підвищити ефективність і 

передбачуваність обчислень, що виконуються в цій абстрактній структурі. Далі 

буде представлений опис деяких найсучасніших методів оптимізації стратегій 

редукції, які були досліджені та розроблені в останні роки.  

I. Графова редукція – ефективний метод оптимізації лямбда-числення, що 

замість дублювання термів, як у бета-редукції, використовує графову структуру для 

повторного використання загальних підвиразів [32, 33]. Це робить процес 

швидшим та ефективнішим, і застосовується, наприклад, у мові Haskell [34]. 

II. Оптимальні стратегії редукції, таких як редукування Леві, 

зосереджений на мінімізації кроків та уникненні дублювання термів. Хоча ця 

стратегія теоретично оптимальна, її реалізація складна і потребує значних 

обчислень [31]. 

III. Лінива оцінка, або виклик за потребою, відкладає обчислення виразів до 

моменту, коли їхні значення необхідні, зменшуючи кількість редукцій і уникаючи 

оцінки термінів, які не використовуються. Цей підхід, подібний до стратегії CBN, 

широко застосовується в Haskell і суттєво покращує продуктивність 

функціональних програм, особливо з складними або нескінченними структурами 

даних [34, 35]. 



 
 

55 

IV. Суперкомпіляція – це метод програмної трансформації, який, аналізуючи 

поведінку програми під час виконання, усуває непотрібні обчислення та скорочує 

терміни, перетворюючи програму на більш ефективну версію. Цей метод можна 

адаптувати для оптимізації виразів лямбда-числення, особливо у функціональному 

програмуванні [36]. 

V. Редукція за типом. У типізованих системах лямбда-числення типи 

можуть керувати процесом редукції. Використовуючи інформацію про тип, можна 

виконати певну оптимізацію, наприклад, зменшити лише ті вирази, які призводять 

до правильного типу результату [37]. Це може запобігти безрезультатним 

скороченням і віддати пріоритет тим, хто з більшою вірогідністю сприятиме 

остаточному обчисленню. 

VI. Паралельна редукція. Стратегії паралельної редукції дозволяють 

одночасно скорочувати кілька редексів, що прискорює обчислення на 

багатоядерних процесорах. Методи, як явна заміна, допомагають підтримувати 

узгодженість замін у паралельних частинах терму [38]. 

VII. Техніки машинного навчання. Останнім часом зростає інтерес до 

використання машинного навчання для оптимізації компіляторів та 

інтерпретаторів [39]. Це дозволяє прогнозувати ефективні шляхи редукції в лямбда-

численні, навчаючи моделі на історичних дани