Skip to content
/ muri Public

A theorem prover for intuitionistic propositional logic

License

Notifications You must be signed in to change notification settings

ncfavier/muri

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

24 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

muri :: Type -> Maybe Term

muri takes a Haskell type, and generates a Haskell term with that type (or a more general one), if possible.

Equivalently, under the propositions-as-types correspondence, muri is a theorem prover for intuitionistic propositional logic. It takes a proposition as input, and produces a proof of that proposition, if one exists.

Input types are limited to type variables, product types (a, b), sum types Either a b and function types a -> b.

Output terms are built using lambda abstraction, function application, let and case expressions, pair construction and the Left and Right type constructors.

muri was inspired by Lennart Augustsson's Djinn, and uses the LJT calculus from "Contraction-Free Sequent Calculi for Intuitionistic Logic" by Roy Dyckhoff to ensure termination.

Usage

muri TYPE

Examples

$ muri 'a -> (b, c) -> (b, (a, c))'
\a -> \(b, c) -> (b, (a, c))
$ muri '(a, b) -> Either a b'
\(a, b) -> Left a
$ muri 'Either (a, c) (b, c) -> (Either a b, c)'
\a -> case a of { Left (b, c) -> (Left b, c); Right (b, c) -> (Right b, c) }
$ muri '(Either (a -> f) a -> f) -> f'
\a -> a (Left (\c -> a (Right c)))
$ muri '(a -> b) -> (Either (a -> f) b -> f) -> f'
\a -> \b -> b (Left (\c -> b (Right (a c))))
$ muri '(Either (a -> f) (b -> f) -> f) -> ((a, b) -> f) -> f'
\a -> \b -> a (Left (\e -> a (Right (\f -> b (e, f)))))
$ muri '((a -> b) -> c) -> ((a, b -> c) -> b) -> c'
\a -> \b -> a (\f -> b (f, \e -> a (\_ -> e)))
$ muri 'a -> b'
Impossible.