{'fraction_non_alphanumeric': 0.0568678915135608, 'fraction_numerical': 0.003499562554680665, 'mean_word_length': 3.46875, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
λ-calculus in an algebraic setting

We define an extension of λ-calculus with linear combinations of terms, with coefficients taken in a fixed rig R. We extend β-reduction on these terms as follows: at + u reduces to at + u as soon as term t reduces to t and a is a non-zero scalar. We prove that reduction is confluent. Under the assumption that R is a positive rig (i.e. a sum of scalars is zero iff all of them are zero), we show that this algebraic λ-calculus is a conservative extension of ordinary λ-calculus: two ordinary λ-terms equalized by the reduction of algebraic λ-calculus are β-equal. Last, we prove that under some reasonably minimal conditions on R, simply typed algebraic λ-terms are strongly normalizing. Preliminary definitions and notations. Let R be a rig. We denote by letters a, b, c the elements of R. We say that R is positive if for all a, b ∈ R, a + b = 0 implies a = 0 and b = 0. An example of positive rig is N, the set of natural numbers. We write R for R \ {0}. If i, j ∈ N, we write [i, j] for the set {k ∈ N; i ≤ k ≤ j}. Also, we write λ-terms à la Krivine: (s) t denotes the application of term s to term t.