An Extension of Martin-Löf’s Type Theory with an Evolution Relation

Tadao Ishii

                            ishii@jaist.ac.jp

School of Information Science, Japan Advanced Institute of Science and Technology

In this note, we will extend Martin-Löf’s type theory by introducing an evolution relation between types and also expressions (similar discussions are found in [1]). The purpose is to formalize the software evolution problem proposed by T. Katayama in [2] under the constructive type theory [3,4].

1 Introduction

As a method of maintaining and/or producing a large scale of software rapidly, the software evolution problem was proposed by T. Katayama in [2]. Here software evolution means to the mechanism that software can change its structure and functions to adapt changes of its requirements and environment.

Let 𝕊 = ⟨S, ⊑⟩ and ℙ = ⟨P, ⊑⟩ be the structures of specification and program, respectively. Then in general, software evolution problem is defined as finding a new program P′ of a new specification S′, in symbols, P′ ⊢ S′ under the assumption that the program P of S is given, P ⊢ S and the specification S changes to S′, in symbols S ⊑ S′. Here, if the change S ⊑ S′ is arbitrary, then we should make P′ newly and software evolution problem does not arise. In [2], there are explanations of two typical evolutional patterns:

(1) P ⊢ S and S ⊑ S′ : if we calculate the difference of specifications S′ and S, in symbols, ΔS = Diff(S′, S) and derive the program ΔP corresponding to this difference ΔS, ΔP ⊢ ΔS then the desired program P′ is obtained by merging two programs P and ΔP, in symbols, P′ = Sup(P, ΔP).

(2) P ⊢ S, T ⊑ S and T ⊑ S′ : if ΔS = Diff(S′, T), ΔP ⊢ ΔS and derive the program Q of T by degenerating the original program P with ΔP, in symbols, Q = Diff(P, ΔP) then the desired program P′ is obtained by applying pattern (1).

2 Martin-Löf’s Type Theory

In this section we will introduce Martin-Löf’s type theory (MTT in short) [3,4]. Since MTT is one of the predicative type theory, in general MTT has a universe type U_{n} (n = 0, 1, 2, …). But in this investigation we will omit to include universes type U_{n} (and also well orderings type W) for the sake of simplicity. MTT has its two major syntactical categories, that is MTT-type and MTT-expression. Here the MTT-types are words over the alphabet and Greek letters such that (1) constants : finite set type N_{n} (n = 0, 1, …) and natural number set type N (here we abbreviate empty set type as ⊥ (= ∅ = N_{0}) and singleton set type as T (= N_{1})), (2) symbols : type constructors Π, Σ, +, I, types A, B, C, …, objects a, b, c, …, object variables x, y, z, …, parentheses (,) and membership relation ∈.

Definition 2.1 The set of MTT-types T is defined inductively as follows:

(i) all constants N_{n} (n = 0, 1, …), N, ⊥ and T are MTT-types (called atomic types),

(ii) if A and B are any MTT-types and x ∈ A is any object variable, then (Πx ∈ A)B(x) is a MTTtype (called dependent product type), (iii) if A and B are any MTT-types and x ∈ A is any object variable, then (Σx ∈ A)B(x) is a MTT-type

(called dependent sum type),

(iv) if A and B are any MTT-types, then A + B is a MTT-type (called direct sum type),

(v) if A is any MTT-type and a, b ∈ A are any objects, then I(A, a, b) is a MTT-type (called propositional equality type).

On the other hand, the MTT-expressions are words over the alphabet and Greek letters such that (1) constant : elements of finite set m_{n} (n = 0, 1, …; m = 0, 1, …, n − 1), natural number 0, here ϵ and t (= 0_{1}) are abbreviation of empty element and singleton element, respectively, (2) variables : x, y, z, …,

(3) symbols : form constructors Ap, E, D, J, R_{n} (n = 0, 1, …), R, functional abstraction λ, indices of set i, j, successor function succ, objects a, b, c, …, parentheses or ordered pair (,).

