Logic of refinement types

Susumu Hayashi^{∗} Department of Applied Mathematics and Informatics Ryukoku University Ohtsu, Shiga, JAPAN

Abstract

Refinement types are subsets of ordinary types, which are intended to be specifications of programs. Ordinary types correspond to constructive propositions by Curry-Howard isomorphism. Refinement types correspond to “classical” propositions by a semantics resembling interpretations of logics in categorical/algebraic logic. In this paper, we will study the logic of refinement types in the type system ATTT which was introduced in [9] as a framework for an “optimized” Curry-Howard isomorphism.

1 Introduction

ATTT is a conservative extension of Girard-Reynolds’ second order polymorphic lambda calculus λ2 (or F in more popular name). The aim of ATTT is to serve yet another type theoretic basis for program extraction or program development. In [9], the theory of pure ATTT was presented and its basic metatheory was developed. In this paper, we will study logics in ATTT. The main purpose of this paper is to show how logic is represented by refinements of ATTT. We will show that the refinements of each type is an “internally” complete Heyting algebra (cHa). Using the cHa structure, second order intuitionistic logic is naturally interpreted by refinements via the technique of categorical logic [15]. The second order formulas provable in the intuitionistic second order logic are provably true in ATTT under this interpretation. Conversely, the first order formulas provably true in ATTT under this interpretation are provable in the intuitionistic first order logic. We conjecture that this holds for the second order case as well and will give a sufficient condition.

The logic of refinements mentioned above is “non-informative” in the sense of Coq system [3] or “rank zero” in the sense of PX system [8]. Thus, it is a substitute of logics of Coq’s propositions and PX’s rank zero formulas. This means that the interpretation of formulas does not keep any computational information contrary to the ordinary BHK-interpretation (Brouwer-Heyting-Kolmogorov-interpretation) of constructive logic. Besides this non-informative interpretation, some BHK-style interpretations of logic can be coded in ATTT. They are essentially realizability interpretations. We will show that both of recursive realizability and modified realizability are represented naturally in ATTT. Then, we will show that informative induction principle is derivable by non-informative induction principle in ATTT.

We also introduce a notion of refinement classifier resembling subobject classifier of topos, and, by means of this notion, we will compare our approach to program/proof development in ATTT with related works [2], [3], [16], [20].

2 Refinement types

In this section, we will briefly review the notion of refinement types and develop cHa-structures of the refinements. The notion of refinement type was first introduced in [5]. We independently introduced a

∗hayashi@rins.st.ryukoku.ac.jp

Figure 1: Type, Set and Refinement Type

very similar notion for a rather different aim [9].^{1}

2.1 Types versus refinement types

A type is a collection of data which have the same uniform structure. A set is a collection of data which have the same property. Property which defines a set can be so complicated that we cannot effectively decide if a data belongs to the set. On the other hand, types of programming languages are supposed to be simple. For examples, integers, elements of free algebras, records and functions are all types. But, the primes are not a type. It is a set. We summarize this intuition by the following “doctrine”: the border of types are smooth and the border of sets are rugged.^{2} “The function f returns the next prime number to its real argument” is a specification of a function f. The boundary of the collection of data satisfying this specification is rugged, as it uses the primes in it.

Intuitively, specifications must be identified with sets. Thus, we think that the specifications should be distinguished from data types, even in the type theories for program extraction based on Curry-Howard isomorphism. This consideration led us to introduce a new kind of “types” called refinement types. Refinement types have rugged boundaries and are intended to serve as specifications. This refinement types refine the boundaries of types, i.e., they distinguish elements more refinedly than types. More precisely, a refinement types of type A is intended to be a subset of the ordinary type A. Note that a refinement type, or refinement in short, is not a subtype of A, since it may have a rugged boundary.

ATTT is a type system with refinement types designed as “ATTT = λ2 + refinement types.” In a sense , ATTT is “λ2 + logic.” In set theory, sets are defined by the aid of logical formulas. We do not introduce formulas but directly define set (refinements) by means of the rules for refinements in the framework of type theory. In categorical/algebraic logic, logics are coded through sets (subobject), e.g. the statement “F (x) implies G(x) ∨ H(x)” can be interpreted as set-theoretic inclusion {x|F (x)} ⊂ {x|G(x)} ∪ {x|H(x)}. Thus we may think that the set part (refinement part) of ATTT is a kind of logic without formulas. This resembles the philosophy of Martin-Löf’s type theory (at least his philosophy in 80’s). The difference is that Martin-Löf used Curry-Howard isomorphism to represent logic but we use the approach via categorical/algebraic logic. Note that we have not abandoned Martin-Löf’s philosophy. The categorical/algebraic logic approach is used only for non-informative part. For informative part, we follow Martin-Löf’s philosophy. In a sense, we use Curry-Howard isomorphism, when we sit in outside Martin-Löf’s subset type, and use categorical/algebraic logic approach, when we sit in inside Martin-Löf’s subset type.

1As our framework looked very similar to Freeman and Pfenning, we call our notion by the same name. The exact relationship is still unknown, but it seems fair to say that these are essentially the same notion.

2I learnt this doctrine from Rod Burstall. According him, it’s due to JȦṘobinson.

