**I'm seeking for a coautor/scientific advisor to research more on the following topic.**

За последние года полтора (плюс древние мысли последних 5 лет) вырисовывается вот такая вот заготовка, там не всё гладко, но в стольких местах "случайно" сходилось, что может выйти интересно. Ниже текст заготовки.

The basic form of recursion is the course-of-values recursion:

in order to define a function f: ℕ -> ℕ we define a “recursor”

and define

i.e. r(list) derives the next value of f depending on the argument of f (calculated as length(list)) and all previous values of f. We'll denote the list (f(0),.., f(n - 1)) by (Σf)(n), so the function f is defined by the equation

which can be solved constructively step-by-step.

This form of recursion (primitive recursion) is very weak it wouldn't allow to simulate mutual recursion for instance. We need to let f(n) depend on certain f(m) with m above n but still avoid vicous circles and infinite descent.

How do ensure absence of vicious circles? Their absence is equivalent to existence such ordering <' on ℕ (which might be different from the usual ordering) so that f(n) depends only on f(m) with m <' n. If the number of elements below n finite (given by g(n)), we can perform as before with the only difference that it's non-trivial for r to find the value of the argument depending on list length: it must apply the inverse of g to the length.

Now in all nontrivial cases the number of elements “below” n according to <' might be infinite. In this case cannot form a “list of all values below n”, we need to construct something like a lazy list! A constructive version of a lazy list is the enumeration function (enum n: ℕ): ℕ -> ℕ that successively enumerates (in usual < order, starting with zero) all values m which are below m according to <'. Absence of infinite decent is ensured by monotone function c: ℕ -> ℕ with c(0) = 0 that provides a bound on how many elements from the enumeration (enum n) are taken in order to calculate f(n).

So, the triple (enum: ℕ -> ℕ -> ℕ, c: ℕ, r: List ℕ -> ℕ) defines the recursive function. In order to evaluate f(n) we form a list of c(n) “preceding” values of f(n) and feed it into r: somehow composes the elements of this list and the number n (which is recovered as “inverse c applied to length of the inbound list”):

(+ denotes composition)

We might note that the evaluation of f according to this equation is horribly inefficient: to calculate f(n) we calculates c(n) other values of f separately, i.e. without memorization although every calculation eventually reduces to values of f at zero, and the closer to zero we are the more often values of f are used for calculations of f at higher arguments. Can we find an algorithm (and reformulate the equation) to make use of memorization?

Memorization cache is always a key-value store, we'll fill it one-by-one until we arive at f(n). We'll start by filling f(0). Then we'll loop the following step:

STEP: Find the smallest natural number n such that the cache already contains c(n) values f(m) with m <' n. Evaluate f(n) and save into the cache.

The byproduct of this algorithm is the sequence O: ℕ -> ℕ of arguments at which we evaluate. It must be a bijection: f should be eventually evaluated at every point and only once. The inverse -O of this function provides us with information how many times r has to be performed to calculate f(n), so it's just the computational complexity of f in terms of r. Now, in form of an equation:

The only condition for this equation to be solvable is the invertibility of H, we make no reference to any kind of order <' and enumeration function. Actually, H already contains all information about the order, it's invertibility is equivalent to well-foundness of the order it represents and the inverse -O is the Hardy function for this order.

Note that the notion of recursion representable by the last equation is the most general one, it includes all cases of transfinite recursion (and, by Curry-Howard correspondence, also transfinite induction) with any degree of mutuality. It mirrors but does not include the dual notion of corecursion/coinduction, also known as bar recursion/induction, which includes backtracking and dependent, countable or general choice depending on which uncountable ordinals we postulate to exist.

In which setting does the equation above actually make sense?

Let's start with an example: a Σ'-Monoid of natural numbers be the monoid of natural numbers by addition together with two additional operations:

We'll study equations over Σ'-monoids. Equation systems over the Σ'-monoid of natural numbers exactly correspond to (polynomial) diophantine equations since multiplication can be expressed via Σ operation and vice verse:

