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. x
y;1) i:{a..b
}. e(i)
i:
b. e(i)
![]()
Iter( x,y. x
y;1) i:{0..b
}. e(i)
e b
![]()
Iter( x,y. x
y;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:(A
A
A), 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:(A
A
A), 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
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |