1 | Showing environment lookups succeed: predicate-style vs free-variables style |
---|
2 | |
---|
3 | I've been working on showing that lookups of environments in Cminor programmes |
---|
4 | always succeed and I'm looking at two ways to maintain such invariants with Σ |
---|
5 | types (see my mail to the cerco list for earlier stuff). |
---|
6 | |
---|
7 | The styles |
---|
8 | ---------- |
---|
9 | |
---|
10 | The higher order predicate style applies a predicate to every variable in the |
---|
11 | body of each function: |
---|
12 | |
---|
13 | (* Assert a predicate on every variable or parameter identifier. *) |
---|
14 | let rec stmt_vars (s:stmt) (P:ident → Prop) on s : Prop ≝ |
---|
15 | match s with |
---|
16 | [ St_skip ⇒ True |
---|
17 | | St_assign _ i e ⇒ P i ∧ expr_vars ? e P |
---|
18 | |
---|
19 | ... |
---|
20 | |
---|
21 | record internal_function : Type[0] ≝ |
---|
22 | ... |
---|
23 | ; f_body : stmt |
---|
24 | ; f_bound : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) |
---|
25 | }. |
---|
26 | |
---|
27 | The free variables style defines the usual free variables function and asserts |
---|
28 | the predicate holds for every variable in the set: |
---|
29 | |
---|
30 | let rec fv_stmt (s:stmt) : identifier_set SymbolTag ≝ |
---|
31 | match s with |
---|
32 | [ St_skip ⇒ ∅ |
---|
33 | | St_assign _ i e ⇒ {(i)} ∪ fv_expr ? e |
---|
34 | ... |
---|
35 | |
---|
36 | record internal_function : Type[0] ≝ |
---|
37 | ... |
---|
38 | ; f_body : stmt |
---|
39 | ; f_bound : ∀id.id ∈ fv_stmt f_body → Exists ? (λx.\fst x = id) (f_params @ f_vars) |
---|
40 | }. |
---|
41 | |
---|
42 | Note that we can define stmt_vars in terms of fv_stmt, |
---|
43 | |
---|
44 | definition stmt_vars : stmt → (ident → Prop) → Prop ≝ λs,P. ∀i.i∈fv_stmt s → P i. |
---|
45 | |
---|
46 | and then use the same definition for internal_function. |
---|
47 | |
---|
48 | Proofs |
---|
49 | ------ |
---|
50 | |
---|
51 | In both styles pattern matching on the statement/expression refines the type |
---|
52 | of the invariant. In the h.o.predicate style we can then access the property |
---|
53 | desired by the appropriate projection of the conjunction. For the f.v. style |
---|
54 | we need to perform additional reasoning about sets. Moreover, the coarse |
---|
55 | choices for reduction currently available in Matita make it difficult to |
---|
56 | prevent the underlying definitions in the f.v. style being reduced. |
---|
57 | |
---|
58 | Given these difficulties, I intend to stick with the higher-order predicate |
---|
59 | style. (One advantage of the approach is that at some points - such as the |
---|
60 | functions which add initialisation code - we can just reason about the free |
---|
61 | variable sets rather than carry around some extra predicate that we don't care |
---|
62 | about.) |
---|