Definition 2.2 The set of MTT-expressions E is defined inductively as follows (notice that [,] denotes the assumptions) :

(i) all variables x, y, z, … and constants m_{n} (n = 0, 1, …; m = 0, 1, …, n − 1), 0, ϵ and t are MTTexpresssions (called atomic expressions),

(ii) if a ∈ A, b(x) ∈ B(x) [x ∈ A] and c ∈ (Πx ∈ A)B(x) are any MTT-expressions, then (λx)b(x) ∈ (Πx ∈ A)B(x) and Ap(c, a) ∈ B(a) are MTT-expressions (called canonical and noncanonical expressions of the type (Πx ∈ A)B(x), respectively),

(iii) if a ∈ A, b ∈ B(a), c ∈ (Σx ∈ A)B(x) and d(x, y) ∈ C((x, y)) [x ∈ A, y ∈ B(x)] are any MTTexpressions, then (a, b) ∈ (Σx ∈ A)B(x) and E(c, d(x, y)) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type (Σx ∈ A)B(x), respectively),

(iv) if a ∈ A, b ∈ B, c ∈ A + B, d(x) ∈ C(i(x)) [x ∈ A] and e(y) ∈ C(j(y)) [y ∈ B] are any MTTexpressions, then i(a), j(b) ∈ A + B and D(c, d(x), e(y)) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type A + B, respectively),

(v) if a, b ∈ A, c ∈ I(A, a, b) and d ∈ C(r) are any MTT-expressions, then r ∈ I(A, a, b) and J(c, d) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type I(A, a, b), respectively),

(vi) if c, m_{n} ∈ N_{n} (n = 0, 1, …; m = 0, 1, …, n − 1) and c_{m} ∈ C(m_{n}) are any MTT- expressions, then m_{n} ∈ N_{n} and R_{n}(c, c_{0}, c_{1}, …, c_{n−1}) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type N_{n} (n = 0, 1, …)), respectively,

(vii) if 0, a, c ∈ N, d ∈ C(0) and e(x, y) ∈ C(succ(x)) [x ∈ N, y ∈ C(x)] are any MTT-expressions, then 0, succ(a) ∈ N and R(c, d, e(x, y)) ∈ C(c) are MTT-expressions (called canonical and noncanonical expressions of the type N, respectively).

The theory of type MTT can evaluate each MTT-expression like a reduction of term in λ-calculus. One reduction (i.e., evaluation) of MTT-expression is performed by simultaneously substitutions. After evaluating MTT-expressions, if a MTT-expression in some MTT-type has itself as a value of substitution, then we will call this expression to canonical form, and otherwise to noncanonical form of this type. For any expressions a ∈ A and b ∈ B, an expression a is equal to b, in symbols, a = b ∈ A if two expressions a, b have the same canonical form. Moreover, for any types A and B, a type A is equal to B, in symbols, A = B if for two canonical forms c_{A} ∈ A and c_{B} ∈ B, it holds that c_{A} = c_{B} ∈ A.

Under the following judgments, the theory of type MTT is axiomatized as Gentzen’s natural deduction style. We will omit to show each individual inference rule now (see [3,4]).

(1) A type : A is a type.

(2) a ∈ A : a is an object of type A.

(3) a = b ∈ A : a and b are equal objects of type A.

(4) A = B : A and B are equal types.

3 Evolution relation and its related operations

In this section we will introduce the notion of evolution relation ⊑ between MTT-types and also expressions. Then we will define some basic operations, i.e., supremum, infimum and difference operations related to this order. Here our idea is that we can order every similar types (generated by the same type constructor) in MTT from the viewpoint of an evolutional relationship by replacing some atomic types in these types with the unit type T, since only N_{n} (n = 0, 1, …) and N are atomic types in MTT and the type T = (N_{1}), which denotes a singleton set, has a noncanonical form R_{1}(c, t) that is corresponding to NOP operation in the programs.

