View Full Document

rfl7-ordered

View Full Document
View Full Document

12 views

Unformatted text preview:

Higher order focusing for ordered logic Request For Logic RFL 7 Robert J Simmons Daniel Licata and Jason Reed March 4 2010 In the previous note we talked about coverage checking and case analysis with linear functions representing one hole contexts In this note we push this further to do a version of higher order focusing for ordered logic using the same notion of linear functions for one hole contexts that reach into structures Ordered logic occupies a unique position in this respect because any one hole context x x into an ordered structure is equivalent to x x we can get away with explicitly representing the left and right hand sides Experience seems to show that this is often quite a bit less satisfying than in linear logic where a one hole context x x is equivalent to x x the formulation we use here seems in any case no worse than the explicit left handside right hand side formulation We only consider the Lambek calculus portion of ordered logic that is we don t consider the validity or mobility modalities Our proof appears to have the property that if we changed the properties of the context formation operator we would still have a valid proof in other words this can be seen as a proof of rigid logic or a redundant proof of linear logic just by manipulating the algebraic properties of the comma Higher order focusing for ordered logic Contexts are written as or The context formation operator is associative and commutative with unit hyp A hyp Q We adopt the convention that a context with one hole is written as or a context with two holes is written as or and so on However these should really be understood as eta contracted versions of the representational linear functions x x x y x y and so on The hole is similarly shorthand for x x The basic idea is that while we usually write the cut principle for ordered logic like this If A and hyp A C then C However we can talk about this cut principle more generally with one hole contexts where we write the cut principle

Unlocking...