Skip to content
Liquid Haskell implementation of ordinal arithmetic
Haskell
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.gitignore
Haskell.sublime-build
NewProofCombinators.hs
README.md
ordinals.hs
ordinals_LH.hs

README.md

Ordinal Arithmetic

A (somewhat) verified Liquid Haskell implementation of ordinal arithmetic.

Files

  • Ordinals.hs : Plain Haskell implementation
  • Ordinals_LH.hs : Liquid Haskell implementation
  • Haskell.sublime-build : Build file for LH with Sublime
  • NewProofCombinators.hs : File copied from LH repo because of dependency issues

Liquid Haskell

Functions expect the ordinal arguments to be in Cantor Normal Form. However, this can't be enforced with plain Haskell, so Liquid Haskell is required.

LH is used to prove:

  • the closure of Normal-Form Ordinals under
    • addition
    • subtraction
    • multiplication
  • termination of all functions
  • totality of all functions

To type-check refinements and proofs:

  1. Install LH
  2. Run liquid ordinals_LH.hs

Note that ordinals_LH.hs can be run as a normal Haskell file.

TODO

  • "reverse" Ordinals so units are constant-time accessible
  • prove closure under exponentiation
  • decouple LH from main haskell (if possible)
  • silence these warnings (if possible)
You can’t perform that action at this time.