General recursion

https://dannypsnl.me/hami2023

company

company logo secondstate

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)
問題回答

讀書方法

看卡片盒筆記（How to take smart notes）

職場選擇

看做自己的生命設計師（Designing your life）

資訊發展方向的基礎技能

  • 基本 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