Parse Ternary Lambda Calculus for correctness

Question

Wheat Wizard has once tried to come up with a parsing problem unsuitable for regex, but it failed due to Anders Kaseorg's Perl regex answer. This is the second attempt. Now that we know that Perl regex is far more powerful than we've imagined, this challenge aims to be un-golfy for it instead.

Introduction

A lambda term is recursively defined as follows:

• A variable is a lambda term.
• A lambda abstraction of a lambda term is a lambda term.
• A function application of two lambda terms is a lambda term.

This is concisely written as follows (where e is a term and x is any valid variable name):

e = x | λx. e | e e

A variable is often a string (as in Wheat Wizard's challenge), but it suffers from name shadowing problem. To avoid it and for an easier encoding, we use de Bruijn indices instead. In this notation, a variable is replaced with a positive integer, which is equal to "the number of binders that are in scope between that occurrence and its corresponding binder". The grammar is simplified to the following:

e = i | λ e | e e

Some examples in this notation:

• λx. x is written as λ 1, as the inner x binds to the first (and only) λ in scope.
• λx. λy. x is written as λ λ 2, as the inner x binds to the second λ, counting from the closest one.
• λx. λy. x (λz. z y) is written as λ λ 2 (λ 1 2).

Ternary lambda calculus

This is an encoding of a lambda term similar to Binary lambda calculus, but in ternary (a string of digits 0, 1, and 2). A lambda term written using de Bruijn indexes is converted to Ternary lambda calculus as follows:

• A variable of index i is converted to binary (using 0 and 1), and then a 2 is added at the end. Since i is positive, this always starts with a 1.
• A lambda abstraction λ e is recursively converted to 0<e>, where <e> denotes the Ternary conversion of e.
• A function application e1 e2 is recursively converted to 2<e1><e2>.

Examples:

• λ 1 is encoded to 012. (1 encodes to 12, and a single lambda abstraction adds a 0)
• λ λ 2 is encoded to 00102.
• λ λ 2 (λ 1 2) is encoded to 0021020212102.

The original BLC requires that the lambda term is closed, i.e. all variables are bound to some lambda abstraction. This means the variable index i is limited by the current "lambda depth"; in particular, no variables may appear at the top level at all. Using the lambda depth (a non-negative integer) as the context, the grammar to match becomes the following:

TermAtDepth(d) =
    bin(i) "2" where 1 ≤ i ≤ d
  | "0" TermAtDepth(d+1)
  | "2" TermAtDepth(d) TermAtDepth(d)

e = TermAtDepth(0)

Code

tlc :: Int -> Parser ()
tlc depth =
  do
    choice
      [ do
        char '1'
        idx <- many $ charBy (`elem` "01")
        guard $ foldl (\x y->x*2+y) 1 [fromEnum x-48|x<-idx] <= depth
        char '2'
        return ()
      , do
        char '0'
        tlc (depth + 1)
      , do
        char '2'
        tlc depth
        tlc depth
      ]
    return ()

Try it online!

Challenge

Given a ternary string (a string that entirely consists of digits 0, 1, and 2), determine if it is a valid Ternary lambda calculus code.

You may take the input as a string or a list of digit values. The input may be empty, and your code should give a false output on it.

For output, you can choose to

• output truthy/falsy using your language's convention (swapping is allowed), or
• use two distinct, fixed values to represent true (affirmative) or false (negative) respectively.

Standard code-golf rules apply. The shortest code in bytes wins.

Test cases

-- Truthy
012
00102
0021020212102
000000000010102
00002210022112122112102

-- Falsy
(empty)
2112
2112112
012012012

Answer 1

Jelly, 32 bytes

4ŀ1Ẹ?‘}
1;œṡ2Ṫ0ḢḄ<ɗ?
ñ⁹ñ
Ḣ‘$ŀ
ç1

Try it online!

A full program taking a list of integers and returning an empty list (falsy) for valid and a non-empty list (truthy) for invalid.

Explanation

Helper link 1 (handles 0…)

   Ẹ?        | If the list is non-empty:
4ŀ   ‘}      | - Call helper link 4 with the depth increased by 1
  1          | - Else return 1

Helper link 2 (handles 1…)

1;           | Prepend 1
  œṡ2        | Split at 2s
       ḢḄ<ɗ? | If the first part of the list converted from binary is less than the depth:
     Ṫ       | - Return the second part of the list
      0      | - Else return 0

Helper link 3 (handles 2…)

ñ⁹ñ          | Call helper link 4 twice, preserving depth

Helper link 4 (handles next part)

Ḣ‘$ŀ         | Call the helper link indicated by the first list member plus 1, preserving the same depth

Main link

ç1           | Call helper link 4 with 1 as the right argument (depth)

Answer 2

Haskell + hgl, 86 bytes

q x=cx[do χ 1;k<-my$kB(<2);gu$x>lF(pl.db)1 k;χ 2,χ 0*>q(x+1),χ 2*>q x*>q x]
x1$q 1

Takes input as a list of integers

hgl is a library I am making for golfing in Haskell. It has pretty decent parsing capabilities. It however does not yet have a function to convert from binary. Which is a bit of a problem for this answer. The code I came up with to do the task is lF(pl.db)0.

This code follows same structure of the parsing code given in the question. That's because both parsing libraries are written by me and use the same theoretic underpinning.

We use cx which is analygous to the choice in the question selecting between 3 options.

q x = cx
  [ do
    χ 1
    k<-my$kB(<2)
    gu$x>lF(pl.db)1 k
    χ 2
  , χ 0*>q(x+1)
  , χ 2*>q x*>q x
  ]

The last two don't use do notation since it would cost bytes, but they can be written with it.

q x = cx
  [ do
    χ 1
    k<-my$kB(<2)
    gu$x>lF(pl.db)1 k
    χ 2
  , do
    χ 0
    q(x+1)
  , do
    χ 2
    q x
    q x
  ]

As one might guess now χ parses a single integer. We have gu which is guard, m which is fmap and kB which is the charBy function.

The remainder is lF(pl.db)1 which converts from binary. In regular haskell this is

foldl((+).(*2))1

Answer 3

JavaScript, 121 bytes

f=d=>(s=s.slice(1),s[0]<1?f(d+1):s[0]>1?f(d)&f(d):(s=s.replace(/[01]+/,x=>parseInt(x,2)>d||''))[0]>1),a=>f(0,s=0+a)&!s[1]

Try it online!

The first function called, which is the unnamed arrow function at the end of the code, calls f while using an extra argument to initialise s to the provided string with 0 prepended.

f does the main parsing, removing characters from s as it goes, returning false on failure. It begins by unconditionally removing one character, which is the reason for the prepended 0.

The first two cases are simple: s[0]<1 (begins with 0) leads to f(d+1), a recursive call with depth increased, and s[0]>1 (begins with 2) leads to f(d)&f(d), parsing two subterms.

The final case covers s beginning with 1, and also s being empty (in which case s[0] is undefined, making both comparisons false). It uses the regexp /^[01]+/ to pick out the binary number. The replacer function (x=>parseInt(x,2)>d||'') checks whether the number is too high, returning true if it is and an empty string otherwise. The function then checks whether the remaining string begins with a digit greater than 1; if the number was too high, it begins with t and that is false. In the case of s being empty, no replacement occurs, and ""[0]>1 is also false.

Finally, back in the unnamed arrow function, !s[1] checks whether the whole string was parsed, in which case all but one character will have been removed from it.

Answer 4

Haskell, 106 bytes

(y%q)x|2:z<-q=[z|y<x]|w:z<-q=(2*y+w)%z$x|1>0=[]
x#(z:y)=[(1+x)#y,1%y$x,x#y>>=(x#)]!!z
x#_=[]
([[]]==).(1#)

Try it online!

Quite different from my Haskell + hgl answer, and still decently short, all things being considered. This uses a more bootleg parse than that, but if you squint you can see the similarities.

Answer 5

Curry (PAKCS), 86 bytes

d#(0:x)=(d+1)#x
d#(1:i++[2])|all(<2)i&&foldl((+).(2*))1 i<=d=1
d#(2:x++y)=d#x*d#y
(0#)

Try it online!

Returns 1 for truth, and nothing otherwise.