# (Functional) space of all lambda types (algorithms)?

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):

1. 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.
2. 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:

1. 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?
2. 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.

• It is very unclear what mathematical question or questions your are actually asking. You make a rather odd statement right at the beginning: the Turing Machine model of computation and the $\lambda$-calculus model are both completely rigorous (and equivalent), so suggesting the latter is more rigorous than the former is wrong (and I suspect it's not what you really meant to say). I think it would be helpful to break your question down into much simpler questions (and not to ask them all at once). You may then get a better idea of how the MSE community can help you. – Rob Arthan Feb 13 at 22:12
• With due respect - I put in bold the essence of my question - is there branch of mathematics for metrics on lambda types and for defining transformations on lambda types - aka functional spaces for lambda types. I can not see how more succint can I be and what can be divided futher here. Well - it may be possible that I am asking for new mathematics. But I can not believe that I am the first one. E.g. new branches emerges every moment, algebraic combinatorics is recent example. – TomR Feb 13 at 22:16
• You have 4 sections in bold in your (very long and far from clear) question. The natural answer to the first one of these sections is "yes, that branch of mathematics is called computer science", but I doubt that is the answer you are looking for. You won't get good answers on MSE unless you make your question crisp and unambiguous. – Rob Arthan Feb 13 at 22:24

It seems to me that the notion of computable function is the answer to my question - it is pure math. Construction and analysis of algorithms is still the answer from the side of applied math. Theory of computable functions is still developing and https://www.acie.eu/70-2/ archives those developments in the widest sense. There is whole world beyond computable functions and arithmetical and hyperarithmetical hierarchies suggest.