]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/lambda-delta/syntax/weight.ma
confluence of parallel substitution (tps) started ...
[helm.git] / matita / matita / lib / lambda-delta / syntax / weight.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic
3     ||A||  Library of Mathematics, developed at the Computer Science
4     ||T||  Department of the University of Bologna, Italy.
5     ||I||
6     ||T||
7     ||A||  This file is distributed under the terms of the
8     \   /  GNU General Public License Version 2
9      \ /
10       V_______________________________________________________________ *)
11
12 include "lambda-delta/syntax/lenv.ma".
13
14 (* WEIGHTS ******************************************************************)
15
16 (* the weight of a term *)
17 let rec tw T ≝ match T with
18 [ TSort _     ⇒ 1
19 | TLRef _     ⇒ 1
20 | TPair _ V T ⇒ tw V + tw T + 1
21 ].
22
23 interpretation "weight (term)" 'Weight T = (tw T).
24
25 (* the weight of a local environment *)
26 let rec lw L ≝ match L with
27 [ LSort       ⇒ 0
28 | LPair L _ V ⇒ lw L + #V
29 ].
30
31 interpretation "weight (local environment)" 'Weight L = (lw L).
32
33 (* the weight of a closure *)
34 definition cw: lenv → term → ? ≝ λL,T. #L + #T.
35
36 interpretation "weight (closure)" 'Weight L T = (cw L T).
37
38 axiom tw_wf_ind: ∀P:term→Prop.
39                  (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
40                  ∀T. P T.
41
42 axiom cw_wf_ind: ∀P:lenv→term→Prop.
43                  (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
44                  ∀L,T. P L T.