The cantor pairing function (natural numbering of natural number pairs) can be expressed in this monoid very neatly:

Variable-length lists [a, b,.., c] are customarily encoded as nested pairs (lenthOfTheList, (a, (b, (..c..)))).

MRDP-theorem establishes that all computable (directed) relations ℕ ↬ ℕ can be expressed in form of such equations with distinguished "in" and "out" variables. Computable directed relation can be viewed as a possibly multivalued or partial function on natural numbers. This view gives an idea what composition of such objects is. In terms of equations, composition of the relations P(in, out) and Q(in, out) is a new relation given by {P(in, intermediate), Q(intermediate, out)}.

Another example of a Σ'-Monoid is given by Σ'-monoif Ord of recursive ordinals, a natural noncommutative extension of natural numbers.

Let Σ'-Monoid of directed computable relations ℕ ↬ ℕ is the monoid of these relations by composition with two additional operations:

[0, 1, .., in] and feeds it into the function (f' + f'' + ...))

In this monoid pairing is given by

The definitions fit exactly do define primitive recursive function by the already mentioned equation

and in general case,

We suspect that there is a global duality between equations over Ord and ℕ ↬ ℕ with underlying mutual interpretability of solving algorithms, i.e. the solvability of an equation in one case is equivalent to the solvability of its dual in the other. For instance

The letter one states totality of multiplication while the former states realizability of primitive recursion. Both have ordinal strength omega when used once or alpha < omega^omega when iterated.

Every directed equation system (DES) over a can Σ'-Monoid can be interpreted as a partial function ℕ ↬ ℕ or as a transformation acting on such partial functions. In particular, DESes can be applied to themselves much like lambda terms can. If the duality would turn out to work, it would mean that duals of total DES are exactly the transformations preserving totality.

If we'll denote duals by * and application by juxtaposition, "P* total, Q total" implies "PQ total", which gives a rise to both: a calculus which can be used to construct total computable functions and an illative deduction system with only one rule (application) every sentence of which can be interpreted as both "P total/solvable" and "P* is a totality-preserwing DES transformation/truth preserving proof schema". The system also exibits Curry-Howard correspondence: DES on Nat is not just a partial function but also a predicate, DES on ℕ ↬ ℕ is not only transformer of partial functions but also a proof.

This deduction system seems to be an excellent environment for metamathematical studies:

- it has straightforward computational interpretation and is as weak as possible: its proof theoretical strength in absence of induction axioms is omega, much less then PRA (omega^omega) and even rudimentary function arithmetic (omega^2). It might even be self verifying in sense of Willard.

- it is single-sorted (no types like in PRA) but still exibits Curry-Howard correspondence (better then PRA);

- it's logic-free (self contained) as PRA in Goodstein formulation and utilizes linear logic (unless we introduce dub and dup axioms) which allows for fine-graned proof-theoreic-strength-tuning (better then PRA, EFA, RFA);

- it has minimal nontrivial set of operators and only one deduction rule (better then PRA, EFA, RFA);

- it is comparably handy to typed lambda calculi when you have to define AST types and perform syntactic manipulations and at the same time it has optimal facilities to speak about ordinals and proof-theoretic strength (both much better then PRA, EFA, RFA, Peano arithmetic).

Recall that the recursion rule states:

We cannot formulate this in form of one equation since there are restrictions on input, we must shift them to the output. i.e. the thing we could do is the following: given any total r and O we could produce function §f that consumes h and returns a pair (n, f(n)) where n = O h:

We could turn this “pair generator” into a guarded function, i.e. a function !f that consumes pairs n, h. If O(n) >= h, the output is f(n), otherwise zero. Guarded functions are the philosophically right approach to totality: if a function needs some extra space in order to evaluate, it consumes not only the argument but also an evidence that there is enough space in form of an correspondingly large number.

By von Neumann construction, ordinals consist of ordinals, therefore recursive ordinals can be modeled by hierarchical type-theoretical universes which nicely also form a Σ'-Monoid. We'll study the correpsondence between ordinals modeled by their O-functions and as type universes.

In type theories types sum of types A + B = Either[A, B] is, assuming univalence, an associative operation with neutral element _|_ = Empty, so types form a monoid. A universe is, roughly said, is a type whose inhabitants are types. For a universe U we can define U' = U + {U} (i.e. we add one element (the original universe U) to the universe U and get U') and ΣU = (T: U, T), i.e. ΣU is a dependent pair where the first element is an element of the universe and the second an element of the first one (recall that the first element is a type). For finite universes U = {T1, T2, .., Tn} we recover ΣU = T1 + T2 + ... + Tn.

Ordered pairs are represented with additional binary consturctor:

Type family is very much like context-free generative grammar for such trees. It consists of two finite or recursively enumerable sets of labels (constructor labels and type labels) and finite or recursively enumerable set of rules that specify type and arity for each constructor label, where arity is a finite (possibly empty) list of argument types of the constructor.

Nat is a particularly simple type family:

TYPES: {Nat}

CONSTRUCTORS: {zero, succ}

RULES

zero: () -> Nat

succ: (Nat) -> Nat

An example of infinite type family would be the family containing finite data types Fin 0, Fin 1 etc.:

TYPES: {Nat, Fin (n: Nat)}

CONSTRUCTORS: {zero, succ, fzero, fsucc (n: Nat), fid (n: Nat)}

RULES:

zero: () -> Nat

succ: (Nat) -> Nat

fzero: () -> Fin zero

fsucc n: (Fin n) -> Fin (succ n)

fsid n: (Fin n) -> Fin (succ n)

We require all type families to be closed, i.e. all types and constructors used in rules should be declared and described. In other words, if a term belongs to a type family T then all its subterms also belong to T. By T(n) we'll denote the set of all terms belonging to T with rank n, by #T(n) we'll denote the number of terms belonging to T with a given rank, it is by definition of rank a finite number. We'll call the function #T: Nat -> Nat growth function of the type family T. By ΣT(n) and Σ#T(n) we'll denote the set of all terms with ranks up to n and the cumulative growth function respectively.

Fixing a linear order on the constructors of a certain type family allows to fix one-to-one numbering of the terms belonging to it and a well-order on the terms.

The well order (called "lexicographical") is given by the following recursive definition: in order to compare a and b first compare their roots (constructors are now ordered), if they are equal, compare the first arguments (as subterms), if they are equal, compare second arguments and so on. If we don't find the difference, terms are equal. It is more efficient to perform recursion on the term (one of a and b) with lower rank if the ranks differ. The algorithm always performs one comparison (on root constructors) and then processes the terms of the lower rank (i.e. of the rank below min(|a|, |b|)). Since there are Σ#T(min(|a|, |b|)-1) possible such terms, the lexicographical comparison reduces to utmost (1 + Σ#T(min(|a|, |b|)-1)) constructor comparisons, hence it's decidable. Note that this bound is optimal, i.e. exact for some a and b in certain type families.

The function O: Nat->Nat that maps n-th term (by natural ordering) to the number of elements below n w.r.t. lexicographic ordering among first n elements by natural ordering. This function contains all information about the type family and lexicographic order on it up to homotopical equivalence. We even can recover signatures of the constructors.

**Towards diophantine illative logic**

**1. Algebraic treatment of recursion**The basic form of recursion is the course-of-values recursion:

in order to define a function f: ℕ -> ℕ we define a “recursor”

r: (List ℕ) -> ℕ

and define

f(0) = r([]) f(1) = r([f(0)]) f(2) = r([f(0), f(1)]) ...

i.e. r(list) derives the next value of f depending on the argument of f (calculated as length(list)) and all previous values of f. We'll denote the list (f(0),.., f(n - 1)) by (Σf)(n), so the function f is defined by the equation

f(n) = r((Σf)(n))

which can be solved constructively step-by-step.

This form of recursion (primitive recursion) is very weak it wouldn't allow to simulate mutual recursion for instance. We need to let f(n) depend on certain f(m) with m above n but still avoid vicous circles and infinite descent.

How do ensure absence of vicious circles? Their absence is equivalent to existence such ordering <' on ℕ (which might be different from the usual ordering) so that f(n) depends only on f(m) with m <' n. If the number of elements below n finite (given by g(n)), we can perform as before with the only difference that it's non-trivial for r to find the value of the argument depending on list length: it must apply the inverse of g to the length.

Now in all nontrivial cases the number of elements “below” n according to <' might be infinite. In this case cannot form a “list of all values below n”, we need to construct something like a lazy list! A constructive version of a lazy list is the enumeration function (enum n: ℕ): ℕ -> ℕ that successively enumerates (in usual < order, starting with zero) all values m which are below m according to <'. Absence of infinite decent is ensured by monotone function c: ℕ -> ℕ with c(0) = 0 that provides a bound on how many elements from the enumeration (enum n) are taken in order to calculate f(n).

So, the triple (enum: ℕ -> ℕ -> ℕ, c: ℕ, r: List ℕ -> ℕ) defines the recursive function. In order to evaluate f(n) we form a list of c(n) “preceding” values of f(n) and feed it into r: somehow composes the elements of this list and the number n (which is recovered as “inverse c applied to length of the inbound list”):

f(n) = r((Σ(f + (enum n)))(c n))

(+ denotes composition)

We might note that the evaluation of f according to this equation is horribly inefficient: to calculate f(n) we calculates c(n) other values of f separately, i.e. without memorization although every calculation eventually reduces to values of f at zero, and the closer to zero we are the more often values of f are used for calculations of f at higher arguments. Can we find an algorithm (and reformulate the equation) to make use of memorization?

Memorization cache is always a key-value store, we'll fill it one-by-one until we arive at f(n). We'll start by filling f(0). Then we'll loop the following step:

STEP: Find the smallest natural number n such that the cache already contains c(n) values f(m) with m <' n. Evaluate f(n) and save into the cache.

The byproduct of this algorithm is the sequence O: ℕ -> ℕ of arguments at which we evaluate. It must be a bijection: f should be eventually evaluated at every point and only once. The inverse -O of this function provides us with information how many times r has to be performed to calculate f(n), so it's just the computational complexity of f in terms of r. Now, in form of an equation:

f = r + Σ(f + O) - O

The only condition for this equation to be solvable is the invertibility of H, we make no reference to any kind of order <' and enumeration function. Actually, H already contains all information about the order, it's invertibility is equivalent to well-foundness of the order it represents and the inverse -O is the Hardy function for this order.

Note that the notion of recursion representable by the last equation is the most general one, it includes all cases of transfinite recursion (and, by Curry-Howard correspondence, also transfinite induction) with any degree of mutuality. It mirrors but does not include the dual notion of corecursion/coinduction, also known as bar recursion/induction, which includes backtracking and dependent, countable or general choice depending on which uncountable ordinals we postulate to exist.

In which setting does the equation above actually make sense?

**2. Algebraic setting**Let's start with an example: a Σ'-Monoid of natural numbers be the monoid of natural numbers by addition together with two additional operations:

n' = n + 1 Σn = 1 + 2 + ... + n

We'll study equations over Σ'-monoids. Equation systems over the Σ'-monoid of natural numbers exactly correspond to (polynomial) diophantine equations since multiplication can be expressed via Σ operation and vice verse:

ab + a + b = Σ(a + b).

The cantor pairing function (natural numbering of natural number pairs) can be expressed in this monoid very neatly:

pair = Σ(fst + snd) + snd

Variable-length lists [a, b,.., c] are customarily encoded as nested pairs (lenthOfTheList, (a, (b, (..c..)))).

MRDP-theorem establishes that all computable (directed) relations ℕ ↬ ℕ can be expressed in form of such equations with distinguished "in" and "out" variables. Computable directed relation can be viewed as a possibly multivalued or partial function on natural numbers. This view gives an idea what composition of such objects is. In terms of equations, composition of the relations P(in, out) and Q(in, out) is a new relation given by {P(in, intermediate), Q(intermediate, out)}.

