Factorial in Stella implemented N ways

In this file, we implement factorial in Stella in multiple different ways.

Very Purely Functional

language core;

// a constant function, specialized to Nat
fn Nat2Nat::const(f : fn(Nat) -> Nat) -> (fn(Nat) -> (fn(Nat) -> Nat)) {
  return fn(x : Nat) { return f }
}

// addition of natural numbers
fn Nat::add(n : Nat) -> (fn(Nat) -> Nat) {
  return fn(m : Nat) {
    return Nat::rec(n, m, fn(i : Nat) {
      return fn(r : Nat) { return succ(r) } })
  }
}

// multiplication of natural numbers
fn Nat::mul(n : Nat) -> (fn(Nat) -> Nat) {
  return fn(m : Nat) {
    return Nat::rec(n, 0, Nat2Nat::const(Nat::add(m)))
  }
}

// factorial via primitive recursion
fn factorial(n : Nat) -> Nat {
  return Nat::rec(n, succ(0), fn(i : Nat) {
    return fn(r : Nat) {
    return Nat::mul(r)(succ(i))  // r := r * (i + 1)
  } })
}

fn main(n : Nat) -> Nat {
  return factorial(n)
}

Factorial with In-Place Total Updates

language core;

extend with
  #unit-type,
  #references,
  #arithmetic-operators,
  #sequencing,
  #natural-literals;

fn helper(ref : &Nat) -> fn(Nat) -> Nat {
  return
    ref := 1;
    fn(n : Nat) {
      return
        Nat::rec(n, unit, fn(i : Nat) {
          return fn(r : Unit) {
            return ref := succ(i) * (*ref)
          }
        });
        (*ref)
    }
}

fn factorial(n : Nat) -> Nat {
  return helper(new(0))(n)
}

fn main(n : Nat) -> Nat {
  return factorial(n)
}

Factorial with In-Place Total Updates (let-version)

language core;

extend with
  #unit-type,
  #references,
  #arithmetic-operators,
  #sequencing,
  #natural-literals,
  #let-bindings;

fn factorial(n : Nat) -> Nat {
  return
    let ref = new(1) in
    (Nat::rec(n, unit, fn(i : Nat) {
      return fn(r : Unit) {
        return ref := succ(i) * (*ref)
      }
    });
    (*ref))
}

fn main(n : Nat) -> Nat {
  return factorial(n)
}

Factorial with Covered Recursion via a Reference

language core;

extend with
  #references,
  #arithmetic-operators,
  #sequencing,
  #natural-literals;

fn factorial(f : &(fn(Nat) -> Nat)) -> fn(Nat) -> Nat {
  return fn(n : Nat) {
    return
      f := fn(x : Nat) { return if Nat::iszero(x) then 1 else x * (*f)(x - 1)} ;
      (*f)(n)
  }
}

fn main(n : Nat) -> Nat {
  return factorial(new(fn(x : Nat) { return x }))(n)
}