Created
September 27, 2019 13:51
-
-
Save jtpaasch/4c627b7dba7555bade70846f99f2ca71 to your computer and use it in GitHub Desktop.
6.820 Program Analysis - Problem Set 1
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- *************************************************** | |
-- 6.820 - Program Analysis - Fall 2019 | |
-- PROBLEM SET 1 | |
-- *************************************************** | |
-- --------------------------------------------------- | |
-- Problem 1 | |
-- --------------------------------------------------- | |
-- Just copying some code from the problem set into this file | |
-- to check that we can load it into ghci and work with it. | |
apply_n f n x = | |
if n == 0 then x | |
else apply_n f (n - 1) (f x) | |
plus a b = apply_n ((+) 1) b a | |
mult a b = apply_n ((+) a) b 0 | |
expon a b = apply_n ((*) a) b 1 | |
-- --------------------------------------------------- | |
-- Problem 2 | |
-- --------------------------------------------------- | |
-- Don't know calculus, so... | |
-- --------------------------------------------------- | |
-- Problem 3 : Sets | |
-- --------------------------------------------------- | |
type IntSet = (Int -> Bool) | |
isMember :: IntSet -> Int -> Bool | |
isMember f x = f x | |
-- Part a : Simple Sets | |
-- --------------------------------------------------- | |
-- A "set" is a function from Int to Bool. | |
-- It checks if an integer is a member of the set. | |
-- An empty set has no members, so no matter what Int | |
-- you give it, it should return False. | |
emptySet :: IntSet -- IntSet == Int -> Bool | |
emptySet x = False | |
-- Check it: | |
-- isMember emptySet 3 == False | |
-- isMember emptySet 5 == False | |
-- The "allInts" set contains all integers. | |
-- So no matter which integer you give it, it should | |
-- return True. | |
allInts :: IntSet | |
allInts x = True | |
-- Check it: | |
-- isMember allInts 3 == True | |
-- isMember allInts 10 == True | |
-- Part b : Intervals | |
-- --------------------------------------------------- | |
-- interval x y contains all the integers in [x, y]. | |
interval :: Int -> Int -> IntSet -- Int -> Int -> (Int -> Bool) | |
interval lBound uBound = \x -> lBound <= x && x <= uBound | |
-- Check it: | |
-- let range = interval 5 10 | |
-- range' = interval 3 7 | |
-- in isMember range 7 == True | |
-- isMember range 13 == False | |
-- isMember range' 2 == False | |
-- isMember range' 5 == False | |
-- Part c : Primes | |
-- --------------------------------------------------- | |
-- Don't care right now... | |
-- Part d : Set Operators | |
-- --------------------------------------------------- | |
-- Boolean Operators | |
-- A "set" is a function that takes an Int and returns a Bool | |
-- indicating whether the Int is in the Set. | |
-- So to build the intersection of two "sets" f and g, | |
-- we build a function that takes an Int, and checks if | |
-- that Int is in both sets f and g. | |
setIntersection :: IntSet -> IntSet -> IntSet | |
setIntersection f g = \x -> f x && g x | |
-- Or in either sets f or g. | |
setUnion:: IntSet -> IntSet -> IntSet | |
setUnion f g = \x -> f x || g x | |
-- Or not in set f. | |
setComplement :: IntSet -> IntSet | |
setComplement f = \x -> not (f x) | |
-- Check it | |
-- let range = interval 5 10 | |
-- range' = interval 3 7 | |
-- intersection range range' | |
-- union range range' | |
-- complement range | |
-- in isMember intersection 6 == True | |
-- isMember intersection 4 == False | |
-- isMember union 6 == True | |
-- isMember union 4 == True | |
-- isMember complement 3 == False | |
-- Part e : Equality | |
-- --------------------------------------------------- | |
-- Not sure. Maybe do set equality for a range, and check every Int in the range. | |
-- --------------------------------------------------- | |
-- Problem 4 : Using Lambda Combinators | |
-- --------------------------------------------------- | |
type LamVar = Char | |
type LamBool = LamVar -> LamVar -> LamVar | |
-- True is represented as a function that takes two arguments and returns the first. | |
true :: LamBool | |
true = \x -> \y -> x | |
-- False is represented as a function that takes two arguments and returns the second. | |
false :: LamBool | |
false = \x -> \y -> y | |
-- Cond is represented as a function that takes a condition and two other arguments. | |
-- If the condition is true, it returns the first argument, otherwise the second. | |
-- cond :: LamBool -> LamBool -> LamBool -> LamBool | |
-- cond = \c -> \e1 -> \e2 -> c e1 e2 | |
-- Check it: | |
-- true 'x' 'y' == 'x' | |
-- false 'x' 'y' == 'y' | |
-- cond true 'x' 'y' == 'x' | |
-- cond false 'x' 'y' == 'y' | |
-- and :: (Char -> Char -> Char) -> (Char -> Char -> Char) -> (Char -> Char -> Char) | |
-- and = \e1 -> \e2 -> cond e1 e2 false | |
-- bnot = \b1 -> cond b1 false true | |
-- --------------------------------------------------- | |
-- Problem 6 : A Normal Order NF Interpreter | |
-- --------------------------------------------------- | |
-- Part c: Renaming Function in Haskell | |
-- --------------------------------------------------- | |
-- Expressions can have the form of variables, applications, or abstractions. | |
data Expr = | |
Var Name -- a variable | |
| App Expr Expr -- application | |
| Lambda Name Expr -- lambda abstraction | |
deriving | |
(Eq, Show) -- use default compiler generated Eq and Show instances | |
-- A variable can have a string name. | |
type Name = String -- a variable name | |
-- @replaceVar ("x", y) z@ takes the expression @z@, and it replaces | |
-- all free occurrences of "x" with the expression @y@. | |
replaceVar :: (Name, Expr) -> Expr -> Expr | |
replaceVar (n, e) src = | |
case src of | |
-- Is the expression a variable? | |
-- If so, replace the variable if it's the one we're looking to replace. | |
Var n' -> | |
case n == n' of | |
True -> e -- If it matches @n@, replace it with @e@. | |
False -> src -- Otherwise, there's no match to replace. | |
-- Is the expression an application? | |
-- If so, replace the variables in each of the subexpressions. | |
App e1 e2 -> App (replaceVar (n, e) e1) (replaceVar (n, e) e2) | |
-- Is the expression a lambda? | |
Lambda n' e' -> | |
case n == n' of | |
True -> src -- @n@ is bound (not free) so we can't replace it. | |
False -> Lambda n' (replaceVar (n, e) e') -- Replace @n@ in the body. | |
-- Note that this last replacement is naive. | |
-- It doesn't prevent variable capture. | |
-- Check it: | |
-- let x = Var "x" | |
-- let y = Var "y" | |
-- replaceVar ("x", y) x -- Returns: @Var "y"@ (it replaces "x" with y) | |
-- replaceVar ("y", y) x -- Returns @Var "x"< (there is no free "x", so it replaces nothing) | |
-- let a = App x y | |
-- let b = App y y | |
-- replaceVar ("x", y) a -- Returns @App (Var "y") (Var "y") (it replaces the first "x" with "y") | |
-- replaceVar ("x", y) b -- Returns @App (Var "y") (Var "y") (no "x" in either expression) | |
-- let z = Var "z" | |
-- let c = Lambda "x" z | |
-- let d = Lambda "y" z | |
-- replaceVar ("x", y) c -- Returns the expression unchanged, because "x" is bound. | |
-- replaceVar ("z", y) d -- Returns the body changed to "y". But now "y" is captured! | |
-- Part d: Doing a Single Step | |
-- --------------------------------------------------- | |
-- Do one step of reduction. | |
normNF_OneStep :: ([Name], Expr) -> Maybe ([Name], Expr) | |
normNF_OneStep (name:names, e) = | |
case e of | |
-- A var can't be reduced any further. | |
Var _ -> Nothing | |
-- If it's an abstraction, we can't reduce further. | |
Lambda _ _ -> Nothing | |
-- If there's an application, we might have a redex. | |
App e1 e2 -> | |
case e1 of | |
-- If the first term is a var, we can't reduce further. | |
Var _ -> Nothing | |
-- If the first term is an application, we can't reduce further. | |
App _ _ -> Nothing | |
-- If the first term is an abstraction, we can apply it to the argument. | |
Lambda n' e' -> | |
-- Alpha rename the bound variables in the body, then do the reduction. | |
let alpha_converted_e = replaceVar (n', Var name) e' | |
reduced_e = replaceVar (name, e2) alpha_converted_e | |
in Just (names, reduced_e) | |
-- Check it: | |
-- let x = Var "x" | |
-- let y = Var "y" | |
-- let z = Var "z" | |
-- let lxx = Lambda "x" x | |
-- let lxy = Lambda "x" y | |
-- let lxx_y = App lxx y | |
-- normNF_OneStep (["a", "b"], lxx) ==> Returns: Nothing | |
-- normNF_OneStep (["a", "b"], lxx_y) ==> Returns: Just (["b"],Var "y") | |
-- Part e: Repitition | |
-- --------------------------------------------------- | |
-- Do @n@ steps of reduction. | |
normNF_n :: Int -> ([Name], Expr) -> ([Name], Expr) | |
normNF_n gas (names, e) = | |
case gas of | |
0 -> (names, e) | |
_ -> | |
case normNF_OneStep (names, e) of | |
Nothing -> (names, e) | |
Just (names', e') -> normNF_n (gas - 1) (names', e') | |
-- Check it: | |
-- let x = Var "x" | |
-- let y = Var "y" | |
-- let z = Var "z" | |
-- let lxx = Lambda "x" x | |
-- let lxx_y = App lxx y | |
-- normNF_n 3 (["a", "b"], lxx_y) ==> Returns: (["b"],Var "y") | |
-- let lylxx_y_z = App (Lambda "y" (App lxx y)) z | |
-- normNF_n 3 (["a", "b", "c"], lylxx_y_z) ==> Returns: (["c"],Var "z") | |
-- Part f: Generating New Names | |
-- --------------------------------------------------- | |
-- A list of integers. | |
freshNames = [1..] | |
-- Gather all names used in an expression. | |
usedNames :: Expr -> [Name] | |
usedNames e = | |
case e of | |
Var n -> [n] | |
App e1 e2 -> (usedNames e1) ++ (usedNames e2) | |
Lambda n e' -> (n : usedNames e') | |
-- Check it: | |
-- let x = Var "x" | |
-- let y = Var "y" | |
-- let lxx = Lambda "x" x | |
-- let lxx_y = App lxx y | |
-- usedNames lxx_y ==> Returns: ["x", "x", "y"] | |
-- Part g: Finishing Up | |
-- --------------------------------------------------- | |
-- @normNF 3 (App (Lambda "x" (Var "x")) (Var "y"))@ performs 3 reductions. | |
normNF :: Int -> Expr -> Expr | |
normNF gas e = | |
let taken_names = usedNames e | |
num_names = length taken_names | |
fresh_names = map show (take num_names freshNames) | |
(fresh_names', e') = normNF_n gas (fresh_names, e) | |
in e' | |
-- Check it: | |
-- let x = Var "x" | |
-- let y = Var "y" | |
-- let lxx = Lambda "x" x | |
-- let lxx_y = App lxx y | |
-- normNF 5 lxx_y ==> Returns: Var "y" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment