# ΠΣ-calculus as foundation for ordinal complexity analysis

The nice thing about ΠΣ-calculus is that everything is explicit there. For example, recursive datatypes are defined with Rec in their definition, and values of these datatypes must contain a "fold" constructor every time recursiveness of their type is made use of.

This allows us to define a major Nat-valued property for normalizable values:
Structural complexity |t| of a term t is the number of "fold" constructor usages in its normal form. Note that memory footprint of a term t is always O(|t|). For a type T let's denote by T[n] a set of terms of type t with structural complexity of utmost n.

For a function f: A -> B we can always determine it's structural boost function
||f|| = (n: Nat) => max {|f(t)| | t : A[n]},
i.e. how much it can maximally increase the structural complexity of its argument. Since every total function Nat -> Nat is majored by some function from the canonical Hardy hierarchy H_o(n), we can find the minimal such ordinal o that ||f||(n) ≤ H_o(n) (at least at one point they would coincide), we'll call it complexity ordinal |f| of the function f.

(Canonical) Examples:
|id| = ω
|n: Nat => n + 1| = ω + 1
|n: Nat => n + 2| = ω + 2
|n: Nat => n + n| = ω·2
|n: Nat => n + n + n| = ω·3
|n: Nat => (n choose p)| = ωp

It's not hard to see that for a function that is completely nonrecursive (not recursive and makes no use of other recursive function, the boost function is O(1): structural complexity is decremented whenever you use unfold, incremented whenever you use fold, sum'ed when you construct a pair, max'ed when you perform choice and remains unaffected by all other constructions of ΠΣ. Their complexity ordinals are therefore of the form ω·n + c. If a function uses every variable utmost once, it is a function of constant boost, i.e. it's ||f|| is bounded by x => x + c for some constant c.

A recursive function f: A -> B can be always defined as
f = finalize . (fix step) . init
where fix is a fixed point combinator and the functions
init: A -> I
step: I -> I
finalize : I -> B
are completely nonrecursive. The function f is total iff the preorder P induced on the type I by applications of the step function is well-founded. We'll show that
|f| = P⨳|step| ⧺ |init| ⧺ |finalize|
We also conjecture that this relation still holds also when one allows for step with internal recursion.
• #### (no subject)

Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

• #### Прогресс

Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

• #### О водосбережении

Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

• Post a new comment

#### Error

default userpic