Published
Edited
Jan 10, 2020
Insert cell
Insert cell
SUCC_MAGNITUDE =
qtyFn =>
transform =>
start_value =>
transform(qtyFn(transform)(start_value))

Insert cell
SUCC_MAGNITUDE_PAIR =
pair =>
lib.PAIR(pair(lib.FALSE))(SUCC_MAGNITUDE(pair(lib.FALSE)))
Insert cell
PRED_MAGNITUDE =
qtyFn =>
qtyFn(SUCC_MAGNITUDE_PAIR)(lib.PAIR(lib.ZERO_MAGNITUDE)(lib.ZERO_MAGNITUDE))(lib.TRUE)
Insert cell
Insert cell
magnitude = qtyFn => qtyFn(lib.incr)(0)
Insert cell
NUMBER = isPositive => qtyFn => lib.PAIR(isPositive)(qtyFn)
Insert cell
IS_POS = number => lib.HEAD(number)
Insert cell
// SIGN is a synonym for IS_POS
SIGN = IS_POS
Insert cell
// Return the absoulte value of a signed integer. This function could also be called MAGNITUDE
ABS = number => lib.TAIL(number)
Insert cell
ZERO_MAGNITUDE = transform => start_value => start_value
Insert cell
UNIT_MAGNITUDE = transform => start_value => transform(start_value)
Insert cell
HAS_ZERO_MAGNITUDE = number => ABS(number)(dont_care => lib.FALSE)(lib.TRUE)
Insert cell
HAS_UNIT_MAGNITUDE = number => magnitude(ABS(number)) === 1 ? lib.TRUE : lib.FALSE
Insert cell
IS_ZERO = number => HAS_ZERO_MAGNITUDE(number)
Insert cell
IS_MINUS_ONE = number => lib.AND(lib.NOT(IS_POS(number)))
(HAS_UNIT_MAGNITUDE(number))
Insert cell
ZERO = NUMBER(lib.TRUE)(ZERO_MAGNITUDE)
Insert cell
Insert cell
SUCC =
number =>
// Is the number positive?
IS_POS(number)
// Yup, so it must be >= 0, therefore return the positive
// number created by calling SUCC_MAGNITUDE on the number's
// absolute value
(NUMBER(lib.TRUE)(SUCC_MAGNITUDE(ABS(number))))

// Nope, so check for the special case of minus one
(IS_MINUS_ONE(number)
// Yup, so return value of ZERO
(ZERO)

// Nope, so the number must be <= -2
// Therefore, return the negative number
// created by calling PRED_MAGNITUDE on the
// number's absolute value
(NUMBER(lib.FALSE)(PRED_MAGNITUDE(ABS(number)))))
Insert cell
Insert cell
PRED =
number =>
// Check for the special case of zero
(IS_ZERO(number)
// Yup, so return MINUS_ONE
(NUMBER(lib.FALSE)(UNIT_MAGNITUDE))

// Is the number positive?
(IS_POS(number)
// Yup, so the number must be >= 1
// Return the positive number created by calling
// PRED_MAGNITUDE on the number's absolute value
(NUMBER(lib.TRUE)(PRED_MAGNITUDE(ABS(number))))

// Nope, so the number must be <= -1
// Therefore, return the negative number
// created by calling SUCC_MAGNITUDE on the
// number's absolute value
(NUMBER(lib.FALSE)(SUCC_MAGNITUDE(ABS(number))))))
Insert cell
Insert cell
PLUS_ONE = SUCC(ZERO)
Insert cell
PLUS_TWO = SUCC(PLUS_ONE)
Insert cell
MINUS_ONE = PRED(ZERO)
Insert cell
MINUS_TWO = PRED(MINUS_ONE)
Insert cell
MINUS_THREE = PRED(MINUS_TWO)
Insert cell
Insert cell
to_integer =
number =>
// Inner function
(sign => mag => sign ? mag : mag * -1)
// Extract the sign and absolute value from the NUMBER, then
// reify these values and pass them to the inner function as the
// sign and mag parameters
(lib.to_boolean(lib.SIGN(number)))
(lib.magnitude(lib.ABS(number)))
Insert cell
Insert cell
{
// Check simple reification
return {
"TWO_to_integer" : to_integer(PLUS_TWO)
, "MINUS_THREE_to_integer" : to_integer(MINUS_THREE)
// Check SUCCessor passes up through ZERO without exploding
, "SUCC_MINUS_ONE" : to_integer(SUCC(MINUS_ONE))
, "2nd_SUCC_MINUS_ONE" : to_integer(SUCC(SUCC(MINUS_ONE)))
, "3rd_SUCC_MINUS_TWO" : to_integer(SUCC(SUCC(SUCC(MINUS_TWO))))
// Check PREDecessor passes down through ZERO without exploding
, "PRED_ONE" : to_integer(PRED(PLUS_ONE))
, "2nd_PRED_ONE" : to_integer(PRED(PRED(PLUS_ONE)))
, "3rd_PRED_TWO" : to_integer(PRED(PRED(PRED(PLUS_TWO))))
}
}
Insert cell
Insert cell
Insert cell

Purpose-built for displays of data

Observable is your go-to platform for exploring data and creating expressive data visualizations. Use reactive JavaScript notebooks for prototyping and a collaborative canvas for visual data exploration and dashboard creation.
Learn more