Linear lambda calculus is a limited form of lambda calculus, where every bound variable must be used exactly once. For example,
\a b c d e -> a b (d c) e is a valid term in linear lambda calculus. When embedded as a logic system, this enforces each input to be consumed exactly once. The equivalents in logic/type/language theory are called linear logic, linear type, and linear language respectively.
Ordered lambda calculus is a more limited version: it requires the variables to be used in the order they are introduced.
\a b c d e -> a (b c) (d e) is such an example.
Affine and relevant lambda calculi are relaxed versions of linear lambda calculus.
- Affine: each variable must be used at most once.
\a b c d e -> a (d c) e
- Relevant: each variable must be used at least once.
\a b c d -> a (c b) (d c)
If omitting and duplicating a variable are both allowed, we get plain lambda calculus.
These have interesting relationship with BCKW combinator calculus:
- Ordered lambda calculus can be represented using just B and I combinators. (I is needed to represent
\a -> a.)
\a b c d e -> a (b c) (d e) \a b c d -> B (a (b c)) d \a b c -> B (a (b c)) \a b -> B B (B a b) \a -> B (B B) (B a) B (B (B B)) B
- Linear lambda calculus can be represented using B and C combinators. (I is equal to BCC, and is used only for simplicity.)
\a b c d e -> a b (d c) e \a b c d -> a b (d c) \a b c -> B (a b) (C I c) \a b -> B (B (a b)) (C I) \a -> C (B B (B B a)) (C I) C (B C (B (B B) (B B))) (C I)
- Affine lambda calculus can be represented using BCK. K allows to delete unused variables.
\a b c d e -> a (d c) e \a b c d -> a (d c) \a b c -> B a (C I c) \a b -> B (B a) (C I) \a -> K (B (B a) (C I)) B K (C (B B B) (C I))
- Relevant lambda calculus can be represented using BCW. W allows to duplicate variables.
\a b c d -> a (c b) (d c) \a b c -> B (a (c b)) (C I c) \a b -> W (\c1 c2 -> B (a (c1 b)) (C I c2)) \a b -> W (\c1 -> B (B (a (c1 b))) (C I)) \a b -> W (C (B B (B B (B a (C I b)))) (C I)) ...
- BCKW forms a complete basis for the plain lambda calculus.
Given a lambda term in the format below, classify it into one of five categories (ordered, linear, affine, relevant, none of these). The output should be the most restrictive one the input belongs to.
The input is a lambda term that takes one or more terms as input and combines them in some way, just like all the examples used above. To simplify, we can eliminate the list of input variables, and simply use the number of variables and the "function body", where each variable used is encoded as its index in the list of arguments.
\a b c d e -> a b (d c) e is encoded to
5, "1 2 (4 3) 5". (Note that it is different from de Bruijn indexes.)
The function body can be taken as a string or a nested structure of integers. The "variable index" can be 0- or 1-based, and you need to handle indexes of 10 or higher.
For output, you can choose five consistent values to represent each of the five categories.
Standard code-golf rules apply. The shortest code in bytes wins.
length, "body" (lambda term it represents) => answer 1, "1" (\a -> a) => Ordered 2, "1 2" (\a b -> a b) => Ordered 2, "2 1" (\a b -> b a) => Linear 2, "1" (\a b -> a) => Affine 2, "2 (1 2)" (\a b -> b (a b)) => Relevant 2, "1 1" (\a b -> a a) => None 3, "1 3 (2 3)" (\a b c -> a c (b c)) => Relevant 4, "1 3 (2 3)" (\a b c d -> a c (b c)) => None 10, "1 (2 (3 4) 5) 6 7 8 (9 10)" => Ordered 10, "5 (2 (6 10) 1) 3 7 8 (9 4)" => Linear 10, "5 (2 (6 10) 1) (9 4)" => Affine 10, "1 5 (2 (3 6 10) 1) 3 7 8 (10 9 4)" => Relevant 10, "1 (2 (4 10) 1) 5 (9 4)" => None