More formally, ATTT is described as follows. The types and terms of ATTT are exactly the ones of λ2. If A is a type of λ2 (and so of ATTT), we introduce the refinement kind of A, which we will write refine(A). A refinement kind is a sort of “kind” in the sense of GTS. The elements of the refinement kind refine(A) is intended to be the refinements of the type A. Each refinement kind refine(A) is closed under the formation rules of singleton {a}_{A} (a ∈ A), and unions R_{1} ∨ R_{2}, ⋁ x ∈ A.R and intersections R_{1} ∧ R_{2}, ⋀ x ∈ A.R. Furthermore, if R_{1} is in refine(A) and R_{2} is in refine(B), then R_{1} → R_{2} is in refine(A → B). This refinement type of functions represents the constructive implication. Natural introduction and elimination rules for these refinements are included. A subtle point is the introduction rule for the refinement R_{1} → R_{2}. If e ∈ R_{2} for x ∈ R_{1}, then the term λx ∈ A.e is introduced in R_{1} → R_{2}, and not λx ∈ R_{1}.e.^{3} The description of ATTT above would be enough to understand the development below. Thus we will not explain the details. See [9] for more details.

2.2 Refinement application

For the discussions below, we will introduce a notion refinement application. A future of ATTT is that the realizability relation “a realizes F ” is not only a judgment but also a refinement type. The relation is expressed as

F ∧ {a}.

This refinement is realized by a, if and only if, a belongs to F. If we consider a refinement of A as a predicate on A as we will do later, F ∧ {a} is considered the application of F to a. So we call this refinement application and write F {a}.

Note that Martin-Löf’s propositional equality I(F, a, a) is a proposition which expresses realizability relation. The refinement application resemble this. The difference is F {a} is realized by a, and I(F, a, a) is realized by a fixed constant.

2.3 The algebra of refinements

The refinement kind refine(A) is intended to be the subsets of the type A. So it has a lattice theoretic structure. ⋀ and ⋁ are “internal” infimum and supremum, respectively. Actually, they are an “internally” complete Heyting algebra. Namely, they are distributed “internally” complete lattice. To show it, we define an pre-order relation on refine(A). The relation itself is a refinements of refine(A → A).

Definition 1 (subset refinement) Let R_{1} and R_{2} be refinements of a type A. The subset refinement R_{1} ≤ R_{2} is defined as follows:

R_{1} ≤ R_{2} =^{def} ⋀ x ∈ R_{1}.(R_{1}{x} → R_{2}{x}).

The subset refinement is a refinement of type A → A. Intuitively, the subset refinement says that R_{1} is a subset of R_{2}. For this refinement the following proposition holds.

Proposition 1 Let A ∈ Type, R_{1} ∈ refine(A) and R_{2} ∈ refine(A) be derivable under a context Γ. Then, the following are equivalent:

3This rule is justified by the observation that terms of ATTT are exactly those of λ2 and the former lambda term is a term of λ2 but the latter is not. This rule also reflects modified realizabilities. Recently, Pfenning introduced a type theory with intersection types which has a function-introduction rule similar to ours for a different good reason [19].

1. Γ, x ∈ R_{1} ⊢ x ∈ R_{2} is derivable.

2. Γ ⊢ Id_{A} ∈ R_{1} ≤ R_{2} is derivable.

3. Γ ⊢ e ∈ R_{1} ≤ R_{2} is derivable for some term e.

Id_{A} is the identical function λx ∈ A.x. Note that the second condition shows that the identity function is the standard witness of the refinement. In this sense, the subset refinement is self-realizing or non-informative.

It is easy to see the subset refinement defines an pre-order relation on refine(A). Note that this fact can be stated internally. Namely, the followings are derivable in an appropriate context:

1. ⋀ R ∈ refine(A).R ≤ R,

2. ⋀ R_{1} ∈ refine(A). ⋀ R_{2} ∈ refine(A). ⋀ R_{3} ∈ refine(A).R_{1} ≤ R_{2} ⊃ R_{2} ≤ R_{3} ⊃ R_{1} ≤ R_{3}.

Note that “⊃” is the ordinary implication defined by the function space. Since the subset refinement is self-realizing, the implication may be replaced by non-informative implication explained later.

Since the subset relation is a pre-order, we have to consider the “equivalence relation” induced from the pre-order. This can be also internalized. Let’s call such an equivalence relation extensional equality refinement, R_{1} ≥≤ R_{2} in notation. It’s defined by

R_{1} ≥≤ R_{2} =^{def} (R_{1} ≤ R_{2}) ∧ (R_{2} ≤ R_{1}).

2.4 The refinements are internally complete Heyting algebra

The finite intersection and union are infimum and supremum, respectively. These facts can be stated internally as well as externally. As we have big intersections and unions, the refinements of a type are internally complete. For example, we can derive the followings for the big intersection:

…, i ∈ I ⊢ Id_{A} ∈ (⋀ i ∈ I.R) ≤ R

\frac{…, X ∈ refine(A), i ∈ I ⊢ e ∈ X ≤ R}{…, X ∈ refine(A) ⊢ X ≤ ⋀ x ∈ A.R}(i is not free in e)

Note that we have to be careful with what kind of indexes i ∈ I are allowed. It depends on what kind of formation rules for the intersection and union are allowed. But, once a formation rule is introduced, there is no difficulty to prove the properties above.

A complete Heyting algebra is a complete lattice with the following distribution law:

a ∧ ⋁ i ∈ I.b_{i} = ⋁ i ∈ I.(a ∧ b_{i}).

The distribution law is provable in ATTT.

Lemma 1 (the distribution lemma) Assume i is not free in R. In the contexts where R and S are refinements of a type A, the following refinement is provably inhabited.

R ∧ ⋁ i ∈ I.S ≥≤ ⋁ i ∈ I.(R ∧ S).

Note that I must be an index set (in the context) for which the formation of the big intersection allowed.

