The most simplest notion of the algorithm is some kind of function with input and output. Input and output can be very sophisticated mathematical objects (not only numbers), but the is irrelevant, because we can encompass all those generalities by the use of category theory. More formal notion of the algorithm is through use of Turing machines. But the most mathematically rigorous view is using lambda calculus/type theory, in which algorithmic function is lambda type (also theorem) and its implementation using concrete data structures and execution paths is lambda term (also proof of this theorem though the Curry-Howard correspondence). Of course, there is also notion of abstraction: each lambda type is lambda term of some higher order lambda type. Lot of theory is there.
But my question is this - is there branch of mathematics that considers the space of lambda types/algorithms, that considers the action of operators (program transformations, evolutions, compositions) in this space for transforming one algorithm into another, that consider subspaces of this space of types/algorithms and so on? When I read any article about functional analysis, like https://www.sciencedirect.com/science/article/pii/S0001870819305778, I always wonder is it possible to transfer the notions of function space, of function transformation, of optimal function (from calculus of variations) to the space of algorithms? And is it not possible, then why not?
While it would be very tempting to imagine such 'calculus of algorithms', my guess is that the answer is not so simple. Lambda calculus is very general framework, actually - full math can be encoded in it (e.g. in the language of Coq proof assistant) that is why whole math constitutes such 'functional space' of algorithms. And indeed - whole math branches into disciplines according - one math consider numbers (subspace on numbers), another branch consider graphs (subspace on graphs) and so on. So - my initial question splits into two questions (whose answers jointly can give the answer to my initial question in the previous paragraph):
- Is it really true that whole math is the (function) space of lambda types/algorithms and one should not seek anything new, one should do math according to the established patterns and that gradually discovers all of the lambda types/algorithms.
- Let it be so. If point 1 is true, then we can focus avoid all the generalities and consider the class of the usual programming algorithms, e.g. sorting (algorithms on vectors), path discovery in graphs (algorithms on graphs), common substring discovery (algorithms on strings). Lets consider this subsapce of the lambda terms/algorithms. Then I have more bounded question - is there some branch of mathematics that consider the lambda types/algorithms (of the usual software programming) as some function space? What is this branch, how it is named?
Why my question is important? There is nascent trend - symbolic reinforcement learning in which the optimal policy is expressed as program/algorithm (generally - as lambda type). And such framework begs for answers to such questions:
- Let algorithm A be the policy of the agent, i.e. algorithm A receives the information about state and returns the action that agent should take and that should bring some immediate or delayed reward. How to evaluate the future reward of algorithm A?
- Let algorithm A be the policy of the agent. Let us suppose that agent observers data d, computes and takes action a and receives reward r. Such new information can change the estimation made in the point 1. What update should be applied to A (what transformation operator should be applied to A) to get A' that is more optimal with regards the future reward?
https://papers.nips.cc/paper/9308-demystifying-black-box-models-with-symbolic-metamodels is example how functions/algorithms can be encoded and how the numerical optimization methods can be used for finding the program. Inductive Logic Programming approach https://en.wikipedia.org/wiki/Inductive_logic_programming is about deriving the logical programs that can explain data. ILP approach can be generalized to the meta-interpretative learning e.g. http://andrewcropper.com/pubs/jelia19-typed.pdf that allow use of higher order logic and compositionality in the inferred programs. All those are practical approaches done by computer scientists, but I am seeking the effort of mathematicians on these advancements? Or maybe mathematicians are not making any effort in such direction.
Of course, there is studies on computability/complexity (P=NP problems), there is studies on arithmetical hierarchies (the classification of formulas according to their complexity), but such studies do not give any measure (e.g. reward measure) on the program and such studies do not consider the program transformation.
Is there some branch of mathematics that can help for defining fitness metrics on the programs/algorithms/lambda types and that can help for defining the transformation operators on the programs/algorithms/lambda types, where algorithms are the usual software engineering algorithms expressed in some sufficiently mathematical form (not the whole math, as we already deduced)?
http://people.idsia.ch/~juergen/goedelmachine.html is practical effort that is can exploit the branch of mathematics that I am seeking.