SeqReduce

Reductions of sequences, both left and right.

Signature of SeqReduce

List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Seq

SIGNATURE SeqReduce [from,to]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

-- reductions of sequences

Parameter

SORT from to

Improts

IMPORT Seq[from] ONLY seq

Reduction functions

(o, e) / s: reduce s, bracketing on the right. Informally: (o / e)(<a, b,..., y, z>) == a o (b o (...(y o (z o e))...)).

FUN / : (from ** to -> to) ** to ** seq[from] -> to             

(o, e) \ s: reduce s, bracketing on the left. Informally: (o \ e)(<a, b,..., y, z>) == z o (y o ... o (b o (a o e))). This function is tail-recursive.

FUN \ : (from ** to -> to) ** to ** seq[from] -> to             

Long name (reduce is equal to /) with and without currying.

FUN reduce : (from ** to -> to) ** to ** seq[from] -> to
FUN reduce : (from ** to -> to) ** to -> seq[from] -> to

The function / is equal to foldr of Bird, Wadler: Introduction to Functional Programming. The function foldl can be expressed by \ as follows: (\\a,b. b o a, e) \ s == foldl(o)(e)(s).

Old fashioned style

FUN / \ : (from ** to -> to) ** to -> seq[from] -> to           
        --  (o / e)(s)== (o, e) / s

next node: SeqSort,
prev node: SeqMapEnv,
up to node: Subsystem Sequences Proper