Another example of a Σ'-Monoid is given by Σ'-monoif Ord of recursive ordinals, a natural noncommutative extension of natural numbers.

Let Σ'-Monoid of directed computable relations ℕ ↬ ℕ is the monoid of these relations by composition with two additional operations:

f' = {f(fIn, fOut), in = Σ(fIn + passThruArgument) + passThruArgument, out = Σ(fOut + passThruArgument) + passThruArgument} Σf(n) = generates the list [f(0),...,f(n – 1)](we could also say that it generates the list

[0, 1, .., in] and feeds it into the function (f' + f'' + ...))

In this monoid pairing is given by

productFunction = fst' + snd

The definitions fit exactly do define primitive recursive function by the already mentioned equation

f = r + Σf

and in general case,

f = r + Σ(f + O) – O.

We suspect that there is a global duality between equations over Ord and ℕ ↬ ℕ with underlying mutual interpretability of solving algorithms, i.e. the solvability of an equation in one case is equivalent to the solvability of its dual in the other. For instance

{out = in + Σout} is dual to {out + in = Σout}

The letter one states totality of multiplication while the former states realizability of primitive recursion. Both have ordinal strength omega when used once or alpha < omega^omega when iterated.

**3. Towards diophantine illative logic**Every directed equation system (DES) over a can Σ'-Monoid can be interpreted as a partial function ℕ ↬ ℕ or as a transformation acting on such partial functions. In particular, DESes can be applied to themselves much like lambda terms can. If the duality would turn out to work, it would mean that duals of total DES are exactly the transformations preserving totality.

If we'll denote duals by * and application by juxtaposition, "P* total, Q total" implies "PQ total", which gives a rise to both: a calculus which can be used to construct total computable functions and an illative deduction system with only one rule (application) every sentence of which can be interpreted as both "P total/solvable" and "P* is a totality-preserwing DES transformation/truth preserving proof schema". The system also exibits Curry-Howard correspondence: DES on Nat is not just a partial function but also a predicate, DES on ℕ ↬ ℕ is not only transformer of partial functions but also a proof.

This deduction system seems to be an excellent environment for metamathematical studies:

- it has straightforward computational interpretation and is as weak as possible: its proof theoretical strength in absence of induction axioms is omega, much less then PRA (omega^omega) and even rudimentary function arithmetic (omega^2). It might even be self verifying in sense of Willard.

- it is single-sorted (no types like in PRA) but still exibits Curry-Howard correspondence (better then PRA);

- it's logic-free (self contained) as PRA in Goodstein formulation and utilizes linear logic (unless we introduce dub and dup axioms) which allows for fine-graned proof-theoreic-strength-tuning (better then PRA, EFA, RFA);

- it has minimal nontrivial set of operators and only one deduction rule (better then PRA, EFA, RFA);

- it is comparably handy to typed lambda calculi when you have to define AST types and perform syntactic manipulations and at the same time it has optimal facilities to speak about ordinals and proof-theoretic strength (both much better then PRA, EFA, RFA, Peano arithmetic).

**4. Encoding the recursion rule as DCE**Recall that the recursion rule states:

For all r, O and H satisfying O + H = 0 there is f satisfying f = r + Σ(f + O) + H.

We cannot formulate this in form of one equation since there are restrictions on input, we must shift them to the output. i.e. the thing we could do is the following: given any total r and O we could produce function §f that consumes h and returns a pair (n, f(n)) where n = O h:

in = r' + o out = (r + Σ(out + O))' + O + dup

We could turn this “pair generator” into a guarded function, i.e. a function !f that consumes pairs n, h. If O(n) >= h, the output is f(n), otherwise zero. Guarded functions are the philosophically right approach to totality: if a function needs some extra space in order to evaluate, it consumes not only the argument but also an evidence that there is enough space in form of an correspondingly large number.

**5. Ordinals as a type universe; Σ'-Monoid of universes**By von Neumann construction, ordinals consist of ordinals, therefore recursive ordinals can be modeled by hierarchical type-theoretical universes which nicely also form a Σ'-Monoid. We'll study the correpsondence between ordinals modeled by their O-functions and as type universes.

In type theories types sum of types A + B = Either[A, B] is, assuming univalence, an associative operation with neutral element _|_ = Empty, so types form a monoid. A universe is, roughly said, is a type whose inhabitants are types. For a universe U we can define U' = U + {U} (i.e. we add one element (the original universe U) to the universe U and get U') and ΣU = (T: U, T), i.e. ΣU is a dependent pair where the first element is an element of the universe and the second an element of the first one (recall that the first element is a type). For finite universes U = {T1, T2, .., Tn} we recover ΣU = T1 + T2 + ... + Tn.

