Computing with relations, functions, and bindings

Separating functional computation from relations

   The development of the logical foundations of arithmetic generally starts with the first-order logic of relations to which constructors for zero and successor have been added. Various axioms (such as Peano’s axioms) are then added to that framework in order to define the natural numbers and various relations among them. Of course, it is often natural to think of some computations, such as say, the addition and multiplication of natural numbers, as being functions instead of relations. A common way to introduce functions into the relational setting is to enhance the equality theory. For example, Troelstra in [Tro73, Section I.3] presents an intuitionistic theory of arithmetic in which all primitive recursive functions are treated as black boxes and every one of their instances, for example 23 + 756 = 779, is simply added as an equation. A modern and more structured version of this approach is that of the λΠ-calculus modulo framework proposed by Cousineau & Dowek [CD07]: in that framework, the dependently typed λ-calculus (a presentation of intuitionistic predicate logic) is extended with a rich set of terms and rewriting rules on them. When rewriting is confluent, it can be given a functional programming implementation: the Dedukti proof checker [Ass+16] is based on this hybrid approach to treating functions in a relational setting. A predicate can, of course, encode a function. For example, assume that we have a (? + 1)-ary (? ≥ 0) predicate R for which we can prove that the first ? arguments uniquely determine the value of its last argument. That is, assume that the following formula is provable (here, ̄? denotes the list of variables ?1 , … , ??): ∀ ̄?([∃?.R( ̄?, ?)] ∧ ∀?∀?[R( ̄?, ?) ⊃ R( ̄?, ?) ⊃ ? = ?]). In this situation, an ?-ary function ?R exists such that ?R( ̄?) = ? if and only if R( ̄?, ?). In order to formally describe the function ?R, Hilbert [HB39] and Church [Chu40] evoked choice operators such as ϵ and ι which (along with appropriate axioms) are able to take a singleton set and return the unique element in that set. For example, in Church’s Simple Theory of Types [Chu40], a definition of ?R is provided by the expression λ?1 … λ??ι(λ?.R(?1 , … , ??, ?)). In this chapter, we present a different approach to separating functional computations from more general reasoning with relations. We shall not extend the equational theory beyond the minimal equality on terms and we shall not use choice principles.

The ℱ⊃ calculus

   The main principle of focusing is to classify inference rules in two groups, invertible ones and non-invertible ones. Then it is possible to organize proofs in an alternation of two phases: the asynchronous phase during which are applied invertible rules only and the synchronous phase when non-invertible rules are applied.
Definition 1.1. We call invertible the rules whose conclusion and premises are equiprovable. Two invertible rules can always be permuted in the tree of inferences. Thus the application order of a series of invertible rules has no impact on the derivability of a formula and such rule applications are guaranteed not to affect the provability of the goal formula. In the two-phases process these sequences of invertible rules, eagerly applied, constitute the asynchronous phase. In Section 2 and Section 3 we will show how invertible phases can provide for a natural treatment of computational behavior. In contrast, the synchronous phases, where non-invertible rules are used, require choices to be made in order to progress in the proof. One example of such a choice is the necessity to exhibit a witness for an existentially quantified formula. When a synchronous phase is entered, the proof is focused on a particular formula which is then used to indicate followup synchronous rules, maintaining focus as long as possible. This drastically reduces the choice points in the proof, since after a focus has been decided the choices are constrained to those relevant to that chosen formula. Connectives whose right introduction rules are invertible will be called negative or asynchronous whereas the others will be called positive or synchronous. We will use the following set of notations in all our focused systems:
Definition 1.2. Notations
– A, B, C denote formulas
– N? and P? respectively range over negatively polarized atoms and positively polarized atoms
– E denotes either a positive formula or a negative atom
– C denotes either a negative formula or a positive atom
– t, u, v denote terms in βη-long normal form
– τ denotes a term type
– Γ is a multiset of formula
– Θ is a list of formulas
– Σ is a list of typed term variables, called the signature, which are considered bound over a sequent. To lighten the sequents the signature will be omitted when not necessary.
– Δ1 and Δ2 are two multisets of formulas such that Δ1 ∪ Δ2 contains one and unique formula.
– We use dots (⋅) to materialize empty zones.

An extension to equivalence classes

   Equivalence relations play important roles in computation and reasoning. Occasionally, we have a relation that is not functional but all the possible outcomes are equivalent, for some specific equivalence relation. For example, if two lists are considered equivalent when they are permutations of each other, then the equivalence class of lists modulo that relation encodes multisets. Similarly, if two pairs of integers (?, ?) and (?, ?) (where ? and ? are not zero) are considered equivalent when ?? = ?? then equivalence classes encode rational numbers. The ambiguity of singletons can be lifted to computation with equivalence classes in the following sense. Let ρ be an equivalence relation. The familiar notation [?]ρ for the ρ-equivalence class containing ? is just syntactic sugar for λ?.?ρ?. (We define logical equivalence in the usual way: A ≡ B is an abbreviation for(A ⊃ B)∧(B ⊃ A).) Assume that ρ is an equivalence relation and that the following holds if Q ∶ ? → ?.∀?∀?. ? ρ ? ⊃ [Q(?) ≡ Q(?)] (Note that this theorem is immediate for all Q ∶ ? → ? when ρ is equality.) The following equivalence holds.[∀?. ? ∈ [?]ρ⊃Q(?)] ≡ [∃?. ? ∈ [?]ρ∧ Q(?)] In a more informal mathematical notation, one might replace either the above existential or universal expression with Q([?]ρ). While we shall not use this expression (it involves a typing error), it conveys the usual mathematical sense of this ambiguity: if we show that one member of an equivalence class satisfies such a property Q then all members of that equivalence class satisfy Q. Obviously, we can generalize the notion of functional dependency to the following ∀ ̄?([∃?.R( ̄?, ?)] ∧ ∀?∀?[R( ̄?, ?) ⊃ R( ̄?, ?) ⊃ ?ρ?]),which states that the ?-ary relation is a total function up to ρ. Thus, during the construction of a proof where one is asked to pick a term ? that makes R(?1, … , ??, ?) true, one can instead compute just any term ?′ such that R(?1, … , ??, ?′) (as long as the established property Q is ρ-invariant). In that setting, we can also extend the phase-abstraction mechanism to exclude border premises that differ up to ρ.

