yet another FP prompt

another_fp_prompt.md

The Interaction Calculus

The Interaction Calculus (IC) is term rewriting 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 "Example 4" reduction above. write it in a single code block, similarly to the other examples.

The goal is to normalize an overlab example based on the Interaction Calculus tutorial. The correct reduction is:

({λ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 }  

Note that arriving at the right answer isn't sufficient. The AI needs to derive the correct steps, in the correct order. The challenging bit is the DUP-LAM pass, which entangles the λz.z as λr.f0 and λs.f1, superposing its bound variables as {r,s}. Getting this pass right implies the AI understood the Interaction Calculus.