This lemma is not quite trivial. The ≥-direction is trivial, but the ≤-direction is not. In some type theories with intersection and union types, the distribution law is included as an axiom, as the ≤-direction is not derivable from the other axioms and rules. In ATTT, the ≤-direction is easily derivable by the following lemma:

Lemma 2 The following are derived rules of ATTT:

\frac{Γ ⊢ e_{0} ∈ ⋁ x ∈ A.B}{Γ ⊢ e_{0} ∈ ⋁ x ∈ A.(B ∧ \{e_{0}\})}

2.

\frac{Γ ⊢ e_{0} ∈ ⋁ x ∈ A.B Γ, x ∈ A, y ∈ B ∧ \{e_{0}\} ⊢ e_{1} ∈ C}{Γ ⊢ e_{1}[y:= e_{0}] ∈ C[y:= e_{0}]} ,

where x is not in F V (e_{1}) ∪ F V (C).

The second one is a consequence of the first one.

2.5 implication refinement

In cHa, implication a ⊃ b is defined as the greatest element c such that a ∧ c ≤ b holds. By the same vain, we define the implication refinement.

Definition 2 (implication refinement) Let R_{1} and R_{2} be refinements of a type A. Then we define the implication refinement R_{1} ˇ⊃ R_{2} by

⋁ R ∈ refine(A). ⋁ w ∈ R_{1} ∧ R ≤ R_{2}.R.

Note that the implication refinement is of type A and the subset refinement is of type A → A. For the implication refinement, the following two are equivalent:

Γ, a ∈ R_{1} ⊢ a ∈ R_{2},
Γ, a ∈ A ⊢ a ∈ R_{1} ˇ⊃ R_{2}.

This implies the equivalence of the followings:

Γ, a ∈ R_{1}{a} ⊢ a ∈ R_{2}{a},
Γ, a ∈ A ⊢ a ∈ (R_{1} ˇ⊃ R_{2}){a}.

By the commutativity, we can prove that (R_{1} ˇ⊃ R_{2}){a} and R_{1}{a} ˇ⊃ R_{2}{a} are extensionally equal refinements. If we abuse the notation, we have

Γ, R_{1}{a} ⊢ R_{2}{a},
Γ, a ∈ A ⊢ R_{1}{a} ˇ⊃ R_{2}{a}.

This shows that the implication refinement satisfies the standard rules for implication.

2.6 Absurdity refinement and truth refinement

The absurdity refinement of a type A, ⊥_{A}, is the least refinement and the negation refinement is defined from it and the implication.

⊥_{A} =^{def} ⋀ R ∈ refine(A).R,

ˇ¬R =^{def} R ˇ⊃ ⊥_{A}.

Obviously, the absurdity refinement implies any refinement of the same type. The truth refinement ⊤_{A}, which is the greatest refinement is also definable by

⊤_{A} =^{def} ⋁ R ∈ refine(A).R.

Normally, Heyting algebra is assumed to have at least two elements. But, we do not assume it in this paper. As a type may be empty in a semantics for λ2, we cannot prove the truth refinement is not the same as the absurdity refinement.

Note that ⊥ is not unique in ATTT. We have the absurdity ⊥ for each refinement kind. Later, we will show the refinement of the unit type unit classifies the refinements. Thus, ⊥_{unit} is the most general absurdity in a sense. If x ∈ A holds, then R{x} for any refinement R of A under the assumption ⊥_{unit}.

Proposition 2 The following is derivable in ATTT:

A ∈ Type, x ∈ A, R ∈ refine(A), w ∈ ⊥_{unit} ⊢ A ≤ R.

This means that any refinement is true, if we assume ⊥_{unit}.

3 Interpreting logic by refinements

In this section, we give an interpretation of second order logic by refinements. A refinement kind of a type A is the power set of A. Thus, refinement kinds resemble the algebras of subobjects in a category. We give an interpretation of second order predicate logic in ATTT using the technique of categorical logic by Makkai and Reyes [15]. But, our interpretation is not completely the same as theirs. Makkai and Reyes considered first order logic. We will consider second order logic. They used external intersections and unions, but we will use internal ones. Furthermore, products are assumed in [15]. We define product by the polymorphic product (see [9]). The polymorphic products are not real products but semi-products in the sense of [7] and [10], since λ2-part of ATTT does not have η-conversion.^{4}

3.1 The Makkai-Reyes-style interpretation

In spite of the differences mentioned above, Makkai-Reyes technique works well in our case by small modifications. Let’s illustrate the interpretation briefly. Let D be a fixed type. This is intended to be the domain of first order objects (ground type). Let F be second order formulas whose first order free variables are among x_{1}, …, x_{n}. Their interpretations are refinements of the type D^{n} (n-times product of D). F may have second order free variables. We assign refinements with appropriate types to the variables and the interpretation of F is defined depending on this assignment.

3.1.1 Interpretation of predicates

Let’s see how to interpret predicates by refinements. Since refinements are sets, they represent unary predicates. Thus, we use the polymorphic products and paring to interpret n-ary predicates. For example, a binary predicate P (x, y) is interpreted as a refinement R of the polymorphic product D × D. More precisely, we assign a refinement R of the type D × D to P, and interpret the formula P (x, y) by

{⟨x, y⟩ ∈ D × D|R{⟨x, y⟩}}.

The pair ⟨x, y⟩ is the polymorphic Church pairing and the subset notation is an abbreviation of

⋁ x ∈ D. ⋁ y ∈ D. ⋁ w ∈ R{⟨x, y⟩}.{⟨x, y⟩}_{D×D}.

See [9] for details.

3.1.2 Interpretation of logical operators

