My hobby: proof engineering
November 25, 2017
I have a great time working with my teammates at Airbnb. Many of them work very hard, so much that they don’t enjoy programming for fun anymore. I still love recreational programming, but in a peculiar sense.
When I come home from work, I try to prove theorems in a proof assistant. Usually the theorems are related to functional programming or type systems.
It’s a masochistic hobby. Convincing a computer that a theorem is true can be quite difficult compared to convincing a human. But if I can get a computer to accept my proof, then a) I must have a pretty good understanding of it, and b) it really must be right!
I use the Coq theorem prover for formalizing proofs. Coq is a beautiful and simple language [1]—far simpler than the languages I use at work! Its beauty is hidden beneath a rather unsightly IDE [2]:
The proof is on the left. The green highlighted part has been verified by Coq. As I am working on a proof, I can ask Coq to step forward through it with
Ctrl+Down, and I can use Ctrl+Up to step backward. At any point if my proof is wrong, Coq will highlight the error in red. It’s similar to how a type checker works—or rather, it’s exactly the same in a very deep sense. I’d love to explain what I mean by that, but I’ll have to save that for separate article.In the screenshot, I’m currently in the middle of a proof. The upper right pane shows what I need to prove (in this case,
f x = x) and also what hypotheses I can use to prove it (shown above the horizontal line). The lower right pane shows helpful information if I request it, such as the type of something or a list of definitions/lemmas/theorems related to it.Coq is not a toy, although it can be fun like one. Many serious results have been proven using it, including the four color theorem and the correctness of a certain C compiler.
Recently I set up a small GitHub repository with a continuous integration system that checks my proofs when I push to a branch, preventing me from merging it into master if there is a mistake. It’s impossible to commit incorrect math to this repository [3]!
Proving theorems in a machine-checked language is invigorating once you get the hang of it. It feels like doing a puzzle. And when you finish a long proof of a nontrivial result, it’s a remarkable sensation unlike anything else.
Case study: domain theory
When you write down a recursive function in any language, it’s actually not obvious that such a definition is mathematically well-defined. This week I was reading about the theoretical underpinning of recursive definitions: fixed points. Whenever you define something recursively, you are technically taking a fixed point of a continuous function (yes, you read that correctly!). There is some really cool math behind this called domain theory.
Before this week, I had a vague understanding of all this. I do a fair amount of functional programming, but I hardly knew anything about domain theory. Today, I finished proving the main result: the Kleene fixed-point theorem. This was a difficult proof for me, but now I consider myself pretty well-versed in the basic ideas of domain theory.
The proof is not very remarkable on paper, but convincing a computer to accept it is another matter entirely. I started by writing down the definitions below. The first step to understanding a theory is being able to formally define the main ideas! I don’t expect the casual reader to dissect all these definitions, but I include them here to give you a sense of what it looks like to write them in Coq:
(* Assumption: Let (T, leq) be a partially ordered set, or poset. A poset is a set with a binary relation which is reflexive, transitive, and antisymmetric. *) Parameter T : Set. Parameter leq : T -> T -> Prop. Axiom refl : forall x, leq x x. Axiom trans : forall x y z, leq x y -> leq y z -> leq x z. Axiom antisym : forall x y, leq x y -> leq y x -> x = y. (* A supremum of a subset of T is a least element of T which is greater than or equal to every element in the subset. This is also called a join or least upper bound. *) Definition supremum P x1 := (forall x2, P x2 -> leq x2 x1) /\ forall x3, (forall x2, P x2 -> leq x2 x3) -> leq x1 x3. (* A directed subset of T is a non-empty subset of T such that any two elements in the subset have an upper bound in the subset. *) Definition directed P := (exists x1, P x1) /\ forall x1 x2, P x1 -> P x2 -> exists x3, leq x1 x3 /\ leq x2 x3 /\ P x3. (* Assumption: Let the partial order be directed-complete. That means every directed subset has a supremum. *) Axiom directedComplete : forall P, directed P -> exists x, supremum P x. (* Assumption: Let T have a least element called bottom. This makes our partial order a pointed directed-complete partial order. *) Parameter bottom : T. Axiom bottomLeast : forall x, leq bottom x. (* A monotone function is one which preserves order. We only need to consider functions for which the domain and codomain are identical and have the same order relation, but this need not be the case for monotone functions in general. *) Definition monotone f := forall x1 x2, leq x1 x2 -> leq (f x1) (f x2). (* A function is Scott-continuous if it preserves suprema of directed subsets. We only need to consider functions for which the domain and codomain are identical and have the same order relation, but this need not be the case for continuous functions in general. *) Definition continuous (f : T -> T) := forall P x1, directed P -> supremum P x1 -> supremum (fun x2 => exists x3, P x3 /\ x2 = f x3) (f x1). (* This function performs iterated application of a function to bottom. *) Fixpoint approx f n := match n with | 0 => bottom | S n => f (approx f n) end.
Next, I proved a few lemmas. To keep the article short, I will only state them; the full proofs are here.
(* We will need this simple lemma about pairs of natural numbers. *) Lemma natDiff : forall n1 n2, exists n3, n1 = add n2 n3 \/ n2 = add n1 n3. (* The supremum of a subset of T, if it exists, is unique. *) Lemma supremumUniqueness : forall P x1 x2, supremum P x1 -> supremum P x2 -> x1 = x2. (* Scott-continuity implies monotonicity. *) Lemma continuousImpliesMonotone : forall f, continuous f -> monotone f. (* Iterated applications of a monotone function f to bottom form an ω-chain, which means they are a totally ordered subset of T. This ω-chain is called the ascending Kleene chain of f. *) Lemma omegaChain : forall f n m, monotone f -> leq (approx f n) (approx f m) \/ leq (approx f m) (approx f n). (* The ascending Kleene chain of f is directed. *) Lemma kleeneChainDirected : forall f, monotone f -> directed (fun x2 => exists n, x2 = approx f n).
To give you an idea of what an actual proof looks like in Coq, below is a proof of one of the easier lemmas above. The proof is virtually impossible to read without stepping through it interactively, so don’t worry if it doesn’t make any sense to you here.
Lemma supremumUniqueness : forall P x1 x2, supremum P x1 -> supremum P x2 -> x1 = x2. Proof. intros. unfold supremum in H; destruct H. unfold supremum in H0; destruct H0. apply H1 in H0. apply H2 in H. apply antisym; auto. Qed.
And finally, this is the main result I proved (the proof is here):
(* The Kleene fixed-point theorem states that the least fixed-point of a Scott- continuous function over a pointed directed-complete partial order exists and is the supremum of the ascending Kleene chain. *) Theorem kleene : forall f, continuous f -> exists x1, supremum (fun x2 => exists n, x2 = approx f n) x1 /\ f x1 = x1 /\ (forall x2, f x2 = x2 -> leq x1 x2).
There’s nothing better than typing
Qed at the end of a long proof and watching it turn green as Coq verifies it. What’s really amazing to me is that Stephen Kleene probably proved this without the help of a computer, but I was able to verify it with the highest possible scrutiny. It’s as if he wrote an impressive program without ever having run it, and it turned out not to have any bugs! This is more than just an analogy. When you work with Coq, you become intimately familiar with the interpretation of propositions as types and proofs as programs.Case study: soundness of a type system
A successful formula for writing papers about programming languages theory is the following:
- Define the syntax of a small but novel language (usually based on the lambda calculus).
- Define a type system for the language (a set of rules that specify which programs are legal).
- Define a semantics for the language (i.e., describe what happens when you run a program).
- Prove that the type system prevents programs from “getting stuck” according to the semantics.
The theorem that is proven in that last step is called soundness. A few months ago, I wanted to try doing a formally-verified soundness proof.
The simply-typed lambda calculus is essentially the smallest programming language with higher-order functions and a meaningful type system [4]. I started by defining the abstract syntax of the language in Coq:
Inductive term : Set := | eUnit : term | eVar : id -> term | eAbs : id -> type -> term -> term | eApp : term -> term -> term with type : Set := | tUnit : type | tArrow : type -> type -> type.
To keep this article short, I won’t describe how the language works. There are many good introductions. My favorite is Chapter 9 of Benjamin C. Pierce’s wonderful book called Types and Programming Languages.
Below are the typing rules. You can add whatever base types you like (e.g., Booleans, integers, etc.) to the simply-typed lambda calculus, but to keep things simple I only have a rather useless “unit” type which has only a single value (akin to an empty tuple).
Inductive hasType : context -> term -> type -> Prop := | htUnit : forall c, hasType c eUnit tUnit | htVar : forall x t c, lookupVar c x = Some t -> hasType c (eVar x) t | htAbs : forall e x t1 t2 c, hasType (cExtend c x t1) e t2 -> hasType c (eAbs x t1 e) (tArrow t1 t2) | htApp : forall e1 e2 t1 t2 c, hasType c e1 t1 -> hasType c e2 (tArrow t1 t2) -> hasType c (eApp e2 e1) t2.
To specify the semantics, I defined a small-step operational semantics. The main idea is that you define a relation which says what steps a program takes when it is run. There are many ways to define the semantics of a programming language, and this is just one of them.
Inductive step : term -> term -> Prop := | sBeta : forall e1 e2 x t, value e2 -> step (eApp (eAbs x t e1) e2) (sub e1 x e2) | sApp1 : forall e1 e2 e3, step e1 e2 -> step (eApp e1 e3) (eApp e2 e3) | sApp2 : forall e1 e2 e3, value e1 -> step e2 e3 -> step (eApp e1 e2) (eApp e1 e3).
How do we know when a program has finished running? We just have to define what kinds of programs are “fully evaluated.”
Inductive value : term -> Prop := | vUnit : value eUnit | vAbs : forall e x t, value (eAbs x t e).
This states that a value (i.e., an expression which has been fully evaluated) is either the unit constant or a function. So function applications are not values, since they can be reduced.
An expression is in normal form if there are no more steps it can take:
Definition normalForm e1 := ~ exists e2, step e1 e2.
A stuck program is one which is in normal form but is not a value:
Definition stuck e := normalForm e /\ ~ value e.
Soundness means a program that is well-typed will never get stuck (
stepStar is the transitive reflexive closure of the step relation defined above):Theorem soundness : forall e1 e2 t, hasType cEmpty e1 t -> stepStar e1 e2 -> ~ stuck e2.
The proof, including definitions and lemmas, is about 500 lines long. For such a simple language, this was quite a difficult undertaking! I recall working on this for an entire weekend, probably 8 hours both days. Now I really appreciate when research papers include a formally verified soundness proof.
Conclusion
I think of Coq as an extension of my own ability to reason logically. When I’m in doubt about something, I open the Coq IDE and try to prove it. I think the reason this is so valuable to me is that I often mull over functional programming, types, logic, algorithms, etc. These kinds of things are well-suited to formalization.
Unfortunately, machine-checked theorem proving is not very easy to learn, which is probably why it’s so esoteric. It’s difficult to prove nontrivial results without a graduate-level understanding of type theory (even then it’s still difficult). The most accessible introduction is Benjamin C. Pierce’s Software Foundations, which is freely available online. After that, read Adam Chlipala’s Certified Programming with Dependent Types, which is also freely available online.
I am not an expert in Coq by any means, and my proofs are probably longer and clunkier than they need to be. I only know basic techniques, but a nice thing about logic is that the underlying rules are very simple. I have reached a point where I can prove anything in Coq that I can rigorously prove on paper (given enough time). The two proofs I described in this article took me a few days each, and I’m steadily getting better.
Footnotes
- Strictly speaking, the language itself is called Gallina, and “Coq” refers to the system as a whole.
- There is also an Emacs-based interface, but I’m a Vim user. A friend helped me set it up with Spacemacs, but I still found navigating proofs in CoqIDE to be more a little more intuitive.
- I should know better than to say it’s impossible. Coq allows you to add your own axioms, which is dangerous because your axioms might be inconsistent.
- One could argue that the SK combinator calculus is smaller and still fits this description.
What are covariance and contravariance?
July 21, 2017
Subtyping is a tricky topic in programming language theory. The trickiness comes from a pair of frequently misunderstood phenomena called covariance and contravariance. This article will explain what these terms mean.
The following notation will be used:
A ≼ BmeansAis a subtype ofB.A → Bis the type of functions for which the argument type isAand the return type isB.x : Ameansxhas typeA.
A motivating question
Suppose I have these three types:
Greyhound ≼ Dog ≼ Animal
So
Greyhound is a subtype of Dog, and Dog is a subtype of Animal. Subtyping is usually transitive, so we’ll say Greyhound is also a subtype of Animal.Question: Which of the following types could be subtypes of
Dog → Dog?Greyhound → GreyhoundGreyhound → AnimalAnimal → AnimalAnimal → Greyhound
How do we answer this question? Let
f be a function which takes a Dog → Dog function as its argument. We don’t care about the return type. For concreteness, we can say f : (Dog → Dog) → String.Now I want to call
f with some function g. Let’s see what happens when g has each of the four types above.1. Suppose
g : Greyhound → Greyhound. Is f(g) type safe?No, because
f might try to call its argument (g) with a different subtype of Dog, like a GermanShepherd.2. Suppose
g : Greyhound → Animal. Is f(g) type safe?No, for the same reason as (1).
3. Suppose
g : Animal → Animal. Is f(g) type safe?No, because
f might call its argument (g) and then try to make the return value bark. Not every Animal can bark.4. Suppose
g : Animal → Greyhound. Is f(g) type safe?Yes—this one is safe.
f might call its argument (g) with any kind of Dog, and all Dogs are Animals. Likewise, it may assume the result is a Dog, and all Greyhounds are Dogs.What’s going on?
So this is safe:
(Animal → Greyhound) ≼ (Dog → Dog)
The return types are straightforward:
Greyhound is a subtype of Dog. But the argument types are flipped around: Animal is a supertype of Dog!To state this strange behavior in the proper jargon, we allow function types to be covariant in their return type and contravariant in their argument type. Covariance in the return type means
A ≼ B implies (T → A) ≼ (T → B) (A stays on the left of the ≼, and B stays on the right). Contravariance in the argument type means A ≼ B implies (B → T) ≼ (A → T) (A and B flipped sides).Fun fact: In TypeScript, argument types are bivariant (both covariant and contravariant), which is unsound (although now in TypeScript 2.6 you can fix this with
--strictFunctionTypes or --strict). Eiffel also got this wrong, making argument types covariant instead of contravariant.What about other types?
Question: Could
List<Dog> be a subtype of List<Animal>?The answer is a little nuanced. If lists are immutable, then it’s safe to say yes. But if lists are mutable, then definitely not!
Why? Suppose I need a
List<Animal> and you pass me a List<Dog>. Since I think I have a List<Animal>, I might try to insert a Cat into it. Now your List<Dog> has a Cat in it! The type system should not allow this.Formally: we can allow the type of immutable lists to be covariant in its type parameter, but the type of mutable lists must be invariant (neither covariant nor contravariant) in its type parameter.
Fun fact: In Java, arrays are both mutable and covariant. This is, of course, unsound.
Type safe dimensional analysis in Haskell
July 16, 2017
Years ago my colleague Gustavo asked how I would represent physical units like
m/s or kg*m/s^2 as types so the compiler can check that they match up and cancel correctly. F# supports this natively, but it felt weird to have it baked into the type system. It seemed too ad hoc, though I didn’t know of anything better.Today I was thinking about this again, and I found a way to do it in Haskell. The main idea is to represent units of measure as function spaces. For example, the unit
m/s can be encoded as the type Seconds -> Meters. The numerator becomes the return type, and the denominator the argument type. Function types can be composed to form more interesting units, such as Seconds -> Seconds -> Meters for acceleration. Products can be represented by higher-order functions. A special type class will enable us to easily convert a Double into a quantity with any units of measure and vice versa.There are a handful of packages on Hackage for doing dimensional analysis. This article will demonstrate a simple, portable way to do it without relying on any language extensions. As we will see in Example 3, this implementation sometimes requires the programmer to provide proofs of unit equivalence (which can be tedious at times). This is less convenient than other libraries, but it’s an interesting exhibition of the power of vanilla Haskell.
Units as function spaces
First, we define some types for base units. We will never instantiate these types, so we don’t specify any constructors. They are only used for type checking.
data Meter data Kilogram data Second
Next, we need types which actually represent quantities with units. For the base units above, we define
BaseQuantity as follows:newtype BaseQuantity a = BaseQuantity Double
It’s just a wrapper for
Double, but written as a phantom type. The type parameter a keeps track of the base unit. For example, BaseQuantity Meter is a type which represents a length.A quotient
a / b of two units a and b will be represented by the function space b -> a. For example, m / s becomes BaseQuantity Second -> BaseQuantity Meter. To make intentions clear, we formalize this idea as a type synonym:type Quotient a b = b -> a
We also need a
BaseQuantity for dimensionless quantities like π. We could define a new base type for this, but () does the job nicely:type Dimensionless = BaseQuantity ()
We can also define multiplicative inverse
a^-1 as the quotient 1 / a.type Inverse a = Quotient Dimensionless a
A product
a * b can be represented as a / b^-1:type Product a b = Quotient a (Inverse b)
A helpful synonym to make square units like
m^2 easier to read:type Square a = Product a a
All quantities have some numeric value. We formalize this in Haskell using a type class:
class Quantity a where construct :: Double -> a destruct :: a -> Double
The instance for base quantities is trivial, since
BaseQuantity just wraps a Double:instance Quantity (BaseQuantity a) where construct = BaseQuantity destruct (BaseQuantity x) = x
Quotients of quantities are quantities as well. To construct a
Quotient from a Double, we define a function which destructs its argument, multiplies the result by the given Double, and constructs a quantity of the return type (the numerator unit). To destruct a Quotient, we first construct 1 in the denominator unit (the argument type), use the quotient to convert it into the numerator unit, and destruct the result.instance (Quantity q, Quantity r) => Quantity (q -> r) where construct x = \y -> construct (x * (destruct y)) destruct x = destruct (x (construct 1))
We need to define an axiom that allows us to rearrange quotients:
-- a / (b / c) = c / (b / a) quotientAxiom :: (Quantity a, Quantity b, Quantity c) => Quotient a (Quotient b c) -> Quotient c (Quotient b a) quotientAxiom = construct . destruct
Exercise for the reader: Do we need this axiom, or is there a way to derive it without destructing any quantities? Alternatively, are there any other axioms we need?
And finally, we define the familiar arithmetic operations:
-- We can add two quantities of the same unit. infixl 6 .+. (.+.) :: Quantity a => a -> a -> a (.+.) x y = construct $ (destruct x) + (destruct y) -- We can subtract two quantities of the same unit. infixl 6 .-. (.-.) :: Quantity a => a -> a -> a (.-.) x y = construct $ (destruct x) - (destruct y) -- We can multiply any two quantities. infixl 7 .*. (.*.) :: (Quantity a, Quantity b) => a -> b -> Product a b (.*.) x y = \z -> construct $ destruct (z y) * destruct x -- We can divide any two quantities. infixl 7 ./. (./.) :: (Quantity a, Quantity b) => a -> b -> Quotient a b (./.) x y = \z -> construct $ (destruct z) * (destruct x) / (destruct y)
Other primitive operations, such as comparison, can be defined similarly.
Examples
The examples below will use these helpful type synonyms:
type Length = BaseQuantity Meter type Mass = BaseQuantity Kilogram type Time = BaseQuantity Second type Area = Square Length type Velocity = Quotient Length Time
Example 1: Tracking units in types
Let’s calculate the area of a table.
tableWidth :: Length tableWidth = construct 1.5 tableHeight :: Length tableHeight = construct 2.5 tableArea :: Area tableArea = tableWidth .*. tableHeight
Calculations with quantities are type safe. Suppose we defined the mass of the table:
tableMass :: Mass tableMass = construct 150
Then the following is a type error:
tableArea :: Area tableArea = tableWidth .*. tableMass -- Error: Couldn't match type ‘Kilogram’ with ‘Meter’ -- Expected type: Area -- Actual type: Product Length Mass
Example 2: Quantities as functions
Suppose we want to calculate how far a train will travel, given its velocity and the duration of the trip.
trainVelocity :: Velocity trainVelocity = construct 30 tripDuration :: Time tripDuration = construct 5000
Here we demonstrate the correspondence between quantities and functions.
Velocity is a synonym for Length / Time, but it’s also a function from Time to Length. Given a Time, we can simply “apply” a Velocity to it to get a Length:tripDistance :: Length tripDistance = trainVelocity tripDuration
So multiplication of
a / b by b is just function application.Example 3: Manual proofs of unit equality
Let’s define a function that takes a
Length and a Velocity and returns a Time. First try:calculateDuration :: Length -> Velocity -> Time calculateDuration distance velocity = distance ./. velocity -- Error: Couldn't match type ‘Velocity -> Length’ with ‘BaseQuantity Second’ -- Expected type: Time -- Actual type: Quotient Length Velocity
Haskell doesn’t know that
Length / Velocity = Time. If this is indeed true, there will be a way to manipulate the program (without destructing the quantity) to make it type check by swapping arguments, defining new functions, using the quotientAxiom, etc. This is similar to what one would do in a proof assistant like Agda or Coq.So we have:
distance ./. velocity :: Length / Velocity
Velocity is a type synonym for Length / Time, so we actually have:distance ./. velocity :: Length / (Length / Time)
We can apply the
quotientAxiom to get:quotientAxiom (distance ./. velocity) :: Time / (Length / Length)
Under the interpretation of units as function spaces, we have:
quotientAxiom (distance ./. velocity) :: (Length -> Length) -> Time
We can apply
id to cancel the Lengths and get a Time. Putting it all together:calculateDuration :: Length -> Velocity -> Time calculateDuration distance velocity = quotientAxiom (distance ./. velocity) id
Now we can calculate how long the trip from Example 2 would take if the train traveled at 40 m/s instead of 30 m/s.
fasterVelocity :: Velocity fasterVelocity = construct 40 shorterDuration :: Time shorterDuration = calculateDuration tripDistance fasterVelocity
Example 4: Destructing the results
When we are done calculating, we can convert the results back to
Doubles with the destruct function. Let’s print the results of the first three examples:main = do putStrLn $ "tableArea: " ++ (show $ destruct $ tableArea) ++ " m^2" putStrLn $ "tripDistance: " ++ (show $ destruct $ tripDistance) ++ " m" putStrLn $ "shorterDuration: " ++ (show $ destruct $ shorterDuration) ++ " s"
The output is:
tableArea: 3.75 m^2 tripDistance: 150000.0 m shorterDuration: 3750.0 s
Conclusion
We can do type safe dimensional analysis by encoding units as function spaces. The basic pattern is:
- Construct whatever quantities you want using the
constructfunction. A type annotation can be used to specify the units, or you can let type inference figure out the units automatically. - Do type safe operations on these quantities using the operations
.+.,.*., etc. You may need to manually rearrange units or cancel them to satisfy the type checker, but this will always be possible if your units are actually correct (exercise for the reader: prove it!). - When you are done with calculation and want to use the resulting quantities, the
destructfunction will convert them intoDoubles.
It’s inconvenient that we sometimes have to provide manual proofs of unit equivalence. It would be nice if rearranging and canceling units was completely automatic. But at least we have type safety!
Finding ambiguities in context-free grammars
January 2, 2017
Recently I was working on a parser, and I thought the grammar might be ambiguous. I looked around for a tool to help me detect ambiguities in context-free grammars, but I couldn’t find anything that worked. So I built CFG Checker!
It is only semi-decidable to determine whether an arbitrary context-free grammar is ambiguous. The best we can do is generate all derivations in a breadth-first fashion and look for two which produce the same sentential form. So that’s exactly what CFG Checker does. If the input grammar is ambiguous, CFG Checker will eventually find a minimal ambiguous sentential form. If the grammar is unambiguous, CFG Checker will either reach this conclusion or loop forever.
Here’s how it works. You specify the grammar as a series of production rules:
expression = number | sum sum = expression + expression
Then you run CFG Checker on it:
$ cfg-checker example.cfg .... Found a sentential form with two different derivations: expression + expression + expression Derivation 1: 0: expression 1: sum 2: expression + expression 3: expression + sum 4: expression + expression + expression Derivation 2: 0: expression 1: sum 2: expression + expression 3: sum + expression 4: expression + expression + expression
If it doesn’t finish within a few seconds, the grammar is probably unambiguous unless you gave it some pathological input.
CFG Checker is written in C++ and has no dependencies. For more details, see the GitHub project.
Decomposing a string into its elements
December 29, 2016
My colleague Esther proposed the following challenge: given a string, decompose it into elemental symbols from the periodic table (if possible). For example,
Hi Esther becomes H I Es Th Er. In general there might be no solutions, one solution, or several.I implemented it in Haskell with dynamic programming. The
elementize function does all the work, using the list monad to compute all possible solutions.import Data.Char (isLetter, toLower)
import Data.Function.Memoize (memoFix)
import Data.List (intercalate, isPrefixOf)
import System.Environment (getArgs)
elements = [ "H" , "He" , "Li" , "Be" , "B" , "C" , "N" , "O" , "F"
, "Ne" , "Na" , "Mg" , "Al" , "Si" , "P" , "S" , "Cl" , "Ar"
, "K" , "Ca" , "Sc" , "Ti" , "V" , "Cr" , "Mn" , "Fe" , "Co"
, "Ni" , "Cu" , "Zn" , "Ga" , "Ge" , "As" , "Se" , "Br" , "Kr"
, "Rb" , "Sr" , "Y" , "Zr" , "Nb" , "Mo" , "Tc" , "Ru" , "Rh"
, "Pd" , "Ag" , "Cd" , "In" , "Sn" , "Sb" , "Te" , "I" , "Xe"
, "Cs" , "Ba" , "La" , "Ce" , "Pr" , "Nd" , "Pm" , "Sm" , "Eu"
, "Gd" , "Tb" , "Dy" , "Ho" , "Er" , "Tm" , "Yb" , "Lu" , "Hf"
, "Ta" , "W" , "Re" , "Os" , "Ir" , "Pt" , "Au" , "Hg" , "Tl"
, "Pb" , "Bi" , "Po" , "At" , "Rn" , "Fr" , "Ra" , "Ac" , "Th"
, "Pa" , "U" , "Np" , "Pu" , "Am" , "Cm" , "Bk" , "Cf" , "Es"
, "Fm" , "Md" , "No" , "Lr" , "Rf" , "Db" , "Sg" , "Bh" , "Hs"
, "Mt" , "Ds" , "Rg" , "Cn" , "Uut", "Uuq", "Uup", "Uuh", "Uus"
, "Uuo" ]
elementize = memoFix (\fn str ->
if null str
then return []
else do element <- filterPrefixes elements str
soln <- fn $ drop (length element) str
return $ element : soln)
where toLowerStr = map toLower
filterPrefixes prefixes str = filter
(\x -> isPrefixOf (toLowerStr x) (toLowerStr str))
prefixes
main = do args <- getArgs
putStrLn $ intercalate"\n" $ map (intercalate " ")
(elementize $ filter isLetter $ concat args)
To compile the program, you need the memoize package. Once compiled, it can be run like this:
$ ./elementizer hi esther H I Es Th Er
Fun fact: the longest word (in the macOS words file) that can be decomposed into elements is nonrepresentationalism, and it has 4 decompositions:
No N Re P Re Se N Ta Ti O Na Li SmN O N Re P Re Se N Ta Ti O Na Li SmNo N Re P Re Se N Ta Ti O N Al I SmN O N Re P Re Se N Ta Ti O N Al I Sm