Interaction Calculus .prompt

interaction_calculus.prompt

# The Interaction Calculus

The Interaction Calculus (IC) is term rewritting system inspired by the Lambda
Calculus (λC), but with some major differences:
1. Vars are affine: they can only occur up to one time.
2. Vars are global: they can occur anywhere in the program.
3. There is a new core primitive: the superposition.

An IC term is defined by the following grammar:

```
Term ::=
  | VAR: Name
  | LAM: "λ" Name "." Term
  | APP: "(" Term " " Term ")"
  | SUP: "{" Term "," Term "}"
  | DUP: "!" "{" Name "," Name "}" "=" Term ";" Term
```

Where:
- VAR represents a named variable.
- LAM represents a lambda.
- APP represents a application.
- SUP represents a superposition.
- DUP represents a duplication.

Lambdas are curried, and work like their λC counterpart, except with a relaxed
scope, and with affine usage. Applications eliminate lambdas, like in λC,
through the beta-reduce (APP-LAM) interaction.

Superpositions work like pairs. Duplications eliminate superpositions through
the collapse (DUP-SUP) interaction, which works exactly like a pair projection.

What makes SUPs and DUPs unique is how they interact with LAMs and APPs. When a
SUP is applied to an argument, it reduces through the overlap interaction
(APP-SUP), and when a LAM is projected, it reduces through the entangle
interaction (DUP-LAM). This gives a computational behavior for every possible
interaction: there are no runtime errors on IC.

The interaction rules are defined below:

Beta-Reduce:

```
(λx.f a)
-------- APP-LAM
x <- a
f
```

Overlap:

```
({a,b} c)
--------------- APP-SUP
! {x0,x1} = c;
{(a x0),(b x1)}
```

Entangle:

```
! {r,s} = λx.f;
K
--------------- DUP-LAM
r <- λx0.f0
s <- λx1.f1
x <- {x0,x1}
! {f0,f1} = f;
K
```

Collapse:

```
! {x,y} = {a,b};
K
--------------- DUP-SUP
x <- a
y <- b
K
```

Where `x <- t` stands for a global substitution of `x` by `t`.

Since variables are affine, substitutions can be implemented efficiently by just
inserting an entry in a global substitution map (`sub[var] = value`). There is
no need to traverse the target term, or to handle name capture, as long as fresh
variable names are globally unique. It can also be implemented in a concurrent
setup with a single atomic-swap.

Below is a pseudocode implementation of these interaction rules:

```
def app_lam(app, lam):
  sub[lam.nam] = app.arg
  return lam.bod

def app_sup(app, sup):
  x0 = fresh()
  x1 = fresh()
  a0 = App(sup.fst, Var(x0))
  a1 = App(Sup.snd, Var(x1))
  return Dup(x0, x1, app.arg, Sup(a0, a1))

def dup_lam(dup, lam):
  x0 = fresh()
  x1 = fresh()
  f0 = fresh()
  f1 = fresh()
  sub[dup.fst] = Lam(x0, Var(f0))
  sub[dup.snd] = Lam(x1, Var(f1))
  sub[lam.nam] = Sup(Var(x0), Var(x1))
  return Dup(f0, f1, lam.bod, dup.bod)

def dup_sup(dup, sup):
  sub[dup.fst] = sup.fst
  sub[dup.snd] = sup.snd
  return dup.bod
```

Terms can be reduced to weak head normal form, which means reducing until the
outermost constructor is a value (LAM, SUP, etc.), or until no more reductions
are possible. Example:

```
def whnf(term):
  while True:
    match term:
      case Var(nam):
        if nam in sub:
          term = sub[nam]
        else:
          return term
      case App(fun, arg):
        fun = whnf(fun)
        match fun:
          case Lam(_, _):
            term = app_lam(term, fun)
          case Sup(_, _):
            term = app_sup(term, fun)
          case _:
            return App(fun, arg)
      case Dup(fst, snd, val, bod):
        val = whnf(val)
        match val:
          case Lam(_, _):
            term = dup_lam(term, val)
          case Sup(_, _):
            term = dup_sup(term, val)
          case _:
            return Dup(fst, snd, val, bod)
      case _:
        return term
```

