%% Defines f(j,f(...f(i+1,f(i,a))...))
for_def(i,j:int,a:T,f:[[int,T]->T]) : RECURSIVE T = IF i > j THEN a ELSE f(j,for_def(i,j-1,a,f)) ENDIF MEASURE max(j-i+1,0)
ForBody(upfrom,upto:int) : TYPE = [[subrange(upfrom,upto),T]->T]
ext2int(upfrom,upto:int,f:ForBody(upfrom,upto))(i:int,a:T) : T = IF upfrom <= i AND i <= upto THEN f(i,a) ELSE a ENDIF
for_it(upfrom:int,i:upfrom(upfrom),upto:int,a:T,f:ForBody(upfrom,upto)) : RECURSIVE
{t : T | t = for_def(i,upto,a,ext2int(upfrom,upto,f))} = IF i > upto THEN a ELSE for_it(upfrom,i+1,upto,f(i,a),f) ENDIF MEASURE max(upto-i+1,0)
%% local a : T := init; %% local i : int; %% for (i := m; i <= n; i++) { %% a := f(i,a); %% } %% return a;
for(m,n:int,init:T,f:ForBody(m,n)) : T =
for_it(m,m,n,init,f)
for_induction : THEOREM FORALL(m:int,(n:int| n >= m-1),init:T,f:ForBody(m,n),inv:PRED[[upto(n-m+1),T]]):
(inv(0,init) AND FORALL (k:subrange(0,n-m),ak:T) : inv(k,ak) IMPLIES inv(k+1,f(m+k,ak))) IMPLIES
inv(n-m+1,for(m,n,init,f))
%% Defines f(j,f(...f(i-1,f(i,a))...))
for_down_def(i,j:int,a:T,f:[[int,T]->T]) : RECURSIVE T = IF i < j THEN a ELSE f(j,for_down_def(i,j+1,a,f)) ENDIF MEASURE max(i-j+1,0)
%% local a : T := init; %% local i : int; %% for (i := n; i >= m; i--) { %% a := f(i,a); %% }
for_down(n,m:int,init:T,f:ForBody(m,n)) : T =
for(m,n,init,LAMBDA(k:subrange(m,n),a:T): f(n+m-k,a))
for_down_induction : THEOREM FORALL(n:int,(m:int| m <= n+1),init:T,f:ForBody(m,n),inv:PRED[[upto(n-m+1),T]]):
(inv(0,init) AND FORALL (k:subrange(0,n-m),ak:T) : inv(k,ak) IMPLIES inv(k+1,f(n-k,ak))) IMPLIES
inv(n-m+1,for_down(n,m,init,f))
%% Defines (... ((f(i) o f(i+1)) o f(i+2)) o .... f(j))
iterate_left_def(i:int,j:upfrom(i),f:[int->T],o:[[T,T]->T]) : RECURSIVE T = IF i = j THEN f(i) ELSE iterate_left_def(i,j-1,f,o) o f(j) ENDIF MEASURE j-i
IterateBody(upfrom,upto:int) : TYPE = [subrange(upfrom,upto)->T]
ext2int(upfrom,upto:int,a:T,f:IterateBody(upfrom,upto))(i:int) : T = IF upfrom <= i AND i <= upto THEN f(i) ELSE a ENDIF
iterate_left_id(i:int,j:int,f:IterateBody(i,j),o:[[T,T]->T],id:T) : MACRO T =
for(i,j,id,LAMBDA(k:subrange(i,j),t:T):t o f(k))
%% local a : T = f(m); %% local i : int; %% for (i := m+1; i <= n; i++) { %% a := a o f(i) %% } %% return a;
iterate_left(m:int,n:upfrom(m),f:IterateBody(m,n),o:[[T,T]->T]) : T =
iterate_left_id(m+1,n,LAMBDA(k:subrange(m+1,n)):f(k),o,f(m))
iterate_left_induction : THEOREM FORALL(m:int,n:upfrom(m),f:IterateBody(m,n),o:[[T,T]->T],inv:PRED[[upto(n-m),T]]):
(inv(0,f(m)) AND FORALL (k:below(n-m),ak:T) : inv(k,ak) IMPLIES inv(k+1,ak o f(m+k+1))) IMPLIES
inv(n-m,iterate_left(m,n,f,o))
%% Defines f(i) o (... (f(j-2) o (f(j-1) o f(j))) ...)
iterate_right_def(i:int,j:upfrom(i),f:[int->T],o:[[T,T]->T]) : RECURSIVE T = IF i = j THEN f(j) ELSE f(i) o iterate_right_def(i+1,j,f,o) ENDIF MEASURE j-i
iterate_right_id(i,j:int,f:IterateBody(i,j),o:[[T,T]->T],id:T) : MACRO T =
for_down(j,i,id,LAMBDA(k:subrange(i,j),t:T):f(k) o t)
%% local a : T = f(n); %% local i : int; %% for (i := n-1; i >= m; i--) { %% a := f(i) o a %% } %% return a;
iterate_right(m:int,n:upfrom(m),f:IterateBody(m,n),o:[[T,T]->T]) : T =
iterate_right_id(m,n-1,LAMBDA(k:subrange(m,n-1)):f(k),o,f(n))
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
