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.
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. xis written as
λ 1, as the inner
xbinds to the first (and only)
λx. λy. xis written as
λ λ 2, as the inner
xbinds 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
iis converted to binary (using 0 and 1), and then a
2is added at the end. Since
iis positive, this always starts with a 1.
- A lambda abstraction
λ eis recursively converted to
<e>denotes the Ternary conversion of
- A function application
e1 e2is recursively converted to
λ 1is encoded to
12, and a single lambda abstraction adds a
λ λ 2is encoded to
λ λ 2 (λ 1 2)is encoded to
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)
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 ()
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.
-- Truthy 012 00102 0021020212102 000000000010102 00002210022112122112102 -- Falsy (empty) 2112 2112112 012012012