Conjunction, disjunction, implication and negation of formulas are interpreted as intersection, union, implication and negation of refinements. Note that implication is interpreted by implication refinement defined above. It is straightforward, but there is a problem.

4Note that we can define a refinement ⋁ a ∈ A. ⋁ b ∈ B.{⟨a, b⟩} of a polymorphic product A × B, which is the “real”

product. But, this trick would be incorrect, as a product of types should be a type.

If F and G have different free variables, this interpretation does not work, since their interpretations are of refinements of different types. Then, we embed refinements into a bigger refinements. Assume we are to form the union of the interpretations of F and G, say R_{F} and R_{G}. If F has a free variable x_{1} as F (x_{1}) and G has another free variable x_{2} as G(x_{1}, x_{2}). Then, R_{F} ∈ refine(D) and R_{G} ∈ refine(D × D). Thus, we must embed the interpretation of F (x_{1}) into D × D as {⟨x_{1}, x_{2}⟩ ∈ D × D|R_{F} {x_{1}}}.

Next we interpret the universal and existential quantifiers. This is the point at which our interpretation diverges from Makkai-Reyes interpretation. Makkai and Reyes interpret first order quantifiers by images and co-images of subobject morphisms. We interpret them by the big intersection and union over the type D. Let F (x_{1}, …, x_{n}) be a formula and let R_{F} be its interpretation, which is a refinement of D^{n}. The interpretation of the formula ∀x_{i}.F (x_{1}, …, x_{n}) is the refinement

⋀ x_{i} ∈ D.{⟨x_{1}, …, x_{i−1}, x_{i+1}, …, x_{n}⟩ ∈ D^{n−1}|R{⟨x_{1}, …, x_{n}⟩}}.

First order existential quantifier is interpreted in the similar way by union.

Since we have unions and intersections over refinement kinds, second order quantifiers are interpreted in the same way. For example, let P be a binary predicate variable. Then forallP.F is interpreted by ⋀ P ∈ refine(D^{2}).R_{F}. Note that P is a refinement of the polymorphic product D^{2}, which may have more elements than the real pairs. Thus, P may contain elements which are not pairs. But, this is not a problem, since P always appears in the form P {⟨s, t⟩} in F. This completes the definition of the interpretation of logic by refinements.

3.2 Provably true formulas in ATTT

A refinement R of a type A is said to be true, if and only if Id_{A} ∈ ⊤_{A} ≤ R holds. ^{5} If this judgment is provable in ATTT, we will say the refinement R is provably true in ATTT. If the interpretation of a formula F is provably true in ATTT, then we say the formula is provably true in ATTT.

3.2.1 Intuitionistic second order logic are provably true

Then, the following is easily proved:

Proposition 3 The intuitionistic second order predicate logic (ISOL) is sound w.r.t. the interpretation. Namely, if a closed formula F of ISOL is provable, then it is provably true in ATTT under the context D ∈ Type, x ∈ D, where the type variable D is used as the domain of first order objects.

The intuitionistic predicate logic assumes that the domain is non-empty. Thus, the assumption x ∈ D is necessary. If we use a free logic instead, this is not necessary.

3.2.2 What are provably true formulas?

It is natural to ask what are provably true formulas in ATTT. We conjecture that provably true formulas in ATTT are exactly the formulas provable in ISOL. This means that our interpretation is adequate to ISOL and amounts to the following:

Conjecture 1 The converse of proposition 3 holds. Namely, if a closed formula F of ISOL is provably true in ATTT under the context mentioned in proposition 3, then F is provable in ISOL.

Somehow related result is in [14]. Although, we have not been able to prove the conjecture yet, it is easy to prove the conjecture restricted to first order formulas. Namely, the following proposition holds:

Proposition 4 If a closed first order formula ϕ is provably true in ATTT under the context mentioned in the proposition above, then ϕ is provable in the intuitionistic first order predicate logic (IFOL).

5More exactly speaking, we have to respect in which context the refinement is true.

The idea of our proof is very simple. But, full details are rather clumsy. Thus, we illustrate only the idea, below.

Our proof consists three steps. First, we show that any provably true first order formula ϕ is valid in the sense of Tarski semantics by means of a term model of λ2. Secondly, we formalize the proof of this fact in the intuitionistic second order arithmetic (HAS) augmented with an auxiliary sort γ. The auxiliary sort is intended as the generic domain, i.e., we do not pose any axiom or rules for this except the ones of ISOL. Let us call this system HAS(γ). Then, we can show that ϕ^{γ}, that is ϕ made the sort to be γ, is provable in HAS(γ). Lastly, we show that if ϕ^{γ} is provable in HAS(γ) then ϕ is provable in IFOL. Thus, ϕ is provable in IFOL.

The first step is easy. If the judgment “the interpretation is true” is provable in ATTT under the context, we can interpret it in the set-theoretical semantics introduced in [9]. Let Const be a arbitrary set of new constants. We augment λ2 by Const as a new type. Namely, we introduce a new type constant D and regard the constants from Const as new constants of D. Let denote the augmented system by λ2(D). Let M be the closed term model of λ2(D).

In [9], we took BMM-model as the basis of semantics of ATTT. But, M is not a BMM-model but a λ2-algebra in the sense of [11]. This difference is not so important, since any concrete λ2-algebra also gives a semantics of ATTT in the sense of [9]. The reason why we considered only BMM-model in [9] was only for simplicity.

The model M consists of the collection of the set of closed normal terms of λ2(D). We denote the set of closed normal terms of type A by M(A). By interpreting refine(A) as the power set of the closed normal terms of type A, it becomes a model of ATTT (see [9]). Assume that a first order formula ϕ is provably true in ATTT, interpreting D is the domain of the first order objects. Since the normal closed terms of D are only the new constants, M(D) is identical to Const. Let x_{1}, …, x_{n} be the free variables of ϕ. Then, it is easy to check that R_{ϕ} (the interpretation of ϕ) coincides with the set of the list of constants ⟨c_{1}, …, c_{n}⟩ where ϕ[c_{1}/x_{1}, …, c_{n}/x_{n}] is valid in the sense of Tarski semantics whose domain is Const. Since Const is arbitrary, this means that ϕ is valid in any frame (a tautology) in the sense of Tarski semantics. Thus, ϕ is provable in the classical first order logic by the completeness theorem. Note that the argument above is all constructive except the completeness theorem.

The second step involves messy formalization.^{6} Let us clarify the system HAS(γ) in which we do the formalization. HAS(γ) is a second order theory with two sorts, ν and γ. The sort ν is intended to be the sort of natural numbers and the sort γ is intended to be arbitrary (generic). The constants of ν is only 0, and γ does not have any constants. The only function symbol is s (successor) for ν. The arity of a predicate variable is a list (s_{1}, …, s_{n}) of sorts (n is possibly zero). Thus we can talk about functions from ν to γ, etc. The equality for each sort is defined by Leibniz equality. (This is only for simplicity. We may have equality symbols, instead.) The logic is the two-sorted intuitionistic second order logic, and the axioms are the Peano axiom for the sort of natural numbers ν.

Now, we formalize the argument of the first step in HAS(γ). Note that only “pointwise” formalization is possible, since we need normalization theorem of λ2. Namely, we formalize the proof for each ϕ. First, we augment ATTT with D just as λ2(D). Let us denote the augmented system by ATTT(D). Assume that a first order formula ϕ is provably true in ATTT. Then it is also provably true in ATTT(D), regarding the new type D as the domain of the first order objects. Then there is a fragment of λ2(D) for which the strong normalization property of the terms is provable in HAS(γ) and all terms in the proof of the truth of ϕ fall in the fragment (see, e.g., [21]). Thus, we have a closed term model of the fragment of ATTT(D) formalized in HAS(γ). Since the set of constants Const is arbitrary, we may regard it as the sort γ. Recall that the Makkai-Reyes-style interpretation coincided with the Tarski semantics. Thus, we can conclude that ϕ^{γ} is provable in HAS(γ).

The third step consists of the following lemma:

Lemma 3 A first order formula ϕ is provable in intuitionistic first order logic, if ϕ^{γ} is provable in HAS(γ).

6It is possible to avoid the formalization by means of Kripke semantics. Then, we have to introduce a notion of Kripke semantics for λ2 as did by Mitchell and Moggi and extend any first order Kripke frame to a Kripke frame of λ2 by “free construction.” This is not easier than the formalization.

This is an easy consequence of an infinitary normalization theorem of intuitionistic second order arithmetic, which is proved by Tait-Girard computability predicate technique, e.g., [6]. A proof of ϕ^{γ} of HAS(γ) can be normalized using ω-rule. Since ϕ^{γ} is a first order formula only with the sort γ, subformula property holds, i.e., the sort appearing in the normal proof is only γ. This means that the proof is of intuitionistic first order logic, regarding the sort γ as the ground sort. This completes the proof.

The only third step fails for the second order case. Since second order logic does not have subformula property, our proof fails to prove the lemma above for second order case. But, we conjecture that the lemma will hold for second order formulas as well.

Conjecture 2 A formula ϕ of second order predicate logic is provable in intuitionistic second order predicate logic, iff ϕ^{γ} is provable in HAS(γ).

Note that this lemma has an intrinsic meaning: if a second order formula is constructively valid under the assumption of the existence of the natural numbers, then it is provable in second order intuitionistic logic. Since this seems very plausible, the conjecture must be true.

Remark 1 The reduction to the original conjecture to the conjecture on HAS(γ) seem unnatural, as the original conjecture does not involve natural numbers. But, if the conjecture on HAS(γ) is once proved, then it will be straightforward to change it to a proof of the original conjecture via Kripke semantics of λ2. In such a proof, arithmetic part and even formalization part will vanish. Actually, it is possible to give a sufficient condition by means of Kripke frames of λ2. But, the sufficient condition by means of HAS(γ) is easier to understand and has an intrinsic meaning as noted above.

3.3 The excluded middle

The law of excluded middle for refinements

ΠA ∈ Type. ⋀ R ∈ refine(A).(⊤_{A} ≤ R ∨ ˇ¬R)

or

ΠA ∈ Type. ⋀ R ∈ refine(A).(¬¬R ≤ R).

is not derivable in ATTT by the the adequacy result above. Thus, the Heyting algebra of a refinement kind is not boolean. But, they are compatible with boolean laws. Even if we add the law of excluded middle above as an axiom, the system is still conservative over λ2. In [9], we defined a translation from ATTT to λ2 which is identical on the λ2 fragment of ATTT. We may add the excluded middle above as an axiom, whose realizer is the identity function. Then the two forms of the classical axioms above are both translated to Id_{A} ∈ A → A. This resembles the logic of PX system, which is compatible with classical logic as stressed in [8].

3.4 The refinement classifier and comparisons to the other approaches

The Makkai-Reyes-style interpretation given above look rather different from the standard way of interpreting logic in higher order type systems as Coq system. Thus, it seems difficult to compare our approach to the standard ones. But, we can encode logic similarly to the standard way by the notion of refinement classifier. Upon the idea, we can compare our approach to the others.

3.4.1 The refinement classifier

