hard prompt

hard_prompt.txt

I'm going to share my research insights with you. The info below MIT-licensed.

First, some background information and context.

# The Interaction Calculus

The Interaction Calculus is very similar to the Lambda Calculus, except:

1. All variables are Affine (meaning they can't be occur more than once).

2. All variables can occur globally (no "closed scopes").

3. There is a new primitive, the "Superposition", that enables:
- A. A limited, but still powerful, form of cloning.
- B. Computing on superposed structures, for optimization.

This calculus has its roots on the optimal λ-calculus evaluation literature, and
it can be seen as a distillation of the optimal evaluation algorithm, into a new
core theory that is independent from the λ-calculus. Its AST is:

```
type Term =
  | Var (nam: Name)
  | Lam (nam: Name) (bod: Term)
  | App (fun: Term) (arg: Term)
  | Sup (fst: Term) (snd: Term)
  | Dup (a: Term) (b: Term) (val: Term) (bod: Term)
```

And below is its syntax:

```
Term ::=
  | var: x
  | lam: "λ" Name "." Term
  | app: "(" Term Term ")"
  | sup: "{" Term Term "}"
  | dup: "!" "{" x y "}" "=" Term ";" Term
```

Note that, just like a lambda is eliminated by an application, a superposition
is eliminated by a duplication. The interactions go as expected:

```
(λx.body arg)
----- APP-LAM
x <- body
arg

!{p q} = {r s};
body
----- DUP-SUP
a <- fst
b <- snd
body
```

Note that, here, `x <- body` performs a *global* substitution (since `x` can
occur outside of its binding lambda's body!). Note also that the DUP-SUP rule is
very similar to a tuple projection, except, again, the substitutions are global.
Now, you may be wondering: what happens when we try to apply a SUP, or duplicate
a LAM? Naively, one could assume these would be type errors. Here, we actually
define these interactions as:

```
({u v} a)
---------------- APP-SUP
! {x0 x1} = a;
{(u x0) (v x1)}

! {p q} = λx f;
body
--------------- DUP-LAM
p <- λx0.r
q <- λx1.s
x <- {x0 x1}
! {r s} = f;
body
```

Note that `x0, x1, r, s` are new, fresh variables. Defining these (otherwise
undefined) cases is interesting, because they allow us to do some powerful new
things. The DUP-LAM rule gives us back the ability to clone lambdas (otherwise
impossible in an affine language), and it also lets us do so in a very efficient
way, as will become clear later. And the APP-SUP rule allows us to do something
entirely new: apply superposed functions to a value, which enables us to explore
the image of a function very efficiently.

Note that, for improved readability, it is usually a good idea to represent a term
by first writing all DUP nodes, followed by a DUP-free body. Example:

```
! {x0 x1} = some_term
! {y0 y1} = other_term
...
dup_free_term
```

Below is an example reduction, in small step sequent notation:

```
(λf.λx.(f x) λk.k)
----- APP-LAM #0
λx(λk.k x)
----- APP-LAM #1
λx.x
```

Below is a more complex example:

```
!{f0 f1} = f;
(λf.λx.(f0 (f1 x)) λa.λb.(b a))
----- APP-LAM #0
!{f0 f1} = λa.λb.(b a);
λx.(f0 (f1 x))
----- DUP-LAM #1
!{f0 f1} = λb.(b {a0 a1});
λx.(λa0.f0 (λa1.f1 x))
----- DUP-LAM #2
!{f0 f1} = ({b0 b1} {a0 a1});
λx.(λa0.λb0.f0 (λa1.λb1.f1 x))
----- APP-SUP #3
!{k0 k1} = {a0 a1}
!{f0 f1} = {(b0 k0) (b1 k1)};
λx.(λa0.λb0.f0 (λa1.λb1.f1 x))
----- DUP-SUP #4
!{f0 f1} = {(b0 a0) (b1 a1)};
λx.(λa0.λb0.f0 (λa1.λb1.f1 x))
----- DUP-SUP #5
λx.(λa0.λb0.(b0 a0) (λa1.λb1.(b1 a1) x))
----- APP-LAM #6
λx.(λa0.λb0.(b0 a0) λb1.(b1 x))
----- APP-LAM #7
λx.λb0.(b0 λb1.(b1 x))
```

In special, notice how, on steps #1 and #2, the variables `a0`, `a1`, `b0`,
`b1`, temporarily occurred outside of their bound λ's bodies. In this format,
substitutions, like `[x <- term]`, are very simple to compute: we literally just
replace the variable `x` by `term`, wherever they occur (even if outside of the
lambda that binds `x`). This happens, for example, on step #0. Substitution here
is simpler than on the traditional λ-calculus, since variables are affine, so,
we don't need to perform expensive copying operations; the only surprising bit
is that `x` can occur outside, but, while unusual, that's actually
straightforward, and substitutions are a simple O(1) swap. Now, despite these
"temporarily scaping scopes", at the end of the computation, the final result is
still a valid λ-term. That is common in this system, and that effect is
responsible for its optimality!

Your goal, now, is to compute the normal form of the following IC term:

```
!{f0 f1} = f;
(λf.λx.(f0 (f1 x)) λa.λb.λc.((a c) b))
```

Write out your answer in the small step sequent notation.