**5.1 W-Types**Type theories describe finite terms and their types. A term is a finite ordered tree with labeled leaves (called 0-ary constructors or terminals) and nodes (called n-ary constructurs where n is the number of children). Subtrees are called subterms. The number of nodes (non-terminals) of a term is called its rank, rank of t is denoted by |t|. Natural numbers are usually represented by linear trees:0 ~ [zero] 1 ~ [succ] -> [zero] 2 ~ [succ] -> [succ] -> [zero]

Ordered pairs are represented with additional binary consturctor:

(0, 1) ~ [pair] -> [zero] -> [succ] -> zero

Type family is very much like context-free generative grammar for such trees. It consists of two finite or recursively enumerable sets of labels (constructor labels and type labels) and finite or recursively enumerable set of rules that specify type and arity for each constructor label, where arity is a finite (possibly empty) list of argument types of the constructor.

Nat is a particularly simple type family:

TYPES: {Nat}

CONSTRUCTORS: {zero, succ}

RULES

zero: () -> Nat

succ: (Nat) -> Nat

An example of infinite type family would be the family containing finite data types Fin 0, Fin 1 etc.:

TYPES: {Nat, Fin (n: Nat)}

CONSTRUCTORS: {zero, succ, fzero, fsucc (n: Nat), fid (n: Nat)}

RULES:

zero: () -> Nat

succ: (Nat) -> Nat

fzero: () -> Fin zero

fsucc n: (Fin n) -> Fin (succ n)

fsid n: (Fin n) -> Fin (succ n)

We require all type families to be closed, i.e. all types and constructors used in rules should be declared and described. In other words, if a term belongs to a type family T then all its subterms also belong to T. By T(n) we'll denote the set of all terms belonging to T with rank n, by #T(n) we'll denote the number of terms belonging to T with a given rank, it is by definition of rank a finite number. We'll call the function #T: Nat -> Nat growth function of the type family T. By ΣT(n) and Σ#T(n) we'll denote the set of all terms with ranks up to n and the cumulative growth function respectively.

**5.2. Lexicographical ordering, natural numbering and characteristic function**Fixing a linear order on the constructors of a certain type family allows to fix one-to-one numbering of the terms belonging to it and a well-order on the terms.

The well order (called "lexicographical") is given by the following recursive definition: in order to compare a and b first compare their roots (constructors are now ordered), if they are equal, compare the first arguments (as subterms), if they are equal, compare second arguments and so on. If we don't find the difference, terms are equal. It is more efficient to perform recursion on the term (one of a and b) with lower rank if the ranks differ. The algorithm always performs one comparison (on root constructors) and then processes the terms of the lower rank (i.e. of the rank below min(|a|, |b|)). Since there are Σ#T(min(|a|, |b|)-1) possible such terms, the lexicographical comparison reduces to utmost (1 + Σ#T(min(|a|, |b|)-1)) constructor comparisons, hence it's decidable. Note that this bound is optimal, i.e. exact for some a and b in certain type families.

The function O: Nat->Nat that maps n-th term (by natural ordering) to the number of elements below n w.r.t. lexicographic ordering among first n elements by natural ordering. This function contains all information about the type family and lexicographic order on it up to homotopical equivalence. We even can recover signatures of the constructors.