mathlib3 documentation

lean-ga / examples.recursors

Recursors in functional programming #

This file contains the examples from section 2 of "Computing with the universal properties of the Clifford algebra and the even subalgebra".

While these are not related to GA at all, they are valuable for building intuition for how to think about clifford_algebra.lift and clifford_algebra.fold, along with other more complex recursion schemes.

Some quick remarks about Lean syntax from those coming from the paper:

$f(a, b)$ or $f(a)(b)$ is written f a b
x ↦ f(x) is written λ x, f x.

def icacga.sum {R : Type u_1} [semiring R] :

Equations

icacga.sum (a :: l) = a + icacga.sum l
icacga.sum list.nil = 0

def icacga.accum_from {R : Type u_1} [semiring R] :

list R → R → list R

Equations

icacga.accum_from (b :: l) = λ (a : R), a :: icacga.accum_from l (a + b)
icacga.accum_from list.nil = λ (a : R), [a]

def icacga.accum {R : Type u_1} [semiring R] :

list R → list R

Equations

icacga.accum l = icacga.accum_from l 0

def icacga.rev_accum_aux {R : Type u_1} [semiring R] :

list R → R × list R

Equations

icacga.rev_accum_aux (a :: l) = icacga.rev_accum_aux._match_1 a (icacga.rev_accum_aux l)
icacga.rev_accum_aux list.nil = (0, list.nil R)
icacga.rev_accum_aux._match_1 a (b, l') = (a + b, b :: l')

def icacga.rev_accum {R : Type u_1} [semiring R] :

list R → list R

Equations

icacga.rev_accum l = icacga.rev_accum._match_1 (icacga.rev_accum_aux l)
icacga.rev_accum._match_1 (b, l') = b :: l'