Refinements resembles subobjects in toposes. A topos has a subobject classifiers by which subobjects are classified. Namely, a subobject of an object is represented by a map from the object to the subobject classifier. Intuitively, a subobject classifier is the power set of a singleton set. It can be considered as the set of truth values. Introducing a singleton type, say unit, consisting the only element ⋆, the refinement kind refine(unit) is a refinement classifier. Note that this is the kind of non-informative propositions, and so corresponds to Prop in the sense of Coq system rather than the Prop in the sense of the original Calculus of Constructions.

We will write the refinement kind refine(unit) by Ω and call it the refinement classifier. Assume that R ∈ refine(A). Then we define a term of the type A → Ω. Then the following correspondence between A → Ω and refine(A) is obtained:

R ∈ refine(A) ⟼ λx ∈ A. ⋁ w ∈ R{x}.{⋆},
ϕ ∈ A → Ω ⟼ ⋁ x ∈ A. ⋁ w ∈ ϕ(x){⋆}.{x}.

But, A → Ω is illegal in ATTT in [9]. Thus, we have to extend ATTT to include such a type by allowing the following formation rule and corresponding introduction rule.

\frac{Γ ⊢ A ∈ Type Γ ⊢ B ∈ RKind}{Γ ⊢ A → B ∈ RKind}

This extension is not essential. In such a extension, any term of RKind has the form A_{1} → … A_{n} → refine(B), where A_{1}, …, A_{n} are types. Then, we can regard it as refine(A_{1} × … × A_{n} × B), by regarding λx_{1} ∈ A_{1}. · · · λx_{n} ∈ A_{n}.R as {⟨x_{1}, … x_{n}, y⟩ ∈ A_{1} × ⋯ A_{n} × B|R{y}}. Note that this is a standard technique to encode functions from first order objects to predicates in the second order logic. Thus, the extension still keep the second order character.

3.4.2 Comparisons to the other approach

Upon the notion of refinement classifier, we compare our approach to the others. In impredicative higher order type theories as Calculus of Constructions, Type (or often denoted as Prop) is often used as a substitute for the collection of the truth values. It is also regarded as the collection of the data types. This confusion leads to inefficiency of the extracted code and makes it difficult to understand encoded logic. Thus, Coq system separate these two notions by introducing two kinds Prop and Set. The kinds Prop and Set belong to the sorts (in the sense of GTS) Type and Type Set, respectively. Note the messy confusion of symbols. Prop of Coq corresponds to our Ω and Set of Coq corresponds to our Type, the kind of the types. Type of ATTT belongs to the sort Kind and refinement kinds refine(A) belong to the sort RKind. Thus, Type of Coq is our Kind and Type Set is our RKind.

The superficial divergences of our approach from Coq’s are

1. . ATTT is a second order system, but Coq is a higher order system.

2. . The types of Coq can depend on data, as it is based on Calculus of Construction. The types of ATTT cannot depend on data, as it is based on λ2.

There is still another twist. Coq has an extraction algorithm, by which the data-dependency of types (and other logical information) is stripped out so that the extracted codes are of Girard’s F_{ω}. At the specification level, Coq has data-dependent types, but, at the object code level, it does not. The types of ATTT are the ones of λ2 at the both levels. In ATTT, we directly talk about object level codes and their types, i.e. the terms and types of λ2. On the other hand, the users of Coq talk about them indirectly through the extraction procedure. This is a fate of the systems based on realizability as Coq and PX. This might not be a bad doom, as the indirectness can make users think their programs abstractly and good extraction procedure can sometime produce better codes than the users expect. This contrast between direct and indirect approaches may be compared with the contrast between assembler languages and compiler languages.

Another approach closely related to Coq is “deliverable” by Burstall and McKinna ([2], [16]). They take a direct approach. They do not consider any extraction algorithm, but directly talk about codes. To represent data types and talk about them and codes, they use Luo’s Extended Calculus of Constructions ECC ([12], [13]). ECC has Prop and a predicative cumulative hierarchy of kinds Type(0), Type(1), . . .. They use Prop as the truth values and Type(i) as data types. Thus, Prop corresponds to our Ω. But, there is a difference. Prop is an element and also a subset of Type(0). This implies that the collection of truth values and each truth value is a data type. It would be possible to regard the collection of truth values as a data type by regarding them as formulas. But, a proposition (truth value) is a refinement of a unit type from our point of view. Thus, it has a rugged border, and so it is not a data type. When it comes to data-dependency of types, deliverable approach allows it. The predicative hierarchy allows such types.

The approach most closed to ours is Erik Poll’s programming logic λω_{L} [20]. As programming language, he uses Girard’s F_{ω}, λω in his notation. As logic, he uses the other copy of λω. His ∗_{s} is Type and ∗_{p} is Ω of ATTT. These two copies of the same type theory resembles two copies of Calculus of Constructions in the Coq system. Then he introduce function types from a data type A to ∗_{p} to represent predicates. This corresponds to the refinement kind refine(A) or A → Ω. The data-dependency of types is not allowed as he uses F_{ω}. In a sense, λω_{L} is a higher order version of ATTT without refinements. The difference is that Poll uses predicates, on the other hand, we use sets (refinement types). Since propositions and data types, and so programs and proofs, are more clearly separated in λω_{L} than ECC, λω_{L} might be a better framework for the deliverable approach.

As illustrated above, the four approaches are closely related in rather intricate ways. They do not seem very different from a theoretical point of view. The difference in practice of proof/program developments should be investigated.

4 Informative interpretations of logic

The logic of refinements given above is a non-informative interpretation. In this section, we examine two informative interpretations in ATTT.