Proposal: Computation and Suspension

   Our first proposed extension of Abella is rather simple: the addition of a compute tactic that performs unfolding and subsequent asynchronous steps for assumptions involving predicates with a fully positive definition. Thus, for instance, if we have an assumption H : plus ( s z ) ( s z ) X then the invocation compute H would repeatedly unfold the definition of plus and handle the resulting subgoals eagerly if it can use purely asynchronous steps. In this particular case, the effect will be the removal of H entirely and the instantiation of X with (s (s z)). The compute tactic is allowed to produce multiple branches. For instance, in the following case: H : plus X Y ( s ( s z ) ) the invocation compute H would produce three subgoals, one each for the three ways there are to decompose 2 into a sum of two natural numbers. This kind of feature has long been recognized as an important need in Abella.6 A very common form is encountered in meta-theoretic proofs involving memberships in contexts, which are represented as lists in Abella, where we have an assumption such as: H : member X ( E1 :: E2 :: Rest ) In this case we would like compute H to yield three subgoals (in addition to the assumption): the first with X = E1, the second with X = E2, and the last with member X Rest. A more interesting scenario is when the compute tactic is used on a purely positive predicate that cannot be fully solved. For instance, given: H : nat ( s ( s X ) ) where X is an eigenvariable, it can be asynchronously simplified to (nat X) by just using the second clause of the definition of nat. However, to go further we would need to consider the cases where X = z and the case for X = s X1, and we would be left with a further assumption nat X1. We can repeat this process now  with X1 and so on. This eager treatment of nat not only leads to non-terminating search (which will eventually be forcefully terminating because it reaches a depth bound), but may be unwarranted before we know anything else about X. In this case, it would be useful to suspend the eager unfolding of nat. To account for this premature unfolding of definitions when the inductive structure is already a variable, we add a new kind of Suspend declaration that will make Abella stop the asynchronous phase prematurely as we described in Section 2.2. The following declaration declares that (nat X) should not be unfolded if X is a variable;we call this a suspension condition.

Table des matières

Introduction
1 The ℋ proof system for Heyting arithmetic 
1 The typed λ-calculus 
1.1 Syntax of terms
1.2 Typing using sequent calculus
1.3 Computing with the λ-calculus
2 Terms and formulas for ℋ
3 The ℋ sequent calculus 
3.1 The logical core of ℋ
3.2 The arithmetic part of ℋ
2 Separating functional computation from relations 
1 An introduction to focusing
1.1 The ℱ⊃ calculus
1.2 Polarity and proof search
2 The ℱ calculus for Heyting arithmetic
2.1 Polarities of connectives
2.2 Suspensions
2.3 The complete ℱ calculus
3 Juggling with phases
3.1 Phases as abstractions
3.2 The polarity ambiguity of singleton sets
3.3 An extension to equivalence classes
4 A practical use: automation in Abella
4.1 The ? Logic and the Abella Implementation
4.2 Proposal: Computation and Suspension
4.3 Proposal: Deterministic Computation using Singleton Predicates
4.4 Possible extensions
5 Conclusion and perspectives
3 A functional programming language using λ-tree syntax 
1 Introduction
1.1 A common example: substitution
1.2 A new language, MLTS
2 The new features of MLTS
3 MLTS examples 
3.1 The untyped λ-calculus
3.2 Higher-order programming examples
3.3 Normalization by Evaluation (NBE)
3.4 The π-calculus
4 Types and syntax
4.1 Abstract syntax as untyped λ-calculus
4.2 Typing for the concrete syntax
4.3 Typing for the explicit syntax
5 Formalizing the design of MLTS
5.1 Equality modulo α, β, η conversion
5.2 Pattern unification and matching
No repeated pattern variable occurrences
Restricted use of higher-order pattern variables
All nab-bound variables must have a rigid occurrence
5.3 β0 versus β
5.4 Match rule quantification
5.5 Nominal abstraction
6 Natural semantic specification 
7 Formal properties of MLTS 
8 Interpreters for MLTS 
8.1 Nominal-escape checking
8.2 Binder mobility
8.3 Costs of moving binders
8.4 A web frontend for the interpreter
9 Related work 
9.1 Systems with two arrow type constructors
9.2 Systems with one arrow type constructor
9.3 Systems using nominal logic
9.4 Challenge problems and benchmarks
10 Perspectives for MLTS 
Conclusion
A A unification algorithm in MLTS
B A prototype implementation for MLTS
1 Terms and types
2 Typing
3 Interpreter

Télécharger le rapport complet