nLab focusing

Idea

Focusing is an idea originating in the proof theory of linear logic. Originally, it was introduced as a technique for making proof search in the sequent calculus tractable, by restricting the potential application of rules based on observations about the polarity of connectives (Andreoli 1992). More abstractly, the focalization property can be seen as a canonical form theorem for sequent calculus proofs, which holds in a wide range of systems beyond linear logic.

Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic [Andreoli 1992], defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grouping sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that every non-focused derivation can be transformed into a focused derivation. (Simmons)

Related concept

• polarity in type theory

References

• Jean-Marc Andreoli, Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992 (pdf)
• Daniel Licata, Noam Zeilberger, Robert Harper, Focusing on Binding and Computation, (pdf)
• Robert Simmons, Structural focalization, arXiv:1109.6273, cs.LO
• Robert Simmons, What does focusing tell us about language design?, (blog post)
• Taus Brock-Nannestad and Carsten Schürmann, Focused Natural Deduction, (pdf)
• Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747–4768, November 2009. (pdf)
• Stéphane Graham-Lengrand. Polarities & Focussing: a journey from Realisability to Automated Reasoning. Habilitation thesis, Université Paris-Sud, 2014. (pdf)