Documentation

Primitive operations can be more powerful. This is similar to Boolean example.

>>> runLoud $ spec_ SysFStar >> naturalsPrimScript
-- 1. Constants
---------------
--
λ» :define succ : ℕ → ℕ = λ n → S n
λ» :define zero = 0
λ» :define one = succ zero
λ» :define two = succ one
λ» :define three = succ two
--
λ» :example zero
↪ 0 : ℕ
--
λ» :example one
↪ 1 : ℕ
--
λ» :example two
↪ 2 : ℕ
--
λ» :example three
↪ 3 : ℕ
--
-- 2. Using elimination
-----------------------
--
λ» :define nat-fold
: ∀ r → ℕ → (r → r) → r → r
= λ r n s z → ℕ-elim (λ _ → r) z (λ l → s) n
λ» :define plus : ℕ → ℕ → ℕ = λ x y → nat-fold ℕ x succ y
--
λ» :example plus
↪ λ x y → ℕ-elim (λ _ → ℕ) y (λ l n → S n) x : ℕ → ℕ → ℕ
--
λ» :example plus two three
↪ 5 : ℕ
--
λ» :example plus two zero
↪ 2 : ℕ
--
λ» :example plus zero three
↪ 3 : ℕ
--
-- 2.1. Partial evaluation
--
-- Because we scrutinise the first argument, following expressions reduce (well):
λ» :example λ n → plus two n : ℕ → ℕ
↪ λ n → S (S n) : ℕ → ℕ
--
λ» :example λ n → plus zero n : ℕ → ℕ
↪ λ n → n : ℕ → ℕ
--
-- ... but these doesn't:
λ» :example λ n → plus n two : ℕ → ℕ
↪ λ n → ℕ-elim (λ _ → ℕ) 2 (λ l n₁ → S n₁) n : ℕ → ℕ
--
λ» :example λ n → plus n three : ℕ → ℕ
↪ λ n → ℕ-elim (λ _ → ℕ) 3 (λ l n₁ → S n₁) n : ℕ → ℕ
--
-- 3. Built-in primitive
------------------------
--
λ» :define plus# : ℕ → ℕ → ℕ = λ x y → ℕ-plus x y
--
λ» :example plus#
↪ λ x y → ℕ-plus x y : ℕ → ℕ → ℕ
--
λ» :example plus# two two
↪ 4 : ℕ
--
λ» :example plus# two zero
↪ 2 : ℕ
--
λ» :example plus# zero two
↪ 2 : ℕ
--
λ» :example plus# zero zero
↪ 0 : ℕ
--
-- 3.1. Partial evaluation
--
-- With primitive plus we get more aggressive reduction behaviour
λ» :example λ n → plus# two n : ℕ → ℕ
↪ λ n → S (S n) : ℕ → ℕ
--
λ» :example λ n → plus# zero n : ℕ → ℕ
↪ λ n → n : ℕ → ℕ
--
λ» :example λ n → plus# n two : ℕ → ℕ
↪ λ n → S (S n) : ℕ → ℕ
--
λ» :example λ n → plus# n zero : ℕ → ℕ
↪ λ n → n : ℕ → ℕ
--
-- In fact, literals are extracted "to front":
λ» :example λ n m p → plus# (plus# (plus# n one) zero)
                            (plus# (plus# m two) p)
                : ℕ → ℕ → ℕ → ℕ
↪ λ n m p → S (S (S (ℕ-plus n (ℕ-plus m p))))
: ℕ → ℕ → ℕ → ℕ
--
-- 4. With multiplication
-------------------------
--
-- 4.1. Using elimination
--
λ» :define times
: ℕ → ℕ → ℕ = λ x y → nat-fold ℕ x (plus y) zero
--
λ» :example times two three
↪ 6 : ℕ
--
-- Because we scrutinise the first argument, following expressions reduce (too well?):
λ» :example λ n → times two n : ℕ → ℕ
↪ λ n → ℕ-elim (λ _ → ℕ)
               (ℕ-elim (λ _ → ℕ) 0 (λ l n₁ → S n₁) n)
               (λ l n₁ → S n₁)
               n
: ℕ → ℕ
--
λ» :example λ n → times zero n : ℕ → ℕ
↪ λ n → 0 : ℕ → ℕ
--
-- ... but these doesn't:
λ» :example λ n → times n two : ℕ → ℕ
↪ λ n → ℕ-elim (λ _ → ℕ) 0 (λ l y → S (S y)) n : ℕ → ℕ
--
λ» :example λ n → times n three : ℕ → ℕ
↪ λ n → ℕ-elim (λ _ → ℕ) 0 (λ l y → S (S (S y))) n : ℕ → ℕ
--
-- 4.2. Built-in primitive
--
λ» :define times# : ℕ → ℕ → ℕ = λ x y → ℕ-times x y
--
λ» :example times# two three
↪ 6 : ℕ
--
-- With primitive times we get more aggressive reduction behaviour
λ» :example λ n → times# three n : ℕ → ℕ
↪ λ n → ℕ-plus n (ℕ-plus n n) : ℕ → ℕ
--
λ» :example λ n → times# zero n : ℕ → ℕ
↪ λ n → 0 : ℕ → ℕ
--
λ» :example λ n → times# n three : ℕ → ℕ
↪ λ n → ℕ-plus n (ℕ-plus n n) : ℕ → ℕ
--
λ» :example λ n → times# n zero : ℕ → ℕ
↪ λ n → 0 : ℕ → ℕ
--
-- A bit more envolved example:
λ» :example λ n → times# (plus# n two) two : ℕ → ℕ
↪ λ n → S (S (S (S (ℕ-plus n n)))) : ℕ → ℕ
--
-- Lastly: a complex expression with plus# and times#:
-- (1 + n) * 1 + 0 + (1 +  m * 2 + m * p)
-- Note how the expression is unrolled as much as possible:
λ» :example λ n m p →
                plus# (plus# (times# (plus# one n) one)
                             zero)
                      (plus# (plus# one (times# m two))
                             (times# m p))
                : ℕ → ℕ → ℕ → ℕ
↪ λ n m p → S (S (ℕ-plus n (ℕ-plus (ℕ-plus m m)
                                   (ℕ-times m p))))
: ℕ → ℕ → ℕ → ℕ
∎