Communications of the ACM
News
Linear Logic
Logician Jean-Yves Girard, author of the seminal paper "Linear Logic."
Credit: Anne Van Der Stegen
When the French logician Jean-Yves Girard first visited Xerox PARC during a trip to Silicon Valley in 1984, he knew he was in the right place. Seeing computer scientists collaborating with linguists, ethnographers, and other non-programmers, he started to consider the possibilities of bridging computer science with his own branch of philosophy. "What impressed me most was the change of spirit," he recalls. "It was a very special time."
Following his trip to California, Girard began work on his breakthrough paper "Linear Logic," which postulated an entirely new approach to logic, one deeply informed by computational principles. In the ensuing years, the principles of linear logic have found their way into a broad range of other arenas including programming languages, proof nets, security applications, game semantics, and even quantum physics.
In the early 1980s, logicians like Girard were just starting to take an interest in computer science, while a handful of computer scientists were starting to recognize the potential of logical proof systems as a framework for functional programming. Linear logic represented an important step forward for computer science because it challenged the conceptual limitations of traditional classical logic. For thousands of years, the study of logic had hinged on the assumption of permanent Aristotelian truths, or unchanging essences. A was A, B was B, and would ever be thus. Through the lens of computer science, Girard began to see a way out of this "foundational aphoria." His chief insight was that logic could function without this unspoken assumption of perenniality. "This was a big shock," Girard recalls. "The discovery of linear logic went completely against all the things I had been taught in logic."
Whereas classical logic might support an assertion like type A → B, computer programs require a set of concrete instructions for transforming A into B, such as applications, variables, or exception handlers. In the eyes of a computer program, then, A is not a permanent entity but a consumable resource. To address this problem, Girard proposed a resource-conscious approach to logic, laying out an entirely new framework capable of describing resources that could be used and depleted during the course of an operation.
In the nearly quarter of a century since Girard published his seminal paper, most of the foundational theoretical work in linear logic has been completed. However, computer scientists continue to find new applications of the theory across a wide range of disciplines like proof nets, categorical semantics, and computer security applications.
At Carnegie Mellon University (CMU), computer science professor Frank Pfenning has been exploring the application of linear logic to distributed security problems. After one of his students introduced him to linear logic, he became convinced it provided the ideal conceptual framework for specifying difficult-to-encode rules like complex privacy policies or resource conservation strategies. "I was most interested in characterizing, logically, complex properties of distributed systems," Pfenning explains.
Working with a team of students, he used the principles of linear logic to implement a proof-carrying file system (PCFS), featuring an access control policy that is stated as a logical theory, wherein file access is granted on the condition of a logical proof of policy compliance. "Linear logic is tremendously useful here," he explains, "because we can easily represent the change of state that takes place, for example, when you read or write a file."
"The discovery of linear logic went completely against all the things I had been taught in logic," says Jean-Yves Girard.
Working with Symantec, Pfenning and CMU postdoctoral researcher Deepak Garg have applied PCFS to formalize the access control policies of the national intelligence community in the United States. In collaboration with Jamie Morgenstern, an undergraduate student from the University of Chicago, Pfenning is now working on extending the implementation to handle even more complex policies. Pfenning feels the biggest challenges lie in translating complex real-world rule sets into unambiguous logic. The ideal outcome is what he calls "an abstract logical form that is theoretically tractable and at the same time practically useful."
Proof Nets
Linear logic has also opened new doors in the field of proof nets. Prior to the introduction of linear logic, most computer scientists working in the field relied on intuitionistic logic, following the well-established Curry-Howard Correspondence, which suggested that formal proof calculi shared a common structure with computational models. Before the advent of linear logic, this model had served as the de facto standard for types. "Linear logic enriched this world greatly," says Dale Miller, director of research at INRIA Saclay, who has spent the last several years applying the principles of linear logic to proof systems.
"Originally, proof systems were used to build 'big-step' inference rules from the 'small-step' inference rules of linear logic," Miller explains. Now, he is exploring the possibilities of so-called focused proof systems by using those "small-step" inference rules to build a range of proof systems for classical and intuitionistic logic. "If one has an interpreter for focused linear logic, that interpreter can be used as an interpreter for many proof systems," says Miller, citing the examples of emulating sequent calculus and tableaux. "Different choices yield different and often, known proof systems."
In recent years, linear logic has also given rise to a new genre of programming languages like Forum, Lolli, and Lygon that incorporate richer forms of expression to allow more powerful approaches to proofs.
Looking ahead, Pfenning believes there is still work to do in improving the state of automation in linear logic. "We need theorem provers, model checkers, and other tools for working with linear logic to make its application to real-world problems easier." Miller agrees that linear logic has the potential to support the automation of theorem proving. "Focused proof systems give a central role to inference rules that are invertible," he explains. "When a formula is introduced by an invertible rule, that formula can be discarded. Such information is useful in building theorem provers."
Miller also sees an opportunity to use linear logic and proof search to provide specifications of algorithms, using proof theory research to help in reasoning about such algorithmic specifications. He also hopes to see the day when a large "logic of unity" might take shape that would encompass classical, intuitionistic, and linear logic in one grand system.
Where could linear logic go from here? Other active research areas include concurrency theory, quantum computing, game semantics, implicit computational complexity, and the verification of imperative programs with heaps using separation logic, a close cousin of linear logic.
With the field maturing, the fundamental principles of linear logic are receding into the background as an area of active inquiry as computer scientists learn to apply the established principles to emerging computational problems. "Linear logic is no longer alive as a specific subject in which you work," says Girard. "It's become something classical. It is part of the toolbox."
Pfenning agrees with Girard's assessment, but thinks linear logic lacks the widespread exposure it deserves at every level of the computer science curriculum. "It should be part of the standard toolkit," he says, "but I don't think it is taught in enough places right now, especially in the United States."
Active research areas for linear logic include concurrency theory, quantum computing, game semantics, and implicit computational complexity.
Girard, meanwhile, has moved on from the problems of computing to set his sights on more esoteric quandaries. "I would like to understand why certain things are difficult, why the world is not transparent," he says. Alas, perhaps some questions are better left to logicians.
Further Reading
Abramsky, S., Jagadeesan, R., and Malacaria, P.
Full abstraction for PCF (extended abstract). Lecture Notes in Computer Science 789, Proceedings of Conference on Theoretical Aspects of Computer Software, 1994.
Bowers, K.D., Bauer, L., Garg, D., Pfenning, F., and Reiter, M.K.
Consumable credentials in logic-based access-control systems. Proceedings of the 14th Annual Network and Distributed System Security Symposium, San Diego, CA, Feb. 28March 2, 2007.
Girard, J.-Y.
Linear logic. Theoretical Computer Science 50, 1,1987.
Lincoln, P., Mitchell, J., Scedrov, A., and Shankar, N.
Decision problems for propositional linear logic. Proceedings of the 31st Annual Symposium on Foundations of Computer Science, St. Louis, MO, Oct. 2224, 1990.
Miller, D.
An overview of linear logic programming. Linear Logic in Computer Science, Ehrhard, T., Girard, J.-Y., Ruet, P., and Scott, P. (Eds.), Cambridge University Press, London, U.K. 2004.
©2010 ACM 0001-0782/10/1000 $10.00
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.
The Digital Library is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.
No entries found