λ-calculus tuple rotl problem

tuple_rotl.txt

Implement a λ-Term named `rotL` that, when applied to a function F, a Church Nat
N, and a Church N-Tuple, returns the same Church N-Tuple, but with elements
shifted left. In other words, create a generic 'rotL<N,F,t>' function for
N-tuples. Example:
- (rotL λf.λx.(f (f x))     λt.(t 1 2))   == λt.(t 2 1)
- (rotL λf.λx.(f (f (f x))) λt.(t 1 2 3)) == λt.(t 2 3 1)
Your final answer must be a λ-Term that implements `rotL` correctly, as follows:
@rotL = term_here

NOTE: Don't omit parenthesis. Each application requires them. Example:
- WRONG: λf. λx. f (f x)
- RIGHT: λf. λx. (f (f x))
- WRONG: (λx. f x) λx.x
- RIGHT: (λx.(f x) λx.x)
- WRONG: λf. λx. λy. (f x y)
- RIGHT: λf. λx. λy. ((f x) y)

ANSWER:

oh that certainly matters, specially if the solution is identical. thanks for bringing my attention to it

take 1. Runnable as bin anywhere

=== Lambda Calculus Reducer ===
(λx.x) y → y [1]
(λx.xx)(λy.y) → (λy.y) [2]
PLUS 2 3 → (λf.(λx.(f (f (f (f (f x))))))) [21] ← Church 5
MULT 2 3 → (λf.(λx.(f (f (f (f (f (f x)))))))) [31] ← Church 6
SUCC 0 → (λf.(λx.(f x))) [3] ← Church 1

package main

import "fmt"

type Term interface{ String() string }
type Var struct{ N string }
type Abs struct{ P string; B Term }
type App struct{ F, A Term }

func (v *Var) String() string { return v.N }
func (a *Abs) String() string { return fmt.Sprintf("(λ%s.%s)", a.P, a.B) }
func (p *App) String() string { return fmt.Sprintf("(%s %s)", p.F, p.A) }

func sub(t Term, n string, r Term) Term {
  switch v := t.(type) {
  case *Var:
  	if v.N == n { return clone(r) }
  	return v
  case *Abs:
  	if v.P == n { return v }
  	return &Abs{v.P, sub(v.B, n, r)}
  case *App:
  	return &App{sub(v.F, n, r), sub(v.A, n, r)}
  }
  return t
}

func clone(t Term) Term {
  switch v := t.(type) {
  case *Var: return &Var{v.N}
  case *Abs: return &Abs{v.P, clone(v.B)}
  case *App: return &App{clone(v.F), clone(v.A)}
  }
  return t
}

func step(t Term) (Term, bool) {
  switch v := t.(type) {
  case *Var: return v, false
  case *Abs:
  	if b, ok := step(v.B); ok { return &Abs{v.P, b}, true }
  	return v, false
  case *App:
  	if a, ok := v.F.(*Abs); ok { return sub(a.B, a.P, v.A), true } // β-reduce!
  	if f, ok := step(v.F); ok { return &App{f, v.A}, true }
  	if a, ok := step(v.A); ok { return &App{v.F, a}, true }
  	return v, false
  }
  return t, false
}

func reduce(t Term, max int) (Term, int) {
  for i := 0; i < max; i++ {
  	if r, ok := step(t); ok { t = r } else { return t, i }
  }
  return t, max
}

// Church numerals: 0 = λf.λx.x, SUCC = λn.λf.λx.f(n f x)
func church(n int) Term {
  if n == 0 { return &Abs{"f", &Abs{"x", &Var{"x"}}} }
  return &App{succ(), church(n - 1)}
}
func succ() Term {
  return &Abs{"n", &Abs{"f", &Abs{"x", &App{&Var{"f"}, &App{&App{&Var{"n"}, &Var{"f"}}, &Var{"x"}}}}}}
}
func plus() Term { // PLUS = λm.λn.λf.λx. m f (n f x)
  return &Abs{"m", &Abs{"n", &Abs{"f", &Abs{"x",
  	&App{&App{&Var{"m"}, &Var{"f"}}, &App{&App{&Var{"n"}, &Var{"f"}}, &Var{"x"}}}}}}}
}
func mult() Term { // MULT = λm.λn.λf. m (n f)
  return &Abs{"m", &Abs{"n", &Abs{"f", &App{&Var{"m"}, &App{&Var{"n"}, &Var{"f"}}}}}}
}

func main() {
  fmt.Println("=== Lambda Calculus Reducer ===")
  run := func(name string, t Term, m int) { r, s := reduce(t, m); fmt.Printf("%s → %s [%d]\n", name, r, s) }
  run("(λx.x) y", &App{&Abs{"x", &Var{"x"}}, &Var{"y"}}, 10)
  run("(λx.xx)(λy.y)", &App{&Abs{"x", &App{&Var{"x"}, &Var{"x"}}}, &Abs{"y", &Var{"y"}}}, 10)
  run("PLUS 2 3", &App{&App{plus(), church(2)}, church(3)}, 100)
  run("MULT 2 3", &App{&App{mult(), church(2)}, church(3)}, 100)
  run("SUCC 0", &App{succ(), church(0)}, 50)
}