Ordered, linear, affine, or relevant?

Question

Background

Supplementary reading 1, Supplementary reading 2

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 code-golf 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

Answer 1

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

The TIO footer adds textual representations of each answer as well.

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.

Answer 2

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

Answer 3

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

Answer 4

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.