Terms can be reduced to full normal form by recursively taking the whnf:

```
def normal(term):
  term = whnf(term)
  match term:
    case Lam(nam, bod):
      bod_nf = normal(bod)
      return Lam(nam, bod_nf)
    case App(fun, arg):
      fun_nf = normal(fun)
      arg_nf = normal(arg)
      return App(fun_nf, arg_nf)
    case Sup(fst, snd):
      fst_nf = normal(fst)
      snd_nf = normal(snd)
      return Sup(fst_nf, snd_nf)
    case Dup(fst, snd, val, bod):
      val_nf = normal(val)
      bod_nf = normal(bod)
      return Dup(fst, snd, val_nf, bod_nf)
    case _:
      return term
```

Below are some normalization examples.

Example 0: (simple λ-term)

```
(λx.λt.(t x) λy.y)
------------------ APP-LAM
λt.(t λy.y)
```

Example 1: (larger λ-term)

```
(λb.λt.λf.((b f) t) λT.λF.T)
---------------------------- APP-LAM
λt.λf.((λT.λF.T f) t)
----------------------- APP-LAM
λt.λf.(λF.t f)
-------------- APP-LAM
λt.λf.t
```

Example 2: (global scopes)

```
{x,(λx.λy.y λk.k)}
------------------ APP-LAM
{λk.k,λy.y}
```

Example 3: (superposition)

```
!{a,b} = {λx.x,λy.y}; (a b)
--------------------------- DUP-SUP
(λx.x λy.y)
----------- APP-LAM
λy.y
```

Example 4: (overlap)

```
({λx.x,λy.y} λz.z)
------------------ APP-SUP  
! {x0,x1} = λz.z; {(λx.x x0),(λy.y x1)}  
--------------------------------------- DUP-LAM  
! {f0,f1} = {r,s}; {(λx.x λr.f0),(λy.y λs.f1)}  
---------------------------------------------- DUP-SUP  
{(λx.x λr.r),(λy.y λs.s)}  
------------------------- APP-LAM  
{λr.r,(λy.y λs.s)}  
------------------ APP-LAM  
{λr.r,λs.s}  
```

---

TODO: based on the spec above, create a complete TypeScript implementation of
the Interaction Calculus. Include a stringifier, a parser, and an evaluator. It
must work as a CLI tool that receives a IC term as the argument, and outputs its
normal form, as well as the interaction count. Make the parser single-pass and
recursive, without a separate tokenizer. Use JSON to represent ADTs, as in
`{$:"Cons",head,tail}`. Make the file concise, simple and purely functional,
except for the fresh count, interaction count, and the subst map, which can be
global states. Answer below with a complete TS implementation of the IC.

Sonnet-3.7 generation:

#!/usr/bin/env bun

// Type definitions for the Interaction Calculus terms
type Term = 
  | { $: "Var", nam: string }
  | { $: "Lam", nam: string, bod: Term }
  | { $: "App", fun: Term, arg: Term }
  | { $: "Sup", fst: Term, snd: Term }
  | { $: "Dup", fst: string, snd: string, val: Term, bod: Term };

// Global state
let freshCount = 0;
let interactionCount = 0;
const sub: Record<string, Term> = {};

// Helper to create fresh variable names
function fresh(): string {
  return `#${freshCount++}`;
}

// Interactions
function appLam(app: Term): Term {
  if (app.$ !== "App" || app.fun.$ !== "Lam") {
    throw new Error("appLam: not an application of a lambda");
  }

  interactionCount++;
  sub[app.fun.nam] = app.arg;
  return app.fun.bod;
}

function appSup(app: Term): Term {
  if (app.$ !== "App" || app.fun.$ !== "Sup") {
    throw new Error("appSup: not an application of a superposition");
  }

  interactionCount++;
  const x0 = fresh();
  const x1 = fresh();
  const a0 = { $: "App", fun: app.fun.fst, arg: { $: "Var", nam: x0 } } as Term;
  const a1 = { $: "App", fun: app.fun.snd, arg: { $: "Var", nam: x1 } } as Term;
  return { $: "Dup", fst: x0, snd: x1, val: app.arg, bod: { $: "Sup", fst: a0, snd: a1 } } as Term;
}

function dupLam(dup: Term): Term {
  if (dup.$ !== "Dup" || dup.val.$ !== "Lam") {
    throw new Error("dupLam: not a duplication of a lambda");
  }

  interactionCount++;
  const x0 = fresh();
  const x1 = fresh();
  const f0 = fresh();
  const f1 = fresh();
  sub[dup.fst] = { $: "Lam", nam: x0, bod: { $: "Var", nam: f0 } } as Term;
  sub[dup.snd] = { $: "Lam", nam: x1, bod: { $: "Var", nam: f1 } } as Term;
  sub[dup.val.nam] = { $: "Sup", fst: { $: "Var", nam: x0 }, snd: { $: "Var", nam: x1 } } as Term;
  return { $: "Dup", fst: f0, snd: f1, val: dup.val.bod, bod: dup.bod } as Term;
}

function dupSup(dup: Term): Term {
  if (dup.$ !== "Dup" || dup.val.$ !== "Sup") {
    throw new Error("dupSup: not a duplication of a superposition");
  }

  interactionCount++;
  sub[dup.fst] = dup.val.fst;
  sub[dup.snd] = dup.val.snd;
  return dup.bod;
}

// Normalization
function whnf(term: Term): Term {
  while (true) {
    switch (term.$) {
      case "Var":
        if (term.nam in sub) {
          term = sub[term.nam];
        } else {
          return term;
        }
        break;
      case "App": {
        const fun = whnf(term.fun);
        if (fun.$ === "Lam") {
          term = appLam({ $: "App", fun, arg: term.arg } as Term);
        } else if (fun.$ === "Sup") {
          term = appSup({ $: "App", fun, arg: term.arg } as Term);
        } else {
          return { $: "App", fun, arg: term.arg } as Term;
        }
        break;
      }
      case "Dup": {
        const val = whnf(term.val);
        if (val.$ === "Lam") {
          term = dupLam({ $: "Dup", fst: term.fst, snd: term.snd, val, bod: term.bod } as Term);
        } else if (val.$ === "Sup") {
          term = dupSup({ $: "Dup", fst: term.fst, snd: term.snd, val, bod: term.bod } as Term);
        } else {
          return { $: "Dup", fst: term.fst, snd: term.snd, val, bod: term.bod } as Term;
        }
        break;
      }
      default:
        return term;
    }
  }
}

function normal(term: Term): Term {
  term = whnf(term);
  switch (term.$) {
    case "Lam": {
      const lamBodNf = normal(term.bod);
      return { $: "Lam", nam: term.nam, bod: lamBodNf } as Term;
    }
    case "App": {
      const funNf = normal(term.fun);
      const argNf = normal(term.arg);
      return { $: "App", fun: funNf, arg: argNf } as Term;
    }
    case "Sup": {
      const fstNf = normal(term.fst);
      const sndNf = normal(term.snd);
      return { $: "Sup", fst: fstNf, snd: sndNf } as Term;
    }
    case "Dup": {
      const valNf = normal(term.val);
      const dupBodNf = normal(term.bod);
      return { $: "Dup", fst: term.fst, snd: term.snd, val: valNf, bod: dupBodNf } as Term;
    }
    default:
      return term;
  }
}

// Stringifier
function stringify(term: Term): string {
  switch (term.$) {
    case "Var":
      return term.nam;
    case "Lam":
      return `λ${term.nam}.${stringify(term.bod)}`;
    case "App":
      return `(${stringify(term.fun)} ${stringify(term.arg)})`;
    case "Sup":
      return `{${stringify(term.fst)},${stringify(term.snd)}}`;
    case "Dup":
      return `!{${term.fst},${term.snd}} = ${stringify(term.val)}; ${stringify(term.bod)}`;
    default:
      return ""; // This should never happen
  }
}

