Why is multiplicative disjunction called “par” in linear logic

linear-logiclogicmath-historysoft-questionterminology

In linear logic multiplicative disjunction is often called par.
This terminology goes back at least to Girard's seminal text Linear logic. I vaguely remember that I read that "par" is an abbreviation for "parallel“. If so, why? Does anyone know the etymology of the term?

EDIT: In Linear logic and parallelism Girard calls par the "parallel connective".

Best Answer

That's right; 'par' is from 'parallelisation'. The following two quotes from Girard may be illuminative about the significance of parallelisation in linear logic:

(ii) The new connectives of linear logic have obvious meanings in terms of parallel computation, especially the multiplicatives. In particular, the multiplicative fragment can be seen as a system of communication without problems of synchronization. The synchronization is handled by proof-boxes which are typical of the additive level. Linear logic is the first attempt to solve the problem of parallelism at the logical level, i.e., by making the success of the communication process only dependent of the fact that the programs can be viewed as proofs of something, and are therefore sound.

[Linear Logic in Theoretical Computer Science 50, 1987, p. 3]

Furthermore, multiplicative connectors and rules can be generalised to make a genuine programming language. [Footnote] Cut elimination is in fact parallel communication between processes. In this language, logic does not ensure termination, but absence of deadlock.

[emphases in the original, Proofs and Types, 2003 Web edition, p. 154]

See also Di Cosmo and Miller's article Linear Logic.

Related Question