source: etc/campbell/dev-notes/2011-07-28-envs.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 2.2 KB
Line 
1Showing environment lookups succeed: predicate-style vs free-variables style
2
3I've been working on showing that lookups of environments in Cminor programmes
4always succeed and I'm looking at two ways to maintain such invariants with Σ
5types (see my mail to the cerco list for earlier stuff).
6
7The styles
8----------
9
10The higher order predicate style applies a predicate to every variable in the
11body 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
27The free variables style defines the usual free variables function and asserts
28the 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
42Note 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
46and then use the same definition for internal_function.
47
48Proofs
49------
50
51In both styles pattern matching on the statement/expression refines the type
52of the invariant.  In the h.o.predicate style we can then access the property
53desired by the appropriate projection of the conjunction.  For the f.v. style
54we need to perform additional reasoning about sets.  Moreover, the coarse
55choices for reduction currently available in Matita make it difficult to
56prevent the underlying definitions in the f.v. style being reduced.
57
58Given these difficulties, I intend to stick with the higher-order predicate
59style.  (One advantage of the approach is that at some points - such as the
60functions which add initialisation code - we can just reason about the free
61variable sets rather than carry around some extra predicate that we don't care
62about.)
Note: See TracBrowser for help on using the repository browser.