Iteration of binary operations

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;u) i:{a..b}. e(i)
Def  == if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)

Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). (Iter(f;u) i:{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:A, a,b:, e:({a..b}A), k:.
Thm*  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{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 /sfa/Nuprl/Shared/Xindentation_hack_doc.html