Linear logic and lazy computation. (English) Zbl 0647.03016

Girard, J. Y.; Lafont, Y.

TAPSOFT ’87, Proc. Int. Conf. Software development, Pisa/Italy 1987, Vol. 2: Functional and logic programming and specifications, Lect. Notes Comput. Sci. 250, 52-66 (1987).

Summary: [For the entire collection see Zbl 0605.00016.]
Recently, the first author discovered that usual logical connectors such as \(\Rightarrow\) (implication) could be broken up into more elementary linear connectors. This provided a new linear logic [Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)] where hypotheses are (in some sense) used once and only once. The most surprising fact is that all the power of the usual logic can be recovered by means of recursive logical operators (connector “of course”). There are two versions of linear logic: the intuitionistic one and the classical one. It seems that the second provides an appropriate formalism for parallelism and communication. This approach is entirely new and requires a further development. Here we restrict our attention to the intuitionistic version and to the consequences of the linear constraint to the computation process. We give two equivalent presentations of the (propositional part of ) linear logic: a sequent calculus and a (categorical) combinator system. Then we introduce inductive and projective connectors, in particular the connector ö (read “of course”). It plays a fundamental role in the encoding of usual intuitionistic logic into linear logic. There is a cut elimination theorem for the sequent calculus that corresponds to an evaluation mechanism for the combinator system. We present a very simple (abstract) machine that performs linear computations with the following features: a very natural lazy evaluation mechanism, no need of garbage collector. Finally, we discuss the relevance of linear logic to implement functional languages.

MSC:

03B70	Logic in computer science
03B40	Combinatory logic and lambda calculus
68N01	General topics in the theory of software
03F05	Cut-elimination and normal-form theorems

Keywords:

intuitionistic linear logic; abstract machine; implementation of functional languages; sequent calculus; combinator system; of course; cut elimination; evaluation mechanism; linear computations; lazy evaluation

Citations:

Zbl 0605.00016; Zbl 0625.03037