Wrong result

[VictorTaelin]

The term:

/ #n #B #T #O #I #E
  ///n
    #r #p //B
      /r /O p
      /r /I p
    #p /T p
    E
  #f #x /f /f /f x

Produces the wrong output in all versions of Absal, including the old Optlam. It is the first example I'm aware of that can be read-back normally but simply produces a wrong output.

[lukaszlew]

What is this notation? Is it a lambda term?

[VictorTaelin]

The syntax is:

• Lambda: #a b, reads as λa. b

• Application: /a b, reads as (a b)

• Variable: as usual

Using this because it wields the simplest ascii parser.

[lukaszlew]

Still hard to read.
Is the problem just with the readback or is the abstract algorithm incorrect for it?

[Kesanov]

Another weird thing: the following expressions returns the correct output ###:a ###c

@Y  #f :#x :f :x x #x :f :x x

-- data Bits = Empty | O Bits | I Bits  
@E       #E #O #I  E
@O  #xs  #E #O #I :O xs
@I  #xs  #E #O #I :I xs

-- copy : Bits -> Bits
@copy :Y #self #xs :::xs 
      #E #O #I  E
  #xs #E #O #I :O :self xs
  #xs #E #O #I :I :self xs 

:copy :I E

but this one hangs indefinitely:

@copy :Y #self #xs #E #O #I :::xs 
       E
  #xs :O :self xs
  #xs :I :self xs 

:copy :I E

[VictorTaelin]

Well, I'll be using EAL on the Rust implementation of Abstract Algorithm which fortunately makes those weird issues not happen!

[L-as]

Is this still happening?

[VictorTaelin]

We implemented an EAL-based proof language and dropped it because it was too verbose to use in practice.