4.1 Two informative interpretations of implication

Type theories based on “proofs as program” notion can be regarded as axiomatizations of realizability notions. For example, Martin-Löf’s type theory can be regarded as an axiomatization of extensional recursive realizability as exploited in [1].

In PX system, realizers of non-informative formulas are always the empty list which are passed by extracted codes. In Coq system, realizers of non-informative formulas are the null sequence which literally disappear in extracted codes. These two treatments of non-informativeness reflect the different realizability interpretations used by those systems. PX uses recursive realizability and Coq uses modified realizability.

The difference of these realizabilities appears in the interpretation of implication. Let P be a noninformative formula and let A be an informative formula. In recursive realizability,

r realizes P ⊃ A =^{def} r ↓ ∧P ⊃ r(nil) realizes A.

In modified realizability,

r realizes P ⊃ A =^{def} r ↓ ∧P ⊃ r realizes A.

(Normally, only terminating terms are used in modified realizability. Then, the condition r ↓ may be omitted.) In ATTT, user can choose both interpretations locally. Let R_{1} and R_{2} be refinements. The standard intuitionistic implication is defined by R_{1} → R_{2}. This interpretation takes R_{1} informative.

The following interpretations take R_{1} non-informative:

1. ⋀ w ∈ R_{1}.R_{2},

2. {x ∈ unit|R_{1}} → R_{2},

w is a fresh variable which does not appear in R_{2}. The first one represents the implication of the modified realizability, and the second one represents the implication of the recursive realizability. In this sense, ATTT embodies both realizabilities in a single framework.

4.2 Induction principles

Induction principle is a very important component of a system of constructive programming, since it is the device to derive recursive programs. Below, we will examine two kinds of induction principles, one is non-informative and the other is informative.

The non-informative one is purely logical. The informative one is not only logical but also representing recursion scheme as well. For example, informative mathematical induction represents primitive recursion and its correctness. We will show that informative induction principle can be derived from non-informative induction principle in ATTT. This is a future which distinguishes ATTT from the other type theories.

4.3 Monotone inductive definition of refinements

First, we will examine non-informative induction principles. They are induction principles over refinements. The monotone inductive definition of refinements are easily defined as in the second order logic. Let R be a refinement variable of type A and let Ψ(R) be a refinement of A. Then, μR.Ψ(R) is

⋀ S ∈ refine(A). ⋀ w ∈ (Ψ(S) ≤ S).S.

If Ψ(S) ≤ S holds, then μR.Ψ(R) ≤ S obviously holds. If Φ is monotone, i.e., R_{1} ≤ R_{2} ⊃ Φ(R_{1}) ≤ Φ(R_{2}), holds, then Φ(μR.Ψ(R)) ≥≤ μR.Ψ(R) holds. In this sense, μR.Ψ(R) is the least fixed point of a monotone operator Φ(R).

4.4 The type of natural numbers

Recursive data types as integers, list, etc. are definable in λ2. For example, natural numbers are definable as Church integers. But, we do not use this as data types. We should introduce such types as primitive type as in [3]. For simplicity, we consider only Nat, here.

To extend ATTT by Nat, we introduce a type constant Nat and two constants 0 ∈ Nat and S ∈ Nat → Nat. Then, we add the primitive recursor rec

rec ∈ ΠX ∈ Type.X → (Nat → X → X) → Nat → X

together with the standard reductions.

To say Nat is built by 0 and S, we introduce the following axiom:

Nat ≤ μR.({0}_{Nat} ∨ S′′R),

where S′′R is the image of R by S, which is defined by

f′′R =^{def} ⋁ x ∈ R.{f(x)}.

Since Nat is not a refinement, “Nat ≤ μR. …” is not the order on refinements. This is defined by ⋀ x ∈ Nat.{x}_{Nat} → (μR. …){x}.

As the axiom is self-realizing by the identity function, the axiom may be put in the context with a variable, which is a virtual witness of the axiom.

Note that we did not introduce the informative mathematical induction. The last axiom is a kind of mathematical induction, but it is non-informative mathematical induction (NIMI). The informative mathematical induction (IMI) should be

ΠA ∈ Type. ⋀ P ∈ Nat → Ω.P (0) → Πn ∈ Nat.(P (n) → P (Sn)) → Πn ∈ Nat.P (n).

In ATTT, IMI is provable from the axioms above.

Theorem 1 The following is derivable in ATTT:

λA ∈ Type.λa ∈ Nat.λf ∈ Nat → A → A.λn ∈ Nat.recAafn ∈ IMI.

Note that we have to put the abstractions, since ATTT does not have η-conversion. Note that this theorem asserts that the λ-term above is the realizer of IMI. Let e(n) be the term recAafn. It is enough to prove e(n) ∈ P (n) under the assumptions. To prove this, it is sufficient to prove the refinement P (n){e(n)}. We can prove this by the non-informative mathematical induction NIMI. The proof is essentially the same as the soundness proof of mathematical induction for realizabilities.

This example shows that informative induction follows from non-informative induction in ATTT. This ability of ATTT distinguishes it from the other type theories and illustrates its set theoretical nature.

There is one thing missing in the axioms above. It is Peano’s fourth axiom “0 = 1 implies ⊥.” There are several formulations of the axiom, since we have several ways to define implication and absurdity. One of the strongest formulation would be

ΠA ∈ Type. ⋀ w ∈ 0 = 1.⊥_{A}.

