# Mathematical Foundation of a Functional Implementation of the CNF Algorithm
## 5 Conclusions  
Algorithm 1 summarises the content of the article. The structure of the work suggests using for loops instead of while loops, and we have done so. The following comments are appropriate:  
* As we commented before, according to Definition 3, Definition 5, and Remark 2, the result of the two for loops in Algorithm 1 is a formula equivalent to the one that each of the loops took as a starting point. Thus, in each application of the algorithm, the result obtained retains the semantic meaning of the form it took as initial data. * Each for loop in Algorithm 1 acts if and only if a change in the formula is necessary, i.e., if \(\operatorname{m}>0\). In this case, the pre-calculated length of each of the two loops (respectively, alt, according to Defintion 2, and akr, according to Definition 4) is exactly the minimum necessary to obtain the intended purpose of the loop. This extreme is guaranteed by Corollary 2 and Corollary 3. In short, under this approach, the length of the two for loops is optimal. * The algorithm achieves what it sets out to do, as stated in Corollary 2 and Corollary 3. * In each of the for loops of Algorithm 1, the comparison between the result formula of each round and that of the previous one, which was carried out in the classical formulation of the algorithm (reproduced in summary and pseudocode in Section 1) in order to decide whether the work has been completed, has disappeared. In its place, a single operation has appeared for each loop, before its start, consisting of the traversal and reading of a single formula, namely the loop data formula. In the general case, a priori this is an improvement over the classical formulation of the CNF algorithm, which in pseudocode we summarily reproduced in Section 1. Very unfavorable examples can be consulted in the readme.md of our GitHub repository [[https://github.com/ringstellung/CNF](https://github.com/ringstellung/CNF)]([https://github.com/ringstellung/CNF](https://github.com/ringstellung/CNF)) (accessed on 23 September 2023), and you can see how it is confronted by our Haskell implementation. * Definition 3 and Definition 5 are an unpublished presentation of the well-known core of the CNF algorithm. We believe we have included, with great concreteness, the concept of \"recursive substitution\" inspired by the usual style of lambda calculus. We believe we have found the appropriate language to be able to express in a very precise way, eliminating all ambiguity, a process usually described with certain formal licenses. We have no doubt that other improvements in the efficiency of the CNF algorithm are possible, although we have only dealt with one here. In the future, we will investigate how to combine all of them. For this, we will build on some of those already introduced in the Haskell code of our GitHub repository. The content of this article will be used in the future to act in the field of the classical SAT problem, e.g., to optimally prepare the application of the Davis-Putnam algorithm. We intend to compare this improved algorithm with that of deduction by sequents. ```
0:\(\alpha\in\mathrm{P}(\mathbf{L})\)
0:\(\beta\in\mathrm{lcnf}(X)\) procedureCNFsa(\(\alpha\)) \(m\leftarrow\mathrm{alt}(\alpha)\) for\(1\leq n\leq m\)do \(\alpha\leftarrow\mathrm{dak}(\alpha)\) endfor \(m\leftarrow\mathrm{hre}(\alpha)\) for\(1\leq n\leq m\)do \(\alpha\leftarrow\mathrm{lasc}(\alpha)\) endfor return\(\alpha\) endprocedure
```  
**Algorithm 1** CNF simplified algorithm for formulas in \(\mathrm{P}(\mathbf{L})\)  
In order to show the feasibility and effectiveness of the theoretical advances presented in this article, we have elaborated a functional implementation for the Haskell language. In it, we also give a preview of the implementation of the Davis-Putnam algorithm. The code can be consulted at [[https://github.com/ringstellung/CNF](https://github.com/ringstellung/CNF)]([https://github.com/ringstellung/CNF](https://github.com/ringstellung/CNF)) (accessed on 23 September 2023).