another challenging prompt

gistfile1.txt

//./runtime.c//
//./reduce.hs//

# 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;
&L{(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)


TASK: complete the file above with the full reduction for the overlap example.