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 innerx
binds to the first (and only)λ
in scope.λx. λy. x
is written asλ λ 2
, as the innerx
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 a2
is added at the end. Sincei
is positive, this always starts with a 1. - A lambda abstraction
λ e
is recursively converted to0<e>
, where<e>
denotes the Ternary conversion ofe
. - A function application
e1 e2
is recursively converted to2<e1><e2>
.
Examples:
λ 1
is encoded to012
. (1
encodes to12
, and a single lambda abstraction adds a0
)λ λ 2
is encoded to00102
.λ λ 2 (λ 1 2)
is encoded to0021020212102
.
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 ()
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