Pourquoi est-ce qu’un mot est intraduisible ? Parce que l’algèbre linéaire

Girard’s linear logic can be used to model programming languages in which each bound variable name has exactly one “occurrence”–i.e., no variable can have implicit “fan-out”; multiple uses require explicit duplication. Among other nice properties, “linear” languages need no garbage collector, yet have no dangling reference problems. We show a natural equivalence between a “linear” programming language and a stack machine in which the top items can undergo arbitrary permutations. Such permutation stack machines can be considered combinator abstractions of Moore’s Forth programming language.