IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops
Nuprl Section: IteratedBinops - Iterated Binary Operations

Iteration of binary operations

This section treats the iteration of binary operations over values indexed indexed by finite integer subranges. We parameterize iteration by the binary operation and a value, typically its identity element, for the empty range. Here are some familiar special cases.

 i:{a..b}. e(i) Iter(x,y. x+y;0) i:{a..b}. e(i) i:b. e(i) Iter(x,y. x+y;0) i:{0..b}. e(i) i:{a..b}. e(i) Iter(x,y. xy;1) i:{a..b}. e(i) i:b. e(i) Iter(x,y. xy;1) i:{0..b}. e(i) eb Iter(x,y. xy;1) :{0..b}. e Or i:{a..b}. e(i) Iter(x,y. x  y;False) i:{a..b}. e(i) Or i:b. e(i) Iter(x,y. x  y;False) i:{0..b}. e(i) And i:{a..b}. e(i) Iter(x,y. x & y;True) i:{a..b}. e(i) And i:b. e(i) Iter(x,y. x & y;True) i:{0..b}. e(i)

where

Def  Iter(f;ui:{a..b}. e(i)
Def  == if a<b f((Iter(f;ui:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)

Thm*  f:(AAA), u:Aa,b:e:({a..b}A). (Iter(f;ui:{a..b}. e(i))  A

Observe that iteration is defined directly only when the index set is an integer subrange

Def  {i..j} == {k:i  k < j }

and so indexing by over some other finite class requires explicitly providing a one-one map from an integer subrange onto that index class. Note that for the above typing of the iteration operator to hold, one must supply a value for the empty range.

A fundamental device for working with iterations index by ranges is shifting the range:

Thm*  f:(AAA), u:Aa,b:e:({a..b}A), k:.
Thm*  (Iter(f;ui:{a..b}. e(i)) = (Iter(f;uj:{a+k..b+k}. e(j-k))

which one might paraphrase by saying that the indices serve as nothing more than specifying the sequence of values to be iterated over.

Continued at iter via intseg remark INTRO cont

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html