Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

ΠΣ-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|
(Conway addition and multiplication).
We also conjecture that this relation still holds also when one allows for step with internal recursion.
Subscribe

  • (no subject)

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

  • Прогресс

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

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

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

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments