## General recursion

https://dannypsnl.me/hami2023

## LFX Mentorship

https://github.com/WasmEdge/WasmEdge https://lfx.linuxfoundation.org/tools/mentorship

## me

sourcehut: sr.ht/~dannypsnl
blog: dannypsnl.me
email: ~dannypsnl/[email protected]

## What is recursion?

Recursion is if $$f$$ occurs both side

$\begin{cases} f(0) = 1 \\ f(n+1) = (n + 1) \times f(n) \end{cases}$
How to find such a recursive function $$f : \N \to \N$$?
Consider a function $$\bot$$, such that undefined on all inputs
And a higher-order function $F : (\N \to \N) \to (\N \to \N)$ , such that improves a given function $$g$$ to a better function $$g'$$, a better function is closer to the target function $$f$$.
Notice a requirement about $$F$$ is the output $$g$$ must satisfy $g(n) = c \implies f(n) = c$

#### Theorem. target function $$f$$ is a fixed point of $$F$$

$f = F(f)$ We also denote $$f = fix(F)$$
What's a function closer to target?

#### Closer means that a function has definition on more inputs

• $$F(\bot)$$ has definition on $$0 \to N$$ for a conrete number $$N$$
• $$F(F(\bot))$$ has definition on $$0 \to M$$ where $$M > N$$
• and so on
Start from $$\bot$$ and repeatly apply $$F$$ forms a series of functions $\bot, F(\bot), F^2(\bot), F^3(\bot), \dots$
We can define a limit for a series! $\lim_{n \to \infty} F^n(\bot)$

#### Theorem. limit of the series is a fixed point (target)

$\lim_{n \to \infty} F^n(\bot) = fix(F)$
A proper functional for this is $F(f)(n) = \begin{cases} 1 \quad \text{if } n = 0 \\ n \times f(n-1) \quad \text{if } n > 0 \end{cases}$
General recursion: doing this for any recursive definition we have.
For example, a higher-order recursive function $F : (\N \to \N) \to (\N \to \N)$ can be determined by a more higher-order function $((\N \to \N) \to (\N \to \N)) \\ \to ((\N \to \N) \to (\N \to \N))$

#### Theorem. general recursion is Turing computable

Can we interpret Turing computable via general recursion?

#### Almost, but need algebra on lambda calculus.

• $$\alpha$$ conversion
• $$\eta$$ conversion
• $$\beta$$ conversion
Further issue (denotational semantic) $(X \subset \N^\N) \cong \N$ is not topological trivial, naïve set-theoretic semantic failed.
• Dana Scott, Domain theory (1960s)
• Lawvere's fixed point theorem (1969)

#### 資訊發展方向的基礎技能

• 基本 git 操作，如何用 send-email 送出 patch
• 至少了解一種 Architecture of a concrete machine: RISCV, x86-64, AArch
• 初步了解 Distributed system：了解至少一種網路協定，並知道 CAP conjecture
• 對計算理論有足夠的了解：Turing theorem, Gödel incompleteness, and Tarski universe