# Ordered, linear, affine, or relevant?

## Background

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.

## Challenge

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 rules apply. The shortest code in bytes wins.

## Test cases

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

• From your definition, Ordered lambda calculus is also Linear, Affine and Relevant. So when the input is Ordered, may the output simply output Affine?
– tsh
Aug 4, 2021 at 5:31
• @tsh No, the output should be the most restrictive set it belongs to. I'll clarify in the post. Aug 4, 2021 at 6:31
• Do we have to handle an empty lambda? My current answer would fail in that situation. Aug 4, 2021 at 16:12
• @Nick No, a lambda won't be empty. Aug 4, 2021 at 20:19

# Jelly, 18 15 bytes

F⁻ȧċⱮɗR}Ṃ;ṀƊ«Ø½


Try it online!

A dyadic link taking a nested list of integers on the left and the number of parameters on the right. Returns the following:

[0,0] - Ordered
[0,1] - Affine
[0,2] - None
[1,1] - Linear
[1,2] - Relevant


## Explanation

F    ɗR}        | Using the flattened list of integers as the left argument and a range of 1..n as the right argument:
⁻              | - Not equal
ȧ             | - Logical and
ċⱮ           | - The count of each of 1..n in the flattened list
Ṃ;ṀƊ    | Min concatenated to max
«Ø½ | Min of [1,2] and this (vectorises, so 1 is matched to the min and 2 to the max)


Note this is similar (though not identical) to my R answer, if that helps in understanding it.

• I think F⁻ȧċⱮɗR}Ṣ.ịḄ«5 works for -1 byte TIO Aug 4, 2021 at 22:42
• Actually, that probably miss categorises some "None"s as "Relevant"s. Aug 4, 2021 at 22:49
• @JonathsnAllan yes it miscategorises [[2, 2, 2], 2] for example. Aug 5, 2021 at 6:48

# JavaScript, 71 bytes

a=>g=i=>i&&(h=j=>~a.flat(1/0).indexOf(i,-j),h(p=h())?5:p?i<-p:3)|g(i-1)


Try it online!

Input a nested integer array (1-indexed), and the number of operand. Assume the input is always valid. Output a number.

• 0 - Ordered
• 1 - Linear
• 3 - Affine
• 5 - Relevant
• 7 - None

# R >= 4.1, 81 bytes

\(x,n)identical(u<-unlist(x,T),r<-1:n+0)+pmin(1:2,range(sapply(r,\(y)sum(u==y))))


Try it online!

A function that takes a nested list of integers x and the number of parameters n. Returns a length 2 vector:

[0,1] - Affine
[0,2] - None
[1,1] - Linear
[1,2] - Relevant
[2,2] - Ordered


# Charcoal, 38 bytes

≔Ｉ⪪ΦＳ›@ι θ≔ＥＮ№θιη¿⁼θＥηκO¿⁼¹⌈η§AL⌊η¿⌊ηR


Try it online! Link is to verbose version of code. Takes the string (with [] delimiters) as the first input and the number of 0-indexed variables as the second input. Explanation:

≔Ｉ⪪ΦＳ›@ι θ


Input the string, filter out the []s, split on spaces, and cast to integer.

≔ＥＮ№θιη


Count the number of occurrences of each variable.

¿⁼θＥηκO


If the flattened list of terms equals the list of variables then output O, otherwise...

¿⁼¹⌈η§AL⌊η


... if there is at most one of each variable then output L if there is (at least) one of each variable or A if there is at least one missing variable, otherwise...

¿⌊ηR


... if there is at least one of each variable then output R otherwise output nothing.