Any MTT-expression b is degenerated according to the following rule : b[t, …, t /b_{1}, …, b_{n}], where this denotes the result of simultaneously replacements of some atomic expressions b_{1}, …, b_{n} in b by the singleton element t ∈ T. For any expressions a ∈ A and b ∈ B, an expression a is evolved to b, in symbols, a ⊑ b ∈ A if for some atomic expressions b_{1}, …, b_{n} ∈ At(b), it holds that b[t, …, t /b_{1}, …, b_{n}] = a ∈ A. Moreover, for any types A and B, a type A is evolved to B, in symbols, A ⊑ B if for two canonical forms c_{A} ∈ A and c_{B} ∈ B, it holds that c_{A} ⊑ c_{B} ∈ A. According to the above definition of an evolution relation, we will define the evolution relation of MTT-types and expressions individually below under the assumption that each type and form constructors are continuous.

Definition 3.1 For any types A and B in T , the evolution relation A ⊑ B of type, is defined inductively as follows:

(i) For any interpretations C : N_{k} → T and D : N_{l} → T , if ⋃_{m=0}^{k−1} C(m_{k}) ⊆ ⋃_{m=0}^{l−1} D(m_{l}), then N_{k} ⊑ N_{l} (k, l = 0, 1, …; k ≤ l).

(ii) N ⊑ N and ⊥ ⊑ T.

(iii) If A_{1} ⊑ A_{2} and B_{1}(x_{1}) ⊑ B_{2}(x_{2}) [x_{1} ∈ A_{1}, x_{2} ∈ A_{2}], then (Πx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Πx_{2} ∈ A_{2})B_{2}(x_{2}).

(iv) If A_{1} ⊑ A_{2} and B_{1}(x_{1}) ⊑ B_{2}(x_{2}) [x_{1} ∈ A_{1}, x_{2} ∈ A_{2}], then (Σx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Σx_{2} ∈ A_{2})B_{2}(x_{2}).

(v) If A_{1} ⊑ A_{2} and B_{1} ⊑ B_{2}, then A_{1} + B_{1} ⊑ A_{2} + B_{2}.

(vi) If A_{1} ⊑ A_{2} and a_{1} ⊑ a_{2} ∈ A_{1} and b_{1} ⊑ b_{2} ∈ A_{1}, then I(A_{1}, a_{1}, b_{1}) ⊑ I(A_{2}, a_{2}, b_{2}).

Definition 3.2 For any expressions a ∈ A and b ∈ B in E, the evolution relation a ⊑ b ∈ A of expression, is defined inductively as follows:

(i) For any object variables x ∈ A and y ∈ B in E such that A ⊑ B, x ⊑ y ∈ A.

(ii) For any m_{k} ∈ N_{k} and m_{l} ∈ N_{l} (k, l = 0, 1, …; k ≤ l), if C(m_{k}) ⊆ D(m_{l}), then m_{k} ⊑ m_{l} ∈ N_{k}.

(iii) 0 ⊑ 0 ∈ N and ϵ ⊑ t ∈ ⊥.

(iv) If A_{1} ⊑ A_{2} and b_{1}(x_{1}) ⊑ b_{2}(x_{2}) [x_{1} ∈ A_{1}, x_{2} ∈ A_{2}], then (λx_{1})b_{1}(x_{1}) ⊑ (λx_{2})b_{2}(x_{2}) ∈ (Πx_{1} ∈ A_{1})B_{1}(x_{1}). Moreover, if c_{1} ⊑ c_{2} ∈ (Πx_{1} ∈ A_{1})B_{1}(x_{1}) and a_{1} ⊑ a_{2} ∈ A_{1}, then Ap(c_{1}, a_{1}) ⊑ Ap(c_{2}, a_{2}) ∈ B_{1}(a_{1}).