// Parser
function parse(code: string): Term {
  let pos = 0;

  function skipWhitespace() {
    while (pos < code.length && /\s/.test(code[pos])) {
      pos++;
    }
  }

  function parseName(): string {
    skipWhitespace();
    let name = "";
    while (pos < code.length && /[a-zA-Z0-9_#]/.test(code[pos])) {
      name += code[pos++];
    }
    if (name.length === 0) {
      throw new Error(`Expected name at position ${pos}`);
    }
    return name;
  }

  function parseVar(): Term {
    const name = parseName();
    return { $: "Var", nam: name } as Term;
  }

  function parseLam(): Term {
    skipWhitespace();
    if (code.charAt(pos) === "λ") {
      pos++; // skip λ
    } else if (code.charAt(pos) === "\\" && (pos + 1 >= code.length || code.charAt(pos + 1) !== "\\")) {
      pos++; // allow \ as an alternative to λ
    } else {
      throw new Error(`Expected 'λ' or '\\', found '${code.charAt(pos)}' at position ${pos}`);
    }
    const name = parseName();
    skipWhitespace();
    if (pos >= code.length || code[pos] !== '.') {
      throw new Error(`Expected '.', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip .
    const bod = parseTerm();
    return { $: "Lam", nam: name, bod } as Term;
  }

  function parseApp(): Term {
    skipWhitespace();
    pos++; // skip (
    const fun = parseTerm();
    skipWhitespace();
    const arg = parseTerm();
    skipWhitespace();
    if (pos >= code.length || code[pos] !== ')') {
      throw new Error(`Expected ')', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip )
    return { $: "App", fun, arg } as Term;
  }

  function parseSup(): Term {
    skipWhitespace();
    pos++; // skip {
    const fst = parseTerm();
    skipWhitespace();
    if (pos >= code.length || code[pos] !== ',') {
      throw new Error(`Expected ',', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip ,
    skipWhitespace();
    const snd = parseTerm();
    skipWhitespace();
    if (pos >= code.length || code[pos] !== '}') {
      throw new Error(`Expected '}', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip }
    return { $: "Sup", fst, snd } as Term;
  }

  function parseDup(): Term {
    skipWhitespace();
    pos++; // skip !
    if (pos >= code.length || code[pos] !== '{') {
      throw new Error(`Expected '{', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip {
    const fst = parseName();
    skipWhitespace();
    if (pos >= code.length || code[pos] !== ',') {
      throw new Error(`Expected ',', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip ,
    skipWhitespace();
    const snd = parseName();
    skipWhitespace();
    if (pos >= code.length || code[pos] !== '}') {
      throw new Error(`Expected '}', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip }
    skipWhitespace();
    if (pos >= code.length || code[pos] !== '=') {
      throw new Error(`Expected '=', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip =
    skipWhitespace();
    const val = parseTerm();
    skipWhitespace();
    if (pos >= code.length || code[pos] !== ';') {
      throw new Error(`Expected ';', found '${pos < code.length ? code[pos] : "EOF"}' at position ${pos}`);
    }
    pos++; // skip ;
    skipWhitespace();
    const bod = parseTerm();
    return { $: "Dup", fst, snd, val, bod } as Term;
  }

  function parseTerm(): Term {
    skipWhitespace();
    if (pos >= code.length) {
      throw new Error("Unexpected end of input");
    }
    switch (code[pos]) {
      case 'λ':
      case '\\':
        return parseLam();
      case '(':
        return parseApp();
      case '{':
        return parseSup();
      case '!':
        return parseDup();
      default:
        return parseVar();
    }
  }

  const term = parseTerm();
  skipWhitespace();
  if (pos < code.length) {
    throw new Error(`Unexpected token '${code[pos]}' at position ${pos}`);
  }
  return term;
}

// Main function
function main() {
  const args = process.argv.slice(2);
  if (args.length === 0) {
    console.error("Usage: node ic.js <term>");
    process.exit(1);
  }

  const input = args.join(" ");
  try {
    // Reset the global state
    freshCount = 0;
    interactionCount = 0;
    Object.keys(sub).forEach(key => delete sub[key]);

    const term = parse(input);
    const result = normal(term);
    console.log(`Normal form: ${stringify(result)}`);
    console.log(`Interactions: ${interactionCount}`);
  } catch (error) {
    console.error(`Error: ${error instanceof Error ? error.message : String(error)}`);
    process.exit(1);
  }
}

main();

Grok-3 generation:

#!/usr/bin/env bun

// Interaction Calculus (IC) Implementation in TypeScript

// Term Representation using JSON-like ADTs
type Term =
  | { $: "Var"; name: string }
  | { $: "Lam"; param: string; body: Term }
  | { $: "App"; func: Term; arg: Term }
  | { $: "Sup"; left: Term; right: Term }
  | { $: "Dup"; leftVar: string; rightVar: string; value: Term; body: Term };

// Global States
const sub = new Map<string, Term>();
let freshCount = 0;
let interactionCount = 0;

// Fresh Variable Generation
function fresh(): string {
  return `v${freshCount++}`;
}

// Interaction Rules
function app_lam(app: { $: "App"; func: Term; arg: Term }, lam: { $: "Lam"; param: string; body: Term }): Term {
  sub.set(lam.param, app.arg);
  interactionCount++;
  return lam.body;
}

function app_sup(app: { $: "App"; func: Term; arg: Term }, sup: { $: "Sup"; left: Term; right: Term }): Term {
  const x0 = fresh();
  const x1 = fresh();
  const a0: Term = { $: "App", func: sup.left, arg: { $: "Var", name: x0 } };
  const a1: Term = { $: "App", func: sup.right, arg: { $: "Var", name: x1 } };
  interactionCount++;
  return { $: "Dup", leftVar: x0, rightVar: x1, value: app.arg, body: { $: "Sup", left: a0, right: a1 } };
}

function dup_lam(dup: { $: "Dup"; leftVar: string; rightVar: string; value: Term; body: Term }, lam: { $: "Lam"; param: string; body: Term }): Term {
  const x0 = fresh();
  const x1 = fresh();
  const f0 = fresh();
  const f1 = fresh();
  sub.set(dup.leftVar, { $: "Lam", param: x0, body: { $: "Var", name: f0 } });
  sub.set(dup.rightVar, { $: "Lam", param: x1, body: { $: "Var", name: f1 } });
  sub.set(lam.param, { $: "Sup", left: { $: "Var", name: x0 }, right: { $: "Var", name: x1 } });
  interactionCount++;
  return { $: "Dup", leftVar: f0, rightVar: f1, value: lam.body, body: dup.body };
}

function dup_sup(dup: { $: "Dup"; leftVar: string; rightVar: string; value: Term; body: Term }, sup: { $: "Sup"; left: Term; right: Term }): Term {
  sub.set(dup.leftVar, sup.left);
  sub.set(dup.rightVar, sup.right);
  interactionCount++;
  return dup.body;
}

// Weak Head Normal Form (WHNF)
function whnf(term: Term): Term {
  while (true) {
    switch (term.$) {
      case "Var":
        const name = term.name;
        if (sub.has(name)) term = sub.get(name)!;
        else return term;
        break;
      case "App":
        const fun = whnf(term.func);
        if (fun.$ === "Lam") term = app_lam(term, fun as { $: "Lam"; param: string; body: Term });
        else if (fun.$ === "Sup") term = app_sup(term, fun as { $: "Sup"; left: Term; right: Term });
        else return { $: "App", func: fun, arg: term.arg };
        break;
      case "Dup":
        const val = whnf(term.value);
        if (val.$ === "Lam") term = dup_lam(term, val as { $: "Lam"; param: string; body: Term });
        else if (val.$ === "Sup") term = dup_sup(term, val as { $: "Sup"; left: Term; right: Term });
        else return { $: "Dup", leftVar: term.leftVar, rightVar: term.rightVar, value: val, body: term.body };
        break;
      default:
        return term;
    }
  }
}

// Full Normal Form
function normal(term: Term): Term {
  term = whnf(term);
  switch (term.$) {
    case "Lam":
      return { $: "Lam", param: term.param, body: normal(term.body) };
    case "App":
      return { $: "App", func: normal(term.func), arg: normal(term.arg) };
    case "Sup":
      return { $: "Sup", left: normal(term.left), right: normal(term.right) };
    case "Dup":
      return { $: "Dup", leftVar: term.leftVar, rightVar: term.rightVar, value: normal(term.value), body: normal(term.body) };
    default:
      return term;
  }
}

// Parser
function skipWhitespace(input: string, index: number): number {
  while (index < input.length && /\s/.test(input[index])) index++;
  return index;
}

function readName(input: string, index: number): [string, number] {
  if (index >= input.length || !/[a-zA-Z]/.test(input[index])) throw new Error("Expected a name");
  let name = input[index];
  index++;
  while (index < input.length && /[a-zA-Z0-9]/.test(input[index])) name += input[index++];
  return [name, index];
}

function parseTerm(input: string, index: number): [Term, number] {
  index = skipWhitespace(input, index);
  if (index >= input.length) throw new Error("Unexpected end of input");
  const char = input[index];
  if (/[a-zA-Z]/.test(char)) {
    const [name, newIndex] = readName(input, index);
    return [{ $: "Var", name }, newIndex];
  } else if (char === 'λ') {
    index++;
    const [param, newIndex] = readName(input, index);
    index = skipWhitespace(input, newIndex);
    if (input[index] !== '.') throw new Error("Expected '.' after lambda parameter");
    const [body, finalIndex] = parseTerm(input, index + 1);
    return [{ $: "Lam", param, body }, finalIndex];
  } else if (char === '(') {
    const [func, newIndex] = parseTerm(input, index + 1);
    index = skipWhitespace(input, newIndex);
    const [arg, finalIndex] = parseTerm(input, index);
    index = skipWhitespace(input, finalIndex);
    if (input[index] !== ')') throw new Error("Expected ')' to close application");
    return [{ $: "App", func, arg }, index + 1];
  } else if (char === '{') {
    const [left, newIndex] = parseTerm(input, index + 1);
    index = skipWhitespace(input, newIndex);
    if (input[index] !== ',') throw new Error("Expected ',' in superposition");
    const [right, finalIndex] = parseTerm(input, index + 1);
    index = skipWhitespace(input, finalIndex);
    if (input[index] !== '}') throw new Error("Expected '}' to close superposition");
    return [{ $: "Sup", left, right }, index + 1];
  } else if (char === '!') {
    index++;
    if (input[index] !== '{') throw new Error("Expected '{' after '!' in duplication");
    const [leftVar, newIndex] = readName(input, index + 1);
    index = skipWhitespace(input, newIndex);
    if (input[index] !== ',') throw new Error("Expected ',' in duplication variables");
    const [rightVar, nextIndex] = readName(input, index + 1);
    index = skipWhitespace(input, nextIndex);
    if (input[index] !== '}') throw new Error("Expected '}' to close duplication variables");
    index = skipWhitespace(input, index + 1);
    if (input[index] !== '=') throw new Error("Expected '=' in duplication");
    const [value, valIndex] = parseTerm(input, index + 1);
    index = skipWhitespace(input, valIndex);
    if (input[index] !== ';') throw new Error("Expected ';' in duplication");
    const [body, finalIndex] = parseTerm(input, index + 1);
    return [{ $: "Dup", leftVar, rightVar, value, body }, finalIndex];
  } else {
    throw new Error(`Unexpected character: ${char}`);
  }
}

function parse(input: string): Term {
  const [term, index] = parseTerm(input, 0);
  if (skipWhitespace(input, index) < input.length) throw new Error("Extra input after term");
  return term;
}

// Stringifier
function stringify(term: Term): string {
  switch (term.$) {
    case "Var": return term.name;
    case "Lam": return `λ${term.param}.${stringify(term.body)}`;
    case "App": return `(${stringify(term.func)} ${stringify(term.arg)})`;
    case "Sup": return `{${stringify(term.left)},${stringify(term.right)}}`;
    case "Dup": return `!{${term.leftVar},${term.rightVar}}=${stringify(term.value)};${stringify(term.body)}`;
  }
}

// CLI Integration
const input = process.argv[2];
if (!input) {
  console.error("Please provide an IC term as argument.");
  process.exit(1);
}
try {
  const term = parse(input);
  const normalForm = normal(term);
  console.log(stringify(normalForm));
  console.log(`Interaction count: ${interactionCount}`);
} catch (error) {
  console.error((error as Error).message);
  process.exit(1);
}

Test with:

./ic.ts "((λf.λx.\!{f0,f1}=f;(f0 (f1 x)) λB.λT.λF.((B F) T)) λa.λb.a)"

Should output a term equivalent to λa.λb.a, with an interaction count of 16.