Skip to content

Instantly share code, notes, and snippets.

@Pet3ris
Created Dec 6, 2012
Embed
What would you like to do?
Basic program induction
{-# LANGUAGE GADTs #-}
import Control.Monad
-- Basic program inducer
--
-- usage:
-- take 5 $ solve [(1, 2::Int), (2, 3)]
-- => [(+ 1 X),(+ X 1),(+ 0 (+ 1 X)),(+ 0 (+ X 1)),(+ 1 (+ 0 X))]
-- Expressions of the target language
data Expr a where
X :: Expr Int
I :: Int -> Expr Int
B :: Bool -> Expr Bool
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr Int
Eq :: Expr Int -> Expr Int -> Expr Bool
-- Rules for displaying expressions
instance Show (Expr a) where
show X = "X"
show (I n) = show n
show (B b) = show b
show (Add x y) = "(+ " ++ show x ++ " " ++ show y ++ ")"
show (Mul x y) = "(* " ++ show x ++ " " ++ show y ++ ")"
show (Eq x y) = "(== " ++ show x ++ " " ++ show y ++ ")"
-- Rules for evaluating expressions
eval :: Int -> Expr a -> a
eval x X = x
eval x (I n) = n
eval x (B b) = b
eval x (Add e1 e2) = eval x e1 + eval x e2
eval x (Mul e1 e2) = eval x e1 * eval x e2
eval x (Eq e1 e2) = eval x e1 == eval x e2
-- check if f(x) = y
check :: (Eq y) => Expr y -> (Int, y) -> Bool
check f (x, y) = eval x f == y
-- check if f(xi) = yi for all i
checkAll :: (Eq y) => Expr y -> [(Int, y)] -> Bool
checkAll f = all (check f)
-- lazy list of programs that have the given input-output restrictions
solve :: (Eq y, Programs y) => [(Int, y)] -> [(Expr y)]
solve graph = lazy 1 where
lazy n = (do
program <- programs n
guard (checkAll program graph)
[program]) ++ lazy (n + 1)
-- class for creating programs that return this type
class Programs a where
programs :: Int -> [Expr a]
-- programs with a given number of terms that return integers
instance Programs Int where
programs 1 = [(I 0), (I 1), X]
programs n = do
k <- [1..(n-1)]
lexpr <- programs k
rexpr <- programs (n - k)
[Add lexpr rexpr, Mul lexpr rexpr]
-- programs with a given number of terms that return boolean values
instance Programs Bool where
programs 1 = [(B True), (B False)]
programs n = do
k <- [1..(n-1)]
lexpr <- programs k
rexpr <- programs (n - k)
[Eq lexpr rexpr]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment