~/talk

Tests, Derivations, Proofs

Talkat Functional Conf 2017 · 2017-11-16..11-19· [functional-programming]
name:Roger Hui
links:none on file
slides:none on file

Uses APL and a custom assert utility to express executable assertions that fully specify correctness: tests for the Diamond Cutter check shape (2n+1 by 2n+1 or 0×0), vertical and horizontal symmetry, quadrant diagonals and off‑diagonals. Tests on the transpose primitive derive the shape formula (grouped by sorted indices) and a terse index‑based implementation with rank = 1+max(X). Derives and verifies recursive 2×2 block inverses, a Cholesky block algorithm, a linear‑time sum proof, and characterizes Ackermann growth experimentally.

AI-written summary · about

  1. 0:00Start
  2. 4:06Solution in Apl
  3. 23:51Proofs
  4. 31:02Inverting a Triangular Matrix
  5. 39:59Prove the Lemma
~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.