(v) If a_{1} ⊑ a_{2} ∈ A_{1} and b_{1}(a_{1}) ⊑ b_{2}(a_{2}) ∈ B_{1}(a_{1}) [a_{1} ∈ A_{1}, a_{2} ∈ A_{2}], then (a_{1}, b_{1}) ⊑ (a_{2}, b_{2}) ∈ (Σx_{1} ∈ A_{1})B_{1}(x_{1}). Moreover, if c_{1} ⊑ c_{2} ∈ (Σx_{1} ∈ A_{1})B_{1}(x_{1}) and d_{1}(x_{1}, y_{1}) ⊑ d_{2}(x_{2}, y_{2}) ∈ C_{1}((x_{1}, y_{1})), then E(c_{1}, d_{1}(x_{1}, y_{1})) ⊑ E(c_{2}, d_{2}(x_{2}, y_{2})) ∈ C_{1}(c_{1}).

(vi) If a_{1} ⊑ a_{2} ∈ A_{1} and b_{1} ⊑ b_{2} ∈ B_{1}, then i(a_{1}) ⊑ i(a_{2}), j(b_{1}) ⊑ j(b_{2}) ∈ A_{1} + B_{1}. Moreover, if c_{1} ⊑ c_{2} ∈ A_{1} + B_{1}, d_{1}(x_{1}) ⊑ d_{2}(x_{2}) ∈ C_{1}(i(x_{1})) [x_{1} ⊑ x_{2} ∈ A_{1}] and e_{1}(y_{1}) ⊑ e_{2}(y_{2}) ∈ C_{1}(j(y_{1})) [y_{1} ⊑ y_{2} ∈ B_{1}], then D(c_{1}, d_{1}(x_{1}), e_{1}(y_{1})) ⊑ D(c_{2}, d_{2}(x_{2}), e_{2}(y_{2})) ∈ C_{1}(c_{1}).

(vii) If a_{1} = b_{1} ∈ A_{1}, a_{2} = b_{2} ∈ A_{2}, a_{1} ⊑ a_{2} ∈ A_{1} and b_{1} ⊑ b_{2} ∈ A_{1}, then r_{1} ⊑ r_{2} ∈ I(A_{1}, a_{1}, b_{1}). Moreover, if c_{1} ⊑ c_{2} ∈ I(A_{1}, a_{1}, b_{1}) and d_{1} ⊑ d_{2} ∈ C_{1}(r_{1}), then J(c_{1}, d_{1}) ⊑ J(c_{2}, d_{2}) ∈ C_{1}(c_{1}).

(viii) If c_{1} ⊑ c_{2} ∈ N_{k} and a_{m} ⊑ b_{m′} ∈ C_{1}(m_{k}) (m = 0, 1, …, k − 1; m′ = 0, 1, …, l − 1), then R_{k}(c_{1}, a_{0}, a_{1}, …, a_{k−1}) ⊑ R_{l}(c_{2}, b_{0}, b_{1}, …, b_{l−1}) ∈ C_{1}(c_{1}).

(ix) a ⊑ a ∈ N implies succ(a) ⊑ succ(a) ∈ N. Moreover, if c_{1} ⊑ c_{2} ∈ N, d_{1} ⊑ d_{2} ∈ C_{1}(0) and e_{1}(x_{1}, y_{1}) ⊑ e_{2}(x_{2}, y_{2}) ∈ C_{1}(succ(x_{1})) [x_{1}, x_{2} ∈ N, y_{1} ∈ C_{1}(x_{1}), y_{2} ∈ C_{2}(x_{2})], then R(c_{1}, d_{1}, e_{1}(x_{1}, y_{1})) ⊑ R(c_{2}, d_{2}, e_{2}(x_{2}, y_{2})) ∈ C_{1}(c_{1}).

Proposition 3.3 For each structures 𝕋 = ⟨T , ⊑⟩ and 𝔼 = ⟨E, ⊑⟩, the evolution relation ⊑ is a partial order.

Next we will define both supremum and infimum operations between every MTT-types w.r.t. the above evolution relation under the assumption that every type constructors are continuous.

