lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

Recursion.md (663B)


      1 +++
      2 title = "Recursion"
      3 +++
      4 
      5 # Recursion
      6 Let’s say you build a function for factorial, using applied lambda calculus (extra functions). For factorial — if x is 0, return 1, otherwise return `x × factorial (n-1)`
      7 
      8 Basic function:
      9 
     10 <pre>
     11 factorial := λx.(iszero x) c₁ (mult x (factorial (n-1)))
     12 </pre>
     13 
     14 The problem is, it has factorial in its definition. It can’t. So abstract it.
     15 
     16 <pre>
     17 factorial := (λa.λx.(iszero x) c₁ (mult x (a (n-1))) ) factorial
     18 </pre>
     19 
     20 We can then divide it into two parts:
     21 
     22 <pre>
     23 F := λa.λx.(iszero x) c₁ (mult x (a (n-1)))
     24 factorial := F factorial
     25 </pre>
     26 
     27 Then use a fixed point combinator.
     28 
     29 <pre>factorial := Y F</pre>