CostAlgebra

Pure cost extraction plus an original isolated payment teaching model.

Package payment, input revision 3. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

x · operator

payment · input revision 3 · CC0 1.0

x == CHOOSE y \in S : TRUE

Exact module download · Source bundle and reproduction instructions

Add · operator

payment · input revision 3 · CC0 1.0

Add(S) == IF S = {} THEN 0
                  ELSE LET x == CHOOSE y \in S : TRUE
                       IN f[x] + Add(S \ {x})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: x, Add

MaxOf · operator

payment · input revision 3 · CC0 1.0

MaxOf(a, b) == IF a >= b THEN a ELSE b

Exact module download · Source bundle and reproduction instructions

ModifiedCost · operator

payment · input revision 3 · CC0 1.0

ModifiedCost(base, increases, reductions) ==
    MaxOf(0, base + SeqSum(increases) - SeqSum(reductions))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, SeqSum

SeqSum · operator

payment · input revision 3 · CC0 1.0

SeqSum(s) == SumMap([i \in 1..Len(s) |-> s[i]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SumMap

SumMap · operator

payment · input revision 3 · CC0 1.0

SumMap(f) ==
    LET RECURSIVE Add(_)
        Add(S) == IF S = {} THEN 0
                  ELSE LET x == CHOOSE y \in S : TRUE
                       IN f[x] + Add(S \ {x})
    IN Add(DOMAIN f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Add