Functional Programming Over Sets with Atoms
summary
A Haskell library called n Lambda implements definable (orbit‑finite) sets with atoms by representing values as first‑order formulas and bound/free‑variable lists and outsourcing satisfiability checks to Z3. Code for transitive closure and automata‑learning is copy‑and‑paste identical to finite versions and runs symbolically; operations like emptiness and membership call the SMT solver. Enumeration and fold over infinite definable sets are impossible; orbit decomposition makes some hard problems (e.g. 3‑colorability) decidable.
AI-written summary · about
chapters (8)
- 0:00Intro
- 2:23Programming with finite sets
- 5:05Example: transitive closure
- 7:05Other examples
- 8:10Sets with atoms
- 11:30NLambda: a Haskell library
- 16:34Semantics
- 24:003-colorability
related talks
15mLogic Programming with Extensible Types (Lightning talk)
30mMore Fixpoints!
01h 00mTheory and Models of Lambda Calculus Untyped and Typed - Part 2 of 5
36mAbstract Machines for Good
27mHaskell equations, thirty-eight years later
51mGreek Classics: Lambda Calculus For Beginners
49mFunctional Programming Essentials
53mIntroduction to Intuitionistic Type Theory