HOAS evaluator of Interaction Calculus returns wrong result when computing 2^2

[VictorTaelin]

Reproducing the behavior

Consider the following Bend program:

type Term
  = (Lam bod)
  | (App fun arg)
  | (Sup lab fst snd)
  | (Dup lab val bod)
  | (Var idx)

#  (λx(bod) arg)
#  ------------- APP-LAM
#  x <- arg
#  bod
(APP (Term/Lam bod) arg) =
  (bod arg)

#  (#i{g,h} arg)
#  ----------------- APP-SUP
#  dup #i{a,b} = arg
#  #i{(g a) (h b)}
(APP (Term/Sup i g h) arg) =
  (DUP i arg λaλb
  (Term/Sup i (APP g a) (APP h b)))

#  ((dup #i{x,y} = val; bod) arg)
#  ------------------------------ APP-DUP
#  (dup #i{x,y} = val; (bod arg))
(APP (Term/Dup i val bod) arg) =
  (DUP i val λaλb(APP (bod a b) arg))

#  (fun arg)
#  --------- APP
#  (fun arg)
(APP fun arg) =
  (Term/App fun arg)

#  dup #i{k0,k1} = λx(f); bod
#  -------------------------- DUP-LAM
#  dup #i{f0,f1} = f
#  x  <- #i{x0,x1}
#  k0 <- λx0(f0)
#  k1 <- λx1(f1)
#  bod
(DUP i (Term/Lam f) bod) =
  (DUP i (f (Term/Sup i $x0 $x1)) λf0λf1
  (bod (Term/Lam λ$x0(f0)) (Term/Lam λ$x1(f1))))

#  dup #i{k0,k1} = #j{fst,snd}; bod
#  -------------------------------- DUP-SUP
#  if #i == #j:
#    k0 <- fst
#    k1 <- snd
#    bod
#  else:
#    k0 <- #j{a0,b0}
#    k1 <- #j{a1,b1}
#    dup #i{a0,a1} = fst
#    dup #i{b0,b1} = snd
#    cont
(DUP i (Term/Sup j fst snd) bod) =
  switch (== i j) {
    0:
      (DUP i fst λa0λa1
      (DUP i snd λb0λb1
      (bod
        (Term/Sup j a0 b0)
        (Term/Sup j a1 b1))))
    _:
      (bod fst snd)
  }

#  dup #i{k0,k1} = (dup #j{r0,r1} = v; f); bod
#  ------------------------------------------- DUP-DUP
#  dup #j{r0,r1} = v
#  dup #i{k0,k1} = f
#  bod
(DUP i (Term/Dup j v f) bod) =
  (DUP j v λr0λr1
  (DUP i (f r0 r1) bod))

#  dup #i{k0,k1} = val; bod
#  ---------------------- DUP
#  dup #i{k0,k1} = val; bod
(DUP i val bod) =
  (Term/Dup i val bod)

(Quote (Term/Lam bod)         dep) = (Term/Lam λx(Quote (bod (Term/Var dep)) (+ dep 1)))
(Quote (Term/App fun arg)     dep) = (Term/App (Quote fun dep) (Quote arg dep))
(Quote (Term/Sup lab fst snd) dep) = (Term/Sup lab (Quote fst dep) (Quote snd dep))
(Quote (Term/Dup lab val bod) dep) = (Term/Dup lab (Quote val dep) λx0λx1(Quote (bod (Term/Var dep) (Term/Var (+ dep 1))) (+ dep 2)))
(Quote (Term/Var idx)         dep) = (Term/Var idx)

C2a = (Term/Lam λf(Term/Lam λx(DUP 0 f λf0λf1(APP f0 (APP f1 x)))))
C2b = (Term/Lam λf(Term/Lam λx(DUP 1 f λf0λf1(APP f0 (APP f1 x)))))
Not = (Term/Lam λb(Term/Lam λt(Term/Lam λf(APP (APP b f) t))))

Main = (Quote (APP C2a C2b) 0)

It implements a HOAS evaluator for the Interaction Calculus. When running it on Bend, for 2 ^ 2, it outputs:

λa (a Term/Lam/tag λ* ($b *))

I expected the result to be the encoding of 4, since C2a and C2b use different dup labels. Yet, we get an erratic result, with a weird, unbound $b variable shown. This could be a bug on Bend or HVM2, this could be a bug or typo on my program, or this could be some fundamental limitation on implementing HOAS IC on Interaction Combinators.

I'm looking for insights.

Note: we also get the wrong result on HVM1 (Gist which makes me suspect it is either some fundamental limitation I'm overseeing, or just a silly bug in the code above. Here is the complete evaluation log (running it on HVM1). Going through this step by step might help us understand where the divergence arises.

System Settings

Bend 0.2.36, OSX Sonoma 14.5.

[NoamDev]

Mistery solved, I believe! I manually reduced this to:

(Quote
    (Term/Lam λx
      (DUP 0 
        (DUP 1 $f4
            λf5λf6
                (DUP 1 x λb0λb1
                  (Term/Sup 0 f5 (APP b0 (APP b1 (Term/Sup 1 f6 $x3))))
                )
        )
        λf3λ$f4 (Term/Lam λ$x3(f3))
      )
    )
0)

(You can "verify" the correctness by running this and the original code without the Quote and seeing it has idenctical results)

If you look closely you'll see that

      (DUP 0 
        (DUP 1 $f4
            λf5λf6
                (DUP 1 x λb0λb1
                  (Term/Sup 0 f5 (APP b0 (APP b1 (Term/Sup 1 f6 $x3))))
                )
        )
        λf3λ$f4 (Term/Lam λ$x3(f3))
      )

which is the one binding $f4,

depends on

        (DUP 1 $f4
            λf5λf6
                (DUP 1 x λb0λb1
                  (Term/Sup 0 f5 (APP b0 (APP b1 (Term/Sup 1 f6 $x3))))
                )
        )

which itself depends on $f4.

Therefore we have circular dependency here, and the functions can't reduce.

I've hit a very similiar issue with my own attempt at an SIC-HOAS