Last active
March 12, 2018 08:00
-
-
Save noblepayne/b9758877dbe52ac741d0272412bdf764 to your computer and use it in GitHub Desktop.
peano naturals
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (ns peano.nat | |
| "A simple construction of the natural numbers." | |
| (:refer-clojure :exclude [zero?])) | |
| ;; A natural number. All natural numbers have a predecessor (except zero). | |
| (defrecord Nat [pred]) | |
| (defn succ | |
| "Given a natural number, return its successor." | |
| [n] | |
| (Nat. n)) | |
| ;; Define zero as the natural number with no (nil) predecessor | |
| (def Zero (succ nil)) | |
| (println "Zero:" Zero) | |
| ;; => Zero: #peano.nat.Nat{:pred nil} | |
| (defn zero? | |
| "Returns true if n is Zero, otherwise false." | |
| [n] | |
| (= Zero n)) | |
| (defn plus | |
| "Add two natural numbers." | |
| [n m] | |
| (cond | |
| (zero? n) m ;; 0 + m = m | |
| (zero? m) n ;; n + 0 = n | |
| :else | |
| (recur (succ n) (:pred m)))) ;; n + m = (n + 1) + (m - 1) | |
| (defn minus | |
| "Subtract two natural numbers. | |
| Returns Zero if n1 < n2." | |
| [n m] | |
| (cond | |
| (zero? n) Zero ;; 0 - m = 0 (restrict to ℕ) | |
| (zero? m) n ;; n - 0 = n | |
| :else | |
| (recur (:pred n) (:pred m)))) ;; n - m = (n - 1) - (m - 1) | |
| (def One (succ Zero)) | |
| (println "One:" One) | |
| ;; => One: #peano.nat.Nat{:pred #peano.nat.Nat{:pred nil}} | |
| (def Two (succ One)) | |
| (println "Two:" Two) | |
| ;; => Two: #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred nil}}} | |
| (def one-plus-one (plus One One)) | |
| (println "One + One:" one-plus-one) | |
| ;; => One + One: #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred nil}}} | |
| (println "Does Two equal One + One?" | |
| (= Two (plus One One))) | |
| ;; => Does Two equal One + One? true | |
| (defn naturals | |
| "Lazy infinite sequence of all natural numbers." | |
| [] | |
| (iterate succ Zero)) | |
| ;; take the first 5 | |
| (take 5 (naturals)) | |
| ;; => (#peano.nat.Nat{:pred nil} | |
| ;; => #peano.nat.Nat{:pred #peano.nat.Nat{:pred nil}} | |
| ;; => #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred nil}}} | |
| ;; => #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred nil}}}} | |
| ;; => #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred #peano.nat.Nat{:pred nil}}}}}) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment