TY - GEN
T1 - Non-linearity as the metric completion of linearity
AU - Mazza, Damiano
PY - 2013/9/27
Y1 - 2013/9/27
N2 - We summarize some recent results showing how the lambda-calculus may be obtained by considering the metric completion (with respect to a suitable notion of distance) of a space of affine lambda-terms, i.e., lambda-terms in which abstractions bind variables appearing at most once. This formalizes the intuitive idea that multiplicative additive linear logic is "dense" in full linear logic (in fact, a proof-theoretic version of the above-mentioned construction is also possible). We argue that thinking of non-linearity as the "limit" of linearity gives an interesting point of view on well-known properties of the lambda-calculus and its relationship to computational complexity (through lambda-calculi whose normalization is time-bounded).
AB - We summarize some recent results showing how the lambda-calculus may be obtained by considering the metric completion (with respect to a suitable notion of distance) of a space of affine lambda-terms, i.e., lambda-terms in which abstractions bind variables appearing at most once. This formalizes the intuitive idea that multiplicative additive linear logic is "dense" in full linear logic (in fact, a proof-theoretic version of the above-mentioned construction is also possible). We argue that thinking of non-linearity as the "limit" of linearity gives an interesting point of view on well-known properties of the lambda-calculus and its relationship to computational complexity (through lambda-calculi whose normalization is time-bounded).
U2 - 10.1007/978-3-642-38946-7_3
DO - 10.1007/978-3-642-38946-7_3
M3 - Conference contribution
AN - SCOPUS:84884513087
SN - 9783642389450
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 14
BT - Typed Lambda Calculi and Applications - 11th International Conference, TLCA 2013, Proceedings
T2 - 11th International Conference on Typed Lambda Calculi and Applications, TLCA 2013
Y2 - 26 June 2013 through 28 June 2013
ER -