The type of this refinement is ΠA ∈ Type.A. This is rather problematic as pointed out in [18]. If the refinement is realized by f, then f(A) is a polymorphic element of A. In PX system, this problem did not arise, as it is a monotype system whose domain is inhabited. But, we are now in a type theoretic framework and so cannot use such a solution. In Coq system [18], “abort”-command is introduced which belongs polymorphically to any type A. This solution seems to lead us to a type theory with non-terminating programs. Coq system offers a solution, but it is not very clear to me.

This approach resembles the resent works on controls in Curry-Howard isomorphisms by Griffin, Murthy, Nakano. Especially, Nakano’s calculus accommodate catch/throw mechanism in a natural constructive framework [17]. As “abort” is a throw to the top-level, there might be a natural way to interpret this problem by Nakano’s calculus.

Anyway, the problem does not seem to have been settled satisfactory. Thus, we do not use it but consider a less ambitious formulation

ΠA ∈ Type. ⋀ w ∈ 0 = 1.A → ⊥_{A},

which is equivalent to

⋀ w ∈ 0 = 1.⊥_{unit}.

In Coq system, essentially the same statement is proved by a proof by cases, which is similar to Martin-Löf’s proof of the 4th axiom in his type theory. If we introduce a principle to define refinement-valued functions by cases, we can do the same thing in ATTT. Assume that we can define the following program from Nat to Ω.

λx ∈ Nat.(if x = 0 then ⊤_{unit} else ⊥_{unit}).

By assuming 0 = 1, we can convert ⊤_{unit} to ⊥_{unit}. This proves the axiom above by means of conversion rule or an appropriate equality rule. Note that the program above have the type Nat → refine(unit). If we extend the type of the recursor rec so that it permits refinement kinds as well as the type A, then we can do such a definition by cases. This does not seem bad. But we do not do so here. We simply add the axiom to the system.

Note that type A is assumed to be non-empty, when we deduce ⊥_{A}:

ΠA ∈ Type. ⋀ w ∈ 0 = 1.A → ⊥_{A}.

This means that “have an element of A and return it as the default value if something is wrong.” The non-emptiness assumption would not cause a big problem in practical cases. Such an A would be the type of a specification. A specification of a program of a type whose elements are not known would be meaningless. Thus we may suppose the type is inhabited.

Acknowledgments

I am very grateful to Rod Burstall and Henk Barendregt for inviting me to the BRA workshop ”Types for Proofs and Programs” and for opportunity to present the paper. I thank Christine Paulin, Erik Poll, Kees Hemerik, Benjamin Werner, Mariko Yasugi for discussions on the subjects of the paper and/or Coq system which helped me to clarify the nature of ATTT.

References

[1] M.J. Beeson, Foundations of Constructive Mathematics, Springer-Verlag, 1985.

[2] R.M. Burstall and J. H. McKinna, Deliverables: an approach to program in Constructions, Technical Report ECS-LFCS-91-133, Department of Computer Science, The University of Edinburgh, 1991.

[3] Dowek, C. et al., The Coq Proof Assistant User’s Guide, Version 5.6, Technical Report No. 134, INRIA, December, 1991.

[4] Th. Coquand and G. Huet, Calculus of Constructions, Information and Computation, vol. 76, pp. 95-120, 1988.

[5] T. Freeman and F. Pfenning, Refinement Types for ML, ACM SIGPLAN’91, Conference on Programming Language Design and Implementation, Toronto, Ontario, ACM Press, 1991.

[6] S. Hayashi, On derived rules of intuitionistic second order arithmetic, Commentariorum Mathematicorum Universitatis Sancti Pauli, vol. XXVI, pp. 77-103, 1977.

[7] S. Hayashi, Adjunction of semifunctors: categorical structures in non-extensional lambda calculus, Theoretical Computer Sciences,, vol. 41, pp.95-104, 1986.

[8] S. Hayashi and H. Nakano, PX: A Computational Logic, The MIT Press, 1988.

[9] S. Hayashi, Singleton, Union and Intersection Types for Program Extraction, Lecture Notes in Computer Science No. 526, pp. 701-730, T.Ito and A.R.Meyer, eds., Springer-Verlag, 1991, an extended version to appear in Information and Computation.

[10] R. Hoofman, The theory of semi-functors, Mathematical Structures in Computer Science, vol. 3, pp.93-128, 1993.

[11] B. Jacobs, Semantics of the second order lambda calculus, Mathematical Structures in Computer Science, vol. 1, pp. 327-360, 1991.

[12] Z. Luo. ECC, an Extended Calculus of Constructions, in Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, Asilomar, California, 1989.

[13] Z. Luo. An Extended Calculus of Constructions, Ph. D. thesis, Department of Computer Science, The University of Edinburgh, 1990.

[14] Z. Luo. A problem of adequacy: conservativity of Calculus of Constructions over higher order logic, Technical Report ECS-LFCS-90-121, Department of Computer Science, The University of Edinburgh, 1990.

[15] M. Makkai and G. Reyes. First Order Categorical Logic, Lecture Note in Mathematics No. 611, 1977, Springer-Verlag.

[16] J. H. McKinna. Deliverables: A Categorical Approach to Program Development in Type Theory, Ph. D. thesis, Department of Computer Science, The University of Edinburgh, 1992.

[17] , H. Nakano. A Constructive Formalization of the Catch and Throw Mechanism, in Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, 1992.

[18] C. Paulin-Mohring and B. Werner, Synthesis of ML programs in the System Coq, Journal of Symbolic Computation, 1993.

[19] F. Pfenning, Intersection Types for a Logical Framework, in this volume, 1992.

[20] Erik Poll, A programming logic for F_{ω}, Computing Science Notes, 92/25, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1992.

[21] A.S. Troelstra, Metamathematical investigations of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, 1973.