Definition 3.4 For any types A and B in T , the supremum Sup(A, B) and infimum Inf(A, B) functions between them w.r.t. the evolution relation ⊑ is defined inductively as follows:

(i) Sup(N_{k}, N_{l}) = N_{r} and Inf(N_{k}, N_{l}) = N_{s} (k, l = 0, 1, …; k ≤ l), where r = |⋃_{m=0}^{k−1} C(m_{k}) ∪ ⋃_{m=0}^{l−1} D(m_{l})| and s = |⋃_{m=0}^{k−1} C(m_{k}) ∩ ⋃_{m=0}^{l−1} D(m_{l})|.

(ii) Sup(N, N) = N, Inf(N, N) = N, Sup(⊥, T) = T and Inf(⊥, T) = ⊥.

(iii) Sup((Πx_{1} ∈ A_{1})B_{1}(x_{1}), (Πx_{2} ∈ A_{2})B_{2}(x_{2})) = (Πx ∈ Sup(A_{1}, A_{2})) Sup(B_{1}, B_{2})(x), Inf((Πx_{1} ∈ A_{1})B_{1}(x_{1}), (Πx_{2} ∈ A_{2})B_{2}(x_{2})) = (Πx ∈ Inf(A_{1}, A_{2})) Inf(B_{1}, B_{2})(x).

(iv) Sup((Σx_{1} ∈ A_{1})B_{1}(x_{1}), (Σx_{2} ∈ A_{2})B_{2}(x_{2})) = (Σx ∈ Sup(A_{1}, A_{2})) Sup(B_{1}, B_{2})(x), Inf((Σx_{1} ∈ A_{1})B_{1}(x_{1}), (Σx_{2} ∈ A_{2})B_{2}(x_{2})) = (Σx ∈ Inf(A_{1}, A_{2})) Inf(B_{1}, B_{2})(x).

(v) Sup(A_{1} + B_{1}, A_{2} + B_{2}) = Sup(A_{1}, A_{2}) + Sup(B_{1}, B_{2}), Inf(A_{1} + B_{1}, A_{2} + B_{2}) = Inf(A_{1}, A_{2}) + Inf(B_{1}, B_{2}).

(vi) Sup(I(A_{1}, a_{1}, b_{1}), I(A_{2}, a_{2}, b_{2})) = I(Sup(A_{1}, A_{2}), Sup(a_{1}, a_{2}), Sup(b_{1}, b_{2})), Inf(I(A_{1}, a_{1}, b_{1}), I(A_{2}, a_{2}, b_{2})) = I(Inf(A_{1}, A_{2}), Inf(a_{1}, a_{2}), Inf(b_{1}, b_{2})).

(vii) For any types A and B which are not matched any cases of the above (i)–(vi), Sup(A, B) = T and Inf(A, B) = ⊥.

Moreover, we can also define both supremum and infimum functions between every MTT-expressions w.r.t. the evolution relation by the similar manner.

Lemma 3.5 (i) For any types A and B in T , Sup(A, B) and Inf(A, B) are the l.u.b. and g.l.b. of A and B w.r.t. the evolution relation ⊑, respectively.

(ii) Similarly, for any expressions a and b in E, Sup(a, b) and Inf(a, b) are the l.u.b. and g.l.b. of a and b w.r.t. the evolution relation ⊑, respectively.

(iii) Both structures 𝕋 = ⟨T , ⊑⟩ and 𝔼 = ⟨E, ⊑⟩ are the complete lattices w.r.t. the evolution relation ⊑.

Theorem 3.6 (i) For any expressions a ∈ A and b ∈ B, it holds that Sup(a, b) ∈ Sup(A, B).

(ii) For any expressions a ∈ A and b ∈ B, it holds that Inf(a, b) ∈ Inf(A, B).

For any types A and B in T such that A ⊑ B, we will say that Diff(B, A) is a difference between B and A if this operation satisfies the following conditions:

(1) Sup(A, Diff(B, A)) = B,

