Free general recursion

Stream: general

[Trebor Huang]

I made a quick Lean implementation of McBride's paper *Turing Completeness Totally Free*, which essentially treats general recursion as a side effect, wrapping it in a monad. Combined with the unchained do notation I find it very powerful. Perhaps we can replace some partial definition with these, so that we can reason about them.

TL; DR:

/-- Unsafe execution of general recursive function. -/
unsafe def execute (f : (s : S) ⌁ T s) (s : S) : T s

/- Example: Counting how many triplings are needed to put a number to 1
  step 1 = 0
  step k = step (k/2)       (k even)
  step k = 1 + step (3k+1)  (k odd)
-/

def step : (_ : Nat) ⌁ Nat := fun n => do
  if n <= 1 then
    return 0
  else if n % 2 = 0 then
    call (n / 2)  -- `call` represents the recursing function
  else
    return 1 + (← call (3 * n + 1))

-- Starting from 17, we need three triplings:
--  17 -> 52 ... 13 -> 40 ... 5 -> 16 ... 1
#eval execute step 17  -- 3

[Trebor Huang]

Full Code

/-- Type representing the computation process of a general recursive program.
`General S T X` represents a process that produces an `X`,
possibly requiring some calls to a function `(s : S) → T s` for help.
-/
inductive General (S : Sort u) (T : S → Sort u') (X : Sort u'') where
/-- Immediately produce a value. -/
| Return : X → General S T X
/-- Call the function, and describe what to do with the result. -/
| Call : (s : S) → (T s → General S T X) → General S T X
namespace General

def fold {Y : Type _} (r : X → Y) (c : (s : S) → (T s → Y) → Y) :
  General S T X → Y
  | Return x => r x
  | Call s κ => c s fun t => fold r c (κ t)

-- Uhh weird universes help
instance : Monad (General.{u+1,u+1,u+1} S T) where
  pure := Return
  bind g k := fold k Call g

variable {S : Type u} {T : S -> Type u}

/-- Type of general recursive function. -/
def PiG {S : Sort u} (T : S -> Sort u') :=
  (s : S) → General S T (T s)

section  -- Syntax `(x : S) ⌁ T x`
open Lean
open TSyntax.Compat
macro:35 xs:bracketedExplicitBinders " ⌁ " b:term:35 : term => expandBrackedBinders ``PiG xs b
end

-- Explain later
def call : (s : S) ⌁ T s := (Call · Return)

def expand (f : (s : S) ⌁ T s) (g : General S T X) : General S T X
  := fold pure (f · >>= ·) g

/-- Unsafe execution of general recursive function. -/
unsafe def execute (f : (s : S) ⌁ T s) (s : S) : T s :=
  match f s with
  | Return x => x
  | _ => execute (fun s => expand f (f s)) s

/- Example: Counting how many triplings are needed to put a number to 1
  step 1 = 0
  step k = step (k/2)       (k even)
  step k = 1 + step (3k+1)  (k odd)
-/

def step : (_ : Nat) ⌁ Nat := fun n => do
  if n <= 1 then
    return 0
  else if n % 2 = 0 then
    call (n / 2)  -- `call` represents the recursing function
  else
    return 1 + (← call (3 * n + 1))

-- Starting from 17, we need three triplings:
--  17 -> 52 ... 13 -> 40 ... 5 -> 16 ... 1
#eval execute step 17  -- 3

[Trebor Huang]

A few questions:

• How can I solve that universe level issue in the middle? Writing the most general level seems to interfere with monad typeclass interference? (Or I messed up when calculating the levels)
• Can this be easily combined with the do notation so general recursion compiles to this monad?
• Is programming like this actually practical?

[Eric Wieser]

I think the universe weirdness is unavoidable, and it's a consequence of the monad framework (and as a result, do notation) not being (maximally) universe-polymorphic

[Eric Wieser]

Which is to say; there is no Monad.bind that can move from one universe to another.

[Eric Wieser]

But this has been discussed a bunch before in other threads

[Ioannis Konstantoulas]

Eric Wieser said:

But this has been discussed a bunch before in other threads

Unfortunately, thread discoverability is an issue, especially to new people who do not know what the right search keywords are. There are also no tags like in Q&A sites, and, honestly, Zulip search is slow (actually, Zulip is unusable on my Samsung phone).

[Eric Wieser]

Zulip search is very bad on mobile, but works on on desktop

[Eric Wieser]

Eric Wieser said:

Here's a discussion about changing the typeclasses to achieve that in Lean 3, and one about universe-polymorphic IO in Lean 4.