(2) Inf(A, Diff(B, A)) = ⊥.

Definition 3.7 For any types A and B in T , the difference Diff(B, A) function between B and A w.r.t. the evolution relation ⊑ is defined inductively as follows:

(i) Diff(N_{l}, N_{k}) = N_{v} (k, l = 0, 1, …; k ≤ l), where v = |⋃_{m=0}^{l−1} D(m_{l}) \ ⋃_{m=0}^{k−1} C(m_{k})|.

(ii) Diff(N, N) = ⊥ and Diff(T, ⊥) = T.

(iii) If (Πx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Πx_{2} ∈ A_{2})B_{2}(x_{2}), then

Diff((Πx_{2} ∈ A_{2})B_{2}(x_{2}), (Πx_{1} ∈ A_{1})B_{1}(x_{1}))

= (Πx ∈ Diff(A_{2}, A_{1}))B_{1}(x) ∪ (Πx_{1} ∈ A_{1}) Diff(B_{2}, B_{1})(x_{1}) ∪

(Πx ∈ Diff(A_{2}, A_{1})) Diff(B_{2}, B_{1})(x).

(iv) If (Σx_{1} ∈ A_{1})B_{1}(x_{1}) ⊑ (Σx_{2} ∈ A_{2})B_{2}(x_{2}), then

Diff((Σx_{2} ∈ A_{2})B_{2}(x_{2}), (Σx_{1} ∈ A_{1})B_{1}(x_{1}))

= (Σx ∈ Diff(A_{2}, A_{1}))B_{1}(x) ∪ (Σx_{1} ∈ A_{1}) Diff(B_{2}, B_{1})(x_{1}) ∪

(Σx ∈ Diff(A_{2}, A_{1})) Diff(B_{2}, B_{1})(x).

(v) If A_{1} + B_{1} ⊑ A_{2} + B_{2}, then

Diff(A_{2} + B_{2}, A_{1} + B_{1})

= Diff(A_{2}, A_{1}) + Diff(B_{2}, B_{1}).

(vi) If I(A_{1}, a_{1}, b_{1}) ⊑ I(A_{2}, a_{2}, b_{2}), then

Diff(I(A_{2}, a_{2}, b_{2}), I(A_{1}, a_{1}, b_{1})

= I(Diff(A_{2}, A_{1}), a_{1}, b_{1}) ∪ I(A_{2}, Diff(a_{2}, a_{1}), Diff(b_{2}, b_{1})) ∪

I(Diff(A_{2}, A_{1}), Diff(a_{2}, a_{1}), Diff(b_{2}, b_{1})).

(vii) For any types A and B which are not matched any cases of the above (i)–(vi),

Diff(A, B) = ⊥.

By the similar manner, we can introduce the difference between expressions Diff(b, a) for any expressions a and b in E such that a ⊑ b.

Lemma 3.8 (i) For any types A and B in T such that A ⊑ B, Diff(B, A) is a difference between B and A.

(ii) Similary, for any expressions a ∈ A and b ∈ B in E such that a ⊑ b ∈ A, Diff(b, a) is a difference between b and a.

Theorem 3.9 For any expressions a ∈ A and b ∈ B, if an expression a is evolved to b in a type A, a ⊑ b ∈ A, then it holds that Diff(b, a) ∈ Diff(B, A).

References

[1] L. Boerio, Extending Pruning Techniques to Polymorphic Second Order λ-Calculus, Proceeding of ESOP ’94, Edinburgh, April 1994, LNCS 788, D. Sannella (ed.), Springer-Verlag, pp.120–134.

[2] T. Katayama, A Theoretical Framework of Software Evolution, International Workshop on Principles of Software Evolution, In Conjunction with International Conference on Software Engineering 1998 (ICSE98), pp.1–5.

[3] P. Martin-Löf, Constructive Mathematics and Computer Programming, In Logic, Methodolgy and Philosophy of Science, VI, NorthHolland,1980.

[4] P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis,1984.