Initial

2025-11-17 14:25:48 +01:00
commit 9bdbe830d2
13 changed files with 1390 additions and 0 deletions
--- a/3/.envrc
+++ b/3/.envrc
@ -0,0 +1 @@
+use flake
--- a/3/.gitignore
+++ b/3/.gitignore
@ -0,0 +1,20 @@
+.DS_Store
+.idea
+*.log
+tmp/
+
+AbsChi.hs
+DocChi.txt
+ErrM.hs
+LexChi.x
+ParChi.y
+PrintChi.hs
+SkelChi.hs
+TestChi.hs
+
+.direnv/
+dist-newstyle/
+
+*.bbl
+*.pdf
+*.tex
--- a/3/Chi.cf
+++ b/3/Chi.cf
@ -0,0 +1,27 @@
+token Constructor (["ABCDEFGHIJKLMNOPQRSTUVWXYZ"]
+                   (["abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_-'"]
+                   | digit
+                   )*);
+token Variable    (["abcdefghijklmnopqrstuvwxyz_"]
+                   (["abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_-'"]
+                   | digit
+                   )*);
+
+Apply  . Exp1 ::= Exp1 Exp2;
+Lambda . Exp  ::= "\\" Variable "." Exp;
+Case   . Exp1 ::= "case" Exp "of" "{" [Br] "}";
+Rec    . Exp  ::= "rec" Variable "=" Exp;
+Var    . Exp2 ::= Variable;
+Const  . Exp2 ::= Constructor "(" [Exp] ")";
+_      . Exp  ::= Exp1;
+_      . Exp1 ::= Exp2;
+_      . Exp2 ::= "(" Exp ")";
+
+Branch . Br ::= Constructor "(" [Variable] ")" "->" Exp;
+
+separator Br       ";";
+separator Exp      ",";
+separator Variable ",";
+
+comment "--";
+comment "{-" "-}";
--- a/3/Chi.hs
+++ b/3/Chi.hs
@ -0,0 +1,787 @@
+-- | A wrapper module that exports the generated abstract syntax of χ
+-- as well as some definitions that may be useful when testing χ code
+-- or interpreters.
+
+{-# LANGUAGE DeriveGeneric,
+             GeneralizedNewtypeDeriving,
+             PatternSynonyms,
+             StandaloneDeriving,
+             TemplateHaskell #-}
+
+module Chi
+  ( -- * The abstract syntax of χ
+    module AbsChi
+    -- * Parsing and pretty-printing
+  , parse
+  , pretty
+    -- * An example
+  , add
+    -- * Conversions
+  , fromNatural
+  , toNatural
+  , Code
+  , Decode
+  , runCode
+  , runDecode
+  , asDecoder
+  , code
+  , decode
+  , codeVar
+  , codeCon
+  , decodeVar
+  , decodeCon
+  , internalCode
+    -- * Free and bound variables
+  , free
+  , bound
+  , closed
+    -- * Functions that can be used to run internal substitution functions and self-interpreters
+  , runInternalSubstitution
+  , runSelfInterpreter
+    -- * Some testing procedures
+  , testEvaluation
+  , testMultiplication
+  , testSubstitution
+  , testInternalSubstitutionWith
+  , testInternalSubstitution
+  , testSelfInterpreterWith
+  , testSelfInterpreter
+  , testTuringMachineInterpreter
+  )
+  where
+
+import AbsChi
+import Control.Applicative
+  (Applicative, Alternative, (<$>), (<*>), empty)
+import Control.Monad.State.Strict (State, evalState, put, get)
+import Control.Monad.Trans (lift)
+import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT)
+import Data.Hashable (Hashable)
+import Data.HashMap.Strict (HashMap)
+import qualified Data.HashMap.Strict as Map
+import Data.HashSet (HashSet)
+import qualified Data.HashSet as Set
+import Data.List (genericReplicate)
+import Data.Typeable (Typeable)
+import GHC.Generics (Generic)
+import Numeric.Natural (Natural)
+import ParChi (pExp, myLexer)
+import PrintChi (printTree)
+import Text.PrettyPrint.HughesPJ (fsep, nest, render, text, vcat, (<+>))
+import Test.QuickCheck
+  (Arbitrary(arbitrary, shrink), Gen, NonNegative(NonNegative),
+   Property, Testable, arbitrarySizedNatural, choose, counterexample,
+   elements, forAll, forAllShrink, genericShrink, maxSuccess, oneof,
+   quickCheckAll, quickCheckResult, quickCheckWithResult,
+   shrinkIntegral, sized, stdArgs, vectorOf, (.&&.), (==>))
+import Test.QuickCheck.Test (isSuccess)
+
+------------------------------------------------------------------------
+-- Some orphan instances for types defined in AbsChi
+
+deriving instance Generic Constructor
+deriving instance Generic Variable
+deriving instance Generic Exp
+deriving instance Generic Br
+
+instance Hashable Constructor
+instance Hashable Variable
+
+------------------------------------------------------------------------
+-- Orphan Arbitrary instances and related definitions
+
+-- | A combinator that can be used to construct properties involving
+-- universal quantification over natural numbers.
+
+forAllNatural :: Testable p => (Natural -> p) -> Property
+forAllNatural = forAllShrink arbitrarySizedNatural shrinkIntegral
+
+-- | A QuickCheck generator for (a small number of) constructors.
+
+instance Arbitrary Constructor where
+  arbitrary = elements $ map Constructor ["Zero", "Suc"]
+
+  shrink (Constructor "Suc") = [Constructor "Zero"]
+  shrink _                   = []
+
+-- | A QuickCheck generator for (a small number of) variables.
+
+instance Arbitrary Variable where
+  arbitrary = elements $ map Variable ["x", "y"]
+
+  shrink (Variable "y") = [Variable "x"]
+  shrink _              = []
+
+-- | A QuickCheck generator for branches.
+
+instance Arbitrary Br where
+  arbitrary = Branch <$> arbitrary <*> arbitrary <*> arbitrary
+
+  shrink = genericShrink
+
+-- | A QuickCheck generator for terms.
+
+instance Arbitrary Exp where
+  arbitrary = sized gen
+    where
+    gen n = oneof $
+      [ Var <$> arbitrary ] ++
+      if n <= 0 then [] else
+        [ Apply <$> g <*> g
+        , Lambda <$> arbitrary <*> g
+        , Case <$> g <*> do
+            i  <- choose (0, n `div` 3)
+            es <- vectorOf i g
+            mapM (\e -> Branch <$> arbitrary
+                               <*> do i <- choose (0, n `div` 3)
+                                      vectorOf i arbitrary
+                               <*> return e) es
+        , Rec <$> arbitrary <*> g
+        , Const <$> arbitrary <*> do
+            n  <- choose (0, n `div` 3)
+            vectorOf n g
+        ]
+      where
+      g = gen (n `div` 2)
+
+  shrink = genericShrink
+
+------------------------------------------------------------------------
+-- Parsing and pretty-printing
+
+-- | Tries to parse a χ program. If parsing fails, then an exception
+-- is raised.
+
+parse :: String -> Exp
+parse s = case pExp (myLexer s) of
+  Right e -> e
+  Left  s -> error ("Parse failed: " ++ s)
+
+-- | Pretty-prints a χ program.
+
+pretty :: Exp -> String
+pretty = printTree
+
+prop_parse_pretty e =
+  parse (pretty e) == e
+
+------------------------------------------------------------------------
+-- An example
+
+-- | A χ program for addition of natural numbers.
+
+add :: Exp
+add = parse
+  "rec add = \\x. \\y. case x of\
+  \  { Zero() -> y\
+  \  ; Suc(n) -> Suc(add n y)\
+  \  }"
+
+------------------------------------------------------------------------
+-- Free and bound variables
+
+-- | Helper function used to implement 'free' and 'bound'.
+
+freeAndBound :: Exp -> (HashSet Variable, HashSet Variable)
+freeAndBound e = case e of
+  Var x       -> (Set.singleton x, Set.empty)
+  Lambda x e  -> let (f, b) = freeAndBound e in
+                 (Set.delete x f, if   Set.member x f
+                                  then Set.insert x b
+                                  else b)
+  Rec x e     -> freeAndBound (Lambda x e)
+  Case e bs   -> freeAndBoundL (e : map (\(Branch _ xs e) ->
+                                            foldr Lambda e xs)
+                                        bs)
+  Apply e1 e2 -> freeAndBoundL [e1, e2]
+  Const _ es  -> freeAndBoundL es
+  where
+  freeAndBoundL :: [Exp] -> (HashSet Variable, HashSet Variable)
+  freeAndBoundL es = (Set.unions fs, Set.unions bs)
+    where (fs, bs) = unzip $ map freeAndBound es
+
+-- | The term's free variables.
+
+free :: Exp -> HashSet Variable
+free e = fst (freeAndBound e)
+
+-- | Bound variables that actually occur bound in the term (not in a
+-- binder). For @λx.x@ a singleton set containing @x@ is returned, but
+-- for @λx.Nil()@ the empty set is returned.
+
+bound :: Exp -> HashSet Variable
+bound e = snd (freeAndBound e)
+
+-- | A QuickCheck generator for closed terms.
+
+closed :: Gen Exp
+closed = do
+  e <- arbitrary
+  let xs = free e
+  bs <- mapM binder (Set.toList xs)
+  return $ foldr ($) e bs
+  where
+  binder x = elements [Rec x, Lambda x]
+
+prop_closed =
+  forAll closed $ \e ->
+    free e == Set.empty
+
+------------------------------------------------------------------------
+-- Conversions
+
+-- | Converts a Haskell natural number to its χ representation.
+
+fromNatural :: Natural -> Exp
+fromNatural n
+  | n == 0    = Const (Constructor "Zero") []
+  | otherwise = Const (Constructor "Suc")  [fromNatural (n - 1)]
+
+-- | Tries to convert the given χ expression to a natural number.
+
+toNatural :: Exp -> Maybe Natural
+toNatural e = case e of
+  Const (Constructor "Zero") []  -> Just 0
+  Const (Constructor "Suc")  [n] -> succ <$> toNatural n
+  _                              -> Nothing
+
+prop_toNatural_fromNatural =
+  forAllNatural $ \n ->
+    toNatural (fromNatural n) == Just n
+
+-- | Partial bijections between strings and natural numbers.
+
+data PartialBijection =
+  Maps (HashMap String Natural)
+       (HashMap Natural String)
+
+-- | Encoding monad.
+
+newtype Code a = Code (State PartialBijection a)
+  deriving (Functor, Applicative, Monad)
+
+-- | Decoding monad.
+
+newtype Decode a = Decode (MaybeT Code a)
+  deriving (Functor, Applicative, Alternative, Monad)
+
+-- | Runs a coder.
+--
+-- Note that coding might not give consistent results if you invoke
+-- 'runCode' multiple times. For instance, the following code will
+-- return 'False':
+--
+-- @
+--   runCode (code (parse "Suc(Zero())"))
+--     ==
+--   runCode (do
+--     code (parse "Zero()")
+--     code (parse "Suc(Zero())"))
+-- @
+
+runCode :: Code a -> a
+runCode (Code m) = evalState m (Maps Map.empty Map.empty)
+
+prop_runCode_inconsistent = not $
+  runCode (code (parse "Suc(Zero())"))
+    ==
+  runCode (do
+    code (parse "Zero()")
+    code (parse "Suc(Zero())"))
+
+-- | Runs a decoder. Note that decoders can fail.
+
+runDecode :: Decode a -> Maybe a
+runDecode (Decode m) = runCode (runMaybeT m)
+
+-- | Turns a coder into a decoder.
+--
+-- Example usage:
+--
+-- @
+--   do e <- 'asDecoder' ('code' e)
+--      'decode' (eval ('Apply' selfInterpreter e))
+-- @
+
+asDecoder :: Code a -> Decode a
+asDecoder = Decode . lift
+
+-- | Converts a string to a natural number.
+
+fromString :: String -> Code Natural
+fromString s = do
+  Maps strMap natMap <- Code get
+  case Map.lookup s strMap of
+    Just n  -> return n
+    Nothing -> do
+      let n = fromIntegral $ Map.size strMap
+      Code (put (Maps (Map.insert s n strMap)
+                      (Map.insert n s natMap)))
+      return n
+
+-- | Tries to convert a natural number to a string.
+
+toString :: Natural -> Decode String
+toString n = Decode $ MaybeT $ Code $ do
+  Maps _ natMap <- get
+  return (Map.lookup n natMap)
+
+-- | Encodes strings.
+
+codeString :: String -> Code Exp
+codeString s = fromNatural <$> fromString s
+
+-- | Decodes strings.
+
+decodeString :: Exp -> Decode String
+decodeString e = do
+  n <- Decode (MaybeT (return (toNatural e)))
+  toString n
+
+-- | Encodes variables.
+
+codeVar :: Variable -> Code Exp
+codeVar (Variable s) = codeString s
+
+-- | Decodes variables.
+
+decodeVar :: Exp -> Decode Variable
+decodeVar e = Variable <$> decodeString e
+
+-- | Encodes constructors.
+
+codeCon :: Constructor -> Code Exp
+codeCon (Constructor s) = codeString s
+
+-- | Decodes constructors.
+
+decodeCon :: Exp -> Decode Constructor
+decodeCon e = Constructor <$> decodeString e
+
+-- | Encodes expressions.
+
+code :: Exp -> Code Exp
+code e = case e of
+  Apply e1 e2 -> constr "Apply" [code e1, code e2]
+  Lambda x e  -> constr "Lambda" [codeVar x, code e]
+  Case e bs   -> constr "Case" [code e, codeList codeBr bs]
+  Rec x e     -> constr "Rec" [codeVar x, code e]
+  Var x       -> constr "Var" [codeVar x]
+  Const c es  -> constr "Const" [codeCon c, codeList code es]
+  where
+  constr c args = Const (Constructor c) <$> sequence args
+
+  codeBr :: Br -> Code Exp
+  codeBr (Branch c xs e) =
+    constr "Branch" [codeCon c, codeList codeVar xs, code e]
+
+  codeList :: (a -> Code Exp) -> [a] -> Code Exp
+  codeList r []       = constr "Nil" []
+  codeList r (x : xs) = constr "Cons" [r x, codeList r xs]
+
+-- | Decodes expressions.
+
+decode :: Exp -> Decode Exp
+decode e = case e of
+  Const (Constructor c) args -> case (c, args) of
+    ("Apply", [e1, e2]) -> Apply <$> decode e1 <*> decode e2
+    ("Lambda", [x, e])  -> Lambda <$> decodeVar x <*> decode e
+    ("Case", [e, bs])   -> Case <$> decode e <*> decodeList decodeBr bs
+    ("Rec", [x, e])     -> Rec <$> decodeVar x <*> decode e
+    ("Var", [x])        -> Var <$> decodeVar x
+    ("Const", [c, es])  -> Const <$> decodeCon c
+                                 <*> decodeList decode es
+    _                   -> empty
+  _ -> empty
+  where
+  decodeBr :: Exp -> Decode Br
+  decodeBr (Const (Constructor "Branch") [c, xs, e]) =
+    Branch <$> decodeCon c <*> decodeList decodeVar xs <*> decode e
+  decodeBr _ = empty
+
+  decodeList :: (Exp -> Decode a) -> Exp -> Decode [a]
+  decodeList decode e = case e of
+    Const (Constructor c) args -> case (c, args) of
+      ("Nil", [])       -> return []
+      ("Cons", [x, xs]) -> (:) <$> decode x <*> decodeList decode xs
+
+prop_decode_code e =
+  runDecode (decode =<< asDecoder (code e)) == Just e
+
+-- | An internal implementation of coding.
+--
+-- Example usage:
+--
+-- @
+--   'runCode' $ do
+--     ic <- 'internalCode'
+--     ce <- 'code' e
+--     return (eval ('Apply' ic ce))
+-- @
+
+internalCode :: Code Exp
+internalCode = do
+  bs <- sequence
+          [ branch 0 "Zero"
+          , branch 1 "Suc"
+          , branch 0 "Nil"
+          , branch 2 "Cons"
+          , branch 2 "Apply"
+          , branch 2 "Lambda"
+          , branch 2 "Case"
+          , branch 2 "Rec"
+          , branch 1 "Var"
+          , branch 2 "Const"
+          , branch 3 "Branch"
+          ]
+  return $
+    Rec (Variable "code") $
+      Lambda (Variable "p") $
+        Case (Var (Variable "p")) bs
+  where
+    args = map (Variable . ("x" ++) . show) [(1 :: Integer)..]
+
+    branch n c = do
+      cc <- codeCon (Constructor c)
+      return $
+        Branch (Constructor c) (take n args) $
+          Const (Constructor "Const") $
+            [ cc
+            , foldr (\arg rest ->
+                        Const (Constructor "Cons")
+                          [ Apply (Var (Variable "code")) (Var arg)
+                          , rest
+                          ])
+                    (Const (Constructor "Nil") [])
+                    (take n args)
+            ]
+
+-- The following test case depends on an implementation of evaluation
+-- (eval), and is therefore commented out.
+
+-- prop_internalCode :: Exp -> Bool
+-- prop_internalCode e = runCode $ do
+--   internalCode <- internalCode
+--   ce           <- code e
+--   cce          <- code ce
+--   return $ eval (Apply internalCode ce) == cce
+
+------------------------------------------------------------------------
+-- Functions that can be used to run internal substitution functions
+-- and self-interpreters
+
+-- | Tries to compute the value of the given internal substitution
+-- function applied to the given arguments.
+--
+-- If the application terminates, and the result can be decoded, then
+-- this result is returned.
+--
+-- Example usage:
+--
+-- @
+--   'runInternalSubstitution' eval internalSubst
+--     (Variable "plus") 'add' ('parse' "plus")
+-- @
+
+runInternalSubstitution
+  :: (Exp -> Exp)  -- ^ Evaluation.
+  -> Exp           -- ^ Internal substitution.
+  -> Variable      -- ^ The variable.
+  -> Exp           -- ^ The closed expression that should be
+                   --   substituted for the variable (not in coded
+                   --   form).
+  -> Exp           -- ^ The possibly open expression in which the
+                   --   closed expression should be substituted for
+                   --   the variable (not in coded form).
+  -> Maybe Exp
+runInternalSubstitution eval internalSubst x e e' = runDecode $ do
+  x  <- asDecoder $ codeVar x
+  e  <- asDecoder $ code e
+  e' <- asDecoder $ code e'
+  decode (eval (foldl1 Apply [internalSubst, x, e, e']))
+
+-- | Uses a self-interpreter to evaluate a program applied to some
+-- arguments.
+--
+-- If the self-interpreter terminates, and the result can be decoded,
+-- then this result is returned.
+--
+-- Example usage:
+--
+-- @
+--   do n <- 'runSelfInterpreter' eval selfInterpreter 'add'
+--             ['fromNatural' 2, 'fromNatural' 2]
+--      'toNatural' n
+-- @
+
+runSelfInterpreter
+  :: (Exp -> Exp)  -- ^ An implementation of evaluation.
+  -> Exp           -- ^ The self-interpreter.
+  -> Exp           -- ^ The program to be evaluated (not in coded form).
+  -> [Exp]         -- ^ The program's arguments (not in coded form).
+  -> Maybe Exp
+runSelfInterpreter eval selfInterpreter p args = runDecode $ do
+  term <- asDecoder (code (foldl1 Apply (p : args)))
+  decode (eval (Apply selfInterpreter term))
+
+------------------------------------------------------------------------
+-- Some testing procedures
+
+-- | Tests whether a purported implementation of evaluation can
+-- evaluate addition of two natural numbers ('add') correctly.
+--
+-- The test is, of course, incomplete.
+
+testEvaluation :: (Exp -> Exp) -> IO Bool
+testEvaluation eval =
+  isSuccess <$>
+    quickCheckResult
+      (forAllNatural $ \m ->
+       forAllNatural $ \n ->
+         eval (Apply (Apply add (fromNatural m)) (fromNatural n)) ==
+         fromNatural (m + n))
+
+-- | Tests whether a purported implementation of evaluation and a
+-- purported implementation of multiplication of two natural numbers
+-- are correct.
+--
+-- The test is, of course, incomplete.
+
+testMultiplication
+  :: (Exp -> Exp)  -- ^ Evaluation.
+  -> Exp           -- ^ Multiplication. The program should take two
+                   --   natural numbers as input and produce a natural
+                   --   number as its result.
+  -> IO Bool
+testMultiplication eval mul =
+  isSuccess <$>
+    quickCheckResult
+      (forAllNatural $ \m' ->
+       forAllNatural $ \n' ->
+         let m = m' `div` 2; n = n' `div` 2 in
+         eval (Apply (Apply mul (fromNatural m)) (fromNatural n)) ==
+         fromNatural (m * n))
+
+-- | Tests a purported implementation of substitution.
+--
+-- The substitution operation takes three arguments, @x@, @e@ and
+-- @e'@, where @e@ is closed, and should substitute @e@ for every free
+-- occurrence of @x@ in @e'@.
+--
+-- The test is designed for substitution operations that are
+-- implemented exactly like in the χ specification. In particular, the
+-- substitution operation should not rename any bound variables.
+--
+-- The test is, of course, incomplete.
+
+testSubstitution :: (Variable -> Exp -> Exp -> Exp) -> IO Bool
+testSubstitution subst =
+  isSuccess <$>
+    quickCheckResult
+      (\e' ->
+        forAll closed $ \e ->
+        let fs     = free e'
+            fbs    = fs `Set.intersection` bound e'
+            var ys = elements (Set.toList ys)
+        in
+        (forAll (var (Set.insert (Variable "x") fs)) $ \x ->
+           counterexample' x e e'
+             (\x -> "However, FV e'' /= FV e' - {" ++ x ++ "}.") $
+           free (subst x e e') == Set.delete x fs)
+          .&&.
+        (not (Set.null fs) && not (isVar e) ==>
+         forAll (var fs) $ \x ->
+           counterexample' x e e'
+             (\x ->
+               "However, e'' = e' (which should not hold, because " ++
+               x ++ " is free in e' and e is not a variable).") $
+           subst x e e' /= e')
+          .&&.
+        (not (Set.null fbs) ==>
+         forAll (var fbs) $ \x ->
+           counterexample' x e e'
+             (\x ->
+               "However, bound e'' /= union (bound e) (bound e') " ++
+               "(the two sides should be equal, because " ++ x ++
+               " is free in e' and bound in e).") $
+           bound (subst x e e')
+             ==
+           bound e `Set.union` bound e'))
+  where
+  isVar Var{} = True
+  isVar _     = False
+
+  para = fsep . map text . words
+
+  def s e =
+    nest 2 $ vcat $
+      [text s <+> text "="] ++
+      map (nest (length s + 3) . text) (lines (pretty e))
+
+  counterexample' x e e' s =
+    counterexample $
+    render $ vcat $
+      [ para "This counterexample uses the following values:"
+      , def "e " e
+      , def "e'" e'
+      , para $
+          "Note that e is closed. " ++
+          "Your implementation gives the following value " ++
+          "for e'[" ++ px ++ " <- e]:"
+      , def "e''" (subst x e e')
+      , para (s px)
+      ]
+    where
+    px = pretty (Var x)
+
+-- | Tests if the result of the given internal substitution function
+-- matches that of the given substitution function for given inputs.
+--
+-- Note that no result is returned if some program crashes or fails to
+-- terminate.
+--
+-- Example usage:
+--
+-- @
+--   'testInternalSubstitutionWith' eval subst internalSubst
+--     ('Variable' "plus") 'add' ('parse' "plus")
+-- @
+
+testInternalSubstitutionWith
+  :: (Exp -> Exp)                     -- ^ Evaluation.
+  -> (Variable -> Exp -> Exp -> Exp)  -- ^ Substitution.
+  -> Exp                              -- ^ Internal substitution.
+  -> Variable                         -- ^ The variable.
+  -> Exp                              -- ^ The closed expression that
+                                      --   should be substituted for
+                                      --   the variable (not in coded
+                                      --   form).
+  -> Exp                              -- ^ The possibly open
+                                      --   expression in which the
+                                      --   closed expression should be
+                                      --   substituted for the
+                                      --   variable (not in coded
+                                      --   form).
+  -> Bool
+testInternalSubstitutionWith eval subst internalSubst x e e' =
+  runInternalSubstitution eval internalSubst x e e'
+    ==
+  Just (subst x e e')
+
+-- | Tests whether an implementation of internal substitution matches
+-- an implementation of substitution.
+--
+-- The test is, of course, incomplete.
+
+testInternalSubstitution
+  :: (Exp -> Exp)                     -- ^ Evaluation.
+  -> (Variable -> Exp -> Exp -> Exp)  -- ^ Substitution.
+  -> Exp                              -- ^ Internal substitution.
+  -> IO Bool
+testInternalSubstitution eval subst internalSubst =
+  isSuccess <$>
+    quickCheckResult (\e' ->
+      forAll closed $ \e ->
+      forAll (elements $ Set.toList $
+                Set.insert (Variable "x") $ free e') $ \x ->
+        testInternalSubstitutionWith eval subst internalSubst x e e')
+
+-- | Tests if the result of the given self-interpreter matches that of
+-- the given evaluator for a program applied to some arguments.
+--
+-- Note that no result is returned if some program crashes or fails to
+-- terminate.
+--
+-- Example usage:
+--
+-- @
+--   'testSelfInterpreterWith' eval selfInterpreter 'add'
+--     ['fromNatural' 2, 'fromNatural' 2]
+-- @
+
+testSelfInterpreterWith
+  :: (Exp -> Exp)  -- ^ Evaluation.
+  -> Exp           -- ^ The self-interpreter.
+  -> Exp           -- ^ The program to be evaluated (not in coded form).
+  -> [Exp]         -- ^ The arguments (not in coded form).
+  -> Bool
+testSelfInterpreterWith eval selfInterpreter p args =
+  runSelfInterpreter eval selfInterpreter p args
+    ==
+  Just (eval (foldl1 Apply (p : args)))
+
+-- | Tests whether a purported implementation of evaluation and a
+-- purported self-interpreter are correctly implemented.
+--
+-- The test is, of course, incomplete.
+
+testSelfInterpreter
+  :: (Exp -> Exp)  -- ^ Evaluation.
+  -> Exp           -- ^ The self-interpreter.
+  -> IO Bool
+testSelfInterpreter eval selfInterpreter =
+  isSuccess <$>
+    quickCheckResult
+      (forAllNatural $ \m ->
+        (forAllNatural $ \n ->
+          testSelfInterpreterWith eval selfInterpreter
+            add [fromNatural (m `min` 5), fromNatural (n `min` 5)])
+          .&&.
+        testSelfInterpreterWith eval selfInterpreter
+          add' [fromNatural m])
+  where
+  add' :: Exp
+  add' = parse $ unlines
+    [ "rec add = \\m. case m of"
+    , "  { Zero() -> \\n. n"
+    , "  ; Suc(m) -> \\n. add m Suc(n)"
+    , "  }"
+    ]
+
+-- | Tests whether a purported implementation of evaluation and a
+-- purported Turing machine interpreter are correctly implemented. The
+-- Turing machine interpreter should satisfy the specification given
+-- in Assignment 6.
+--
+-- The test is, of course, incomplete.
+
+testTuringMachineInterpreter
+  :: (Exp -> Exp)  -- ^ Evaluation.
+  -> Exp           -- ^ The Turing machine interpreter.
+  -> IO Bool
+testTuringMachineInterpreter eval tmInterpreter =
+  isSuccess <$>
+    quickCheckWithResult
+      (stdArgs { maxSuccess = 36 })
+      (forAll smallNumber $ \m ->
+       forAll smallNumber $ \n ->
+         eval (foldl1 Apply [ tmInterpreter
+                            , add
+                            , fromList (ones m ++ [0] ++ ones n)
+                            ])
+           ==
+         fromList (ones (m + n)))
+  where
+  smallNumber :: Gen Natural
+  smallNumber = fromInteger <$> choose (0, 5)
+
+  ones :: Natural -> [Natural]
+  ones n = genericReplicate n 1
+
+  fromList :: [Natural] -> Exp
+  fromList []       = Const (Constructor "Nil") []
+  fromList (n : ns) =
+    Const (Constructor "Cons") [fromNatural n, fromList ns]
+
+  add :: Exp
+  add = Const (Constructor "TM") [Const (Constructor "Zero") [],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Zero") [],Const (Constructor "Zero") [],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "R") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Zero") [],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Zero") [],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "R") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Blank") [],Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Zero") []]],Const (Constructor "Blank") [],Const (Constructor "L") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "R") []],Const (Constructor "Cons") [Const (Constructor "Rule") [Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Zero") []]],Const (Constructor "Suc") [Const (Constructor "Zero") []],Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Suc") [Const (Constructor "Zero") []]]],Const (Constructor "Blank") [],Const (Constructor "L") []],Const (Constructor "Nil") []]]]]]]
+
+------------------------------------------------------------------------
+-- Internal tests
+
+return []
+
+-- | Runs all the internal tests.
+
+tests :: IO Bool
+tests = $quickCheckAll
--- a/3/assig.org
+++ b/3/assig.org
@ -0,0 +1,119 @@
+#+title: Assignment 3
+#+options: toc:nil
+#+latex_header: \usepackage{parskip}
+
+* Supporting files
+
+~This~ time you can make use of a [[http://bnfc.digitalgrammars.com/][BNFC]] specification ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) of a variant of the concrete syntax of $\chi$. This grammar gives specific rules for variable and constructor names, and differs from the concrete syntax presented in the lectures in some ways:
+# TODO: Fix '
+- Variables and constructors are sequences of letters (~a~ to ~z~ and ~A~ to ~Z~), digits (~0~ to ~9~), underscores (~_~), dashes (~-~) and primes ('), and variables have to start with lower-case letters or underscores, whereas constructors have to start with upper-case letters.
+- Lambdas are written using backslash characters (~\~) and arrows are written using the string ~->~.
+- End-of-line comments of the form ~-- ...~ are allowed, as are (non-nested) comments of the form ~{- ... -}~.
+- There can be a final comma after a non-empty list of constructor arguments, and there can be a final semicolon after a non-empty list of branches.
+- Parentheses are treated differently. Superfluous parentheses are allowed around expressions. Some parentheses can be omitted; application is treated as a left-associative operation. Note that some grammatically correct expressions actually parse differently with this variant of the grammar, for instance ~(rec x = x y)~ which is interpreted as ~rec x = (x y)~ rather than ~(rec x = x) y~ (which was previously grammatically incorrect). See the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][grammar]] for details.
+
+If you want to use Haskell then there is also a wrapper module ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) that exports the generated abstract syntax and some definitions that may be useful for testing your code ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.html][documentation]]). The wrapper module comes with a Cabal file ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]]) and a [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] file that might make installation a little easier. Here is one way to (hopefully) get started:
+
+- Install all dependencies properly, including suitable versions of GHC and cabal-install ([[https://www.haskell.org/downloads/][installation instructions]]), as well as [[http://bnfc.digitalgrammars.com/][BNFC]].
+- Put [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][~Chi.hs~]], [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/chi.cabal][~chi.cabal~]] and [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/cabal.project][~cabal.project~]] in an otherwise empty directory.
+- Run ~bnfc --haskell Chi.cf~ in that directory.
+    - Now it is hopefully possible to use standard ~cabal~ commands. You could for instance try the following (still in the same directory):
+    - First use cabal repl to start GHCi.
+    - Then issue the following commands at the GHCi command prompt:
+    #+begin_src haskell
+    import Chi
+    import Prelude
+    pretty <$> (runDecode (decode =<<
+                        asDecoder (code =<< code (parse "\\x. x"))))
+    #+end_src
+
+* Exercises
+In order to pass this assignment you have to get at least four points.
+
+Please provide your source code in a form which is easy to test, not, say, a PDF file. Do not submit the files provided on this page or the generated code, only the code that you write.
+
+(Exercises marked with [BN] are based on exercises from a previous version of this course, given by Bengt Nordström.)
+
+** (1p)
+Consider the following $\chi$ program:
+#+begin_src chi 
+rec foo = \m. \n. case m of
+  { Zero() → case n of
+    { Zero() → True()
+    ; Suc(n) → False()
+    }
+  ; Suc(m) → case n of
+    { Zero() → False()
+    ; Suc(n) → foo m n
+    }
+  }
+#+end_src
+Give a high-level explanation of the mathematical function in $\mathbb{N} \rightarrow \mathbb{N} \rightarrow \text{Bool}$ that is implemented by this code.
+
+*** Answer
+The function will check for equality of the two natural numbers. If they are both $Zero()$, then it returns true, and if both are the successor of a some values, it checks if they are equal. In the other cases, it returns false.
+
+** (2p)
+Consider the $\chi$ term /t/ with concrete syntax $C (\lambda z.z)$:
+- Give the abstract syntax corresponding to /t/. Use the abstract syntax presented in the lectures. The answer should be a value in the set /Exp/.
+- Give the concrete syntax of the (standard) $\chi$ representation of /t/.
+- Give the abstract syntax of the (standard) $\chi$ representation of /t/.
+
+In the abstract syntax the constructor ~C~ should be represented by $\underline{C} \in \text{Const}$, and the variable ~z~ by $\underline{z} \in \text{Var}$. When giving the $\chi$ representation of the term you should use (the representation of) the number 0 to represent $\underline{C}$, and 1 to represent $\underline{z}$.
+*** Answer
+The abstract syntax is the following: $\text{const}\ \underline{C}\  (\text{cons}\ (\text{lambda}\ \underline{z}\ (\text{var}\ \underline{z}))\ \text{nil})$.
+
+The concrete syntax of the standard representation is the following: $Const(\ulcorner \underline{C} \urcorner, Cons(Lambda(\ulcorner \underline{z} \urcorner, Cons (Var(\ulcorner \underline{z} \urcorner), Nil())), Nil())$
+# TODO: check parenthesis above
+
+** (2p) [BN]
+
+Implement substitution for $\chi$. The function should take three arguments, a variable, a closed term, and another term, and substitute the first term for every free occurrence of the variable in the second term.
+
+If you use the BNFC specification above and Haskell, then the substitution function should have the following type:
+#+begin_src haskell
+ Variable -> Exp -> Exp -> Exp
+#+end_src
+Test your implementation. Here are some test cases that must work:
+| Variable | Substituted term | Term                                        | Result                                      |
+|----------+------------------+---------------------------------------------+---------------------------------------------|
+| ~x~        | ~Z()~              | ~rec x = x~                                   | ~rec x = x~                                   |
+| ~y~        | $\lambda x.x$          | $\lambda x. (x y)$                                | $\lambda x . (x (\lambda x . x))$                       |
+| ~z~        | $C(\lambda z . z)$     | $\text{case}\ z\ \text{of}\ \{ C(z) \rightarrow z \}$ | $\text{case}\ C(\lambda z. z) \ \text{of}\ \{ C(z) \rightarrow z \}$ |
+
+*** Answer
+
+** (1p)
+Implement multiplication of natural numbers in $\chi$, using the representation of natural numbers given in the $\chi$ specification.
+
+Hint: If you want to make use of addition in the implementation of multiplication, then you can define multiplication using a free variable ~add~, and use the substitution operation from the previous exercise to substitute a complete (closed) implementation of addition for this variable.
+
+*** Answer
+
+** (2p) [BN]
+Implement an interpreter for $\chi$. The interpreter should be a partial function from closed terms to values, and should implement the operational semantics of $\chi$.
+
+If you use the BNFC specification above and Haskell, then the interpreter should have the following type:
+#+begin_src haskell
+ Exp -> Exp
+#+end_src
+
+Test your implementation, for instance by testing that addition (defined in the [[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.hs][wrapper module]]) works for some inputs. If addition doesn’t work when your code is tested, then your solution will not be accepted. Also make sure that the following examples are implemented correctly:
+
+- The following programs should fail to terminate:
+    + $C() C()$
+    + $case \lambda x.x of {}$
+    + $case C() of { C(x) \rightarrow C() }$
+    + $case C(C()) of { C() \rightarrow C() }$
+    + $case C(C()) of { C() \rightarrow C(); C(x) \rightarrow x }$
+    + $case C() of { D() \rightarrow D() }$
+    + $(\lambda x.\lambda y.x) (rec x = x)$
+- The following programs should terminate with specific results:
+    + The program $case C(D(),E()) of { C(x, x) \rightarrow x }$ should terminate with the value $E()$.
+    + The program $case C(\lambda x.x, Zero()) of { C(f, x) \rightarrow f x }$ should terminate with the value $Zero()$.
+    + The program $case (\lambda x.x) C() of { C() \rightarrow C() }$ should terminate with the value $C()$.
+    + The program $((\lambda x.x)(\lambda x.x))(\lambda x.x)$ should terminate with the value $\lambda x.x$.
+
+Note that implementing a call-by-value semantics properly in a language like Haskell, which is by default non-strict, can be tricky. However, you will not fail if the only problem with your implementation is that some programs that should fail to terminate instead terminate with a “reasonable” result.
+
+*** Answer
--- a/3/cabal.project
+++ b/3/cabal.project
@ -0,0 +1,2 @@
+packages:
+  chi.cabal
--- a/3/chi.cabal
+++ b/3/chi.cabal
@ -0,0 +1,28 @@
+cabal-version: 2.0
+name:          chi
+version:       0.1.0
+build-type:    Simple
+
+library
+  default-language:
+    Haskell2010
+  build-depends:
+    array ^>= 0.5.4.0,
+    base >= 4.15 && < 4.22,
+    hashable >= 1.4.7.0 && < 1.6,
+    mtl >= 2.2.2 && < 2.4,
+    pretty ^>= 1.1.3.6,
+    QuickCheck ^>= 2.15.0.0,
+    transformers >= 0.5.6.2 && < 0.7,
+    unordered-containers ^>= 0.2.20
+  build-tool-depends:
+    alex:alex ^>= 3.5.2.0,
+    happy:happy ^>= 2.1.5
+  exposed-modules:
+    AbsChi
+    Chi
+    LexChi
+    ParChi
+    PrintChi
+  hs-source-dirs:
+    .
--- a/3/flake.lock
+++ b/3/flake.lock
@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1763283776,
+        "narHash": "sha256-Y7TDFPK4GlqrKrivOcsHG8xSGqQx3A6c+i7novT85Uk=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "50a96edd8d0db6cc8db57dab6bb6d6ee1f3dc49a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
--- a/3/flake.nix
+++ b/3/flake.nix
@ -0,0 +1,89 @@
+{
+  description = "χ ^^";
+
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+
+  nixConfig.allow-import-from-derivation = true; # cabal2nix uses IFD
+
+  outputs = { self, nixpkgs, flake-utils }:
+    let
+      ghcVer = "ghc910";
+      makeHaskellOverlay = overlay: final: prev: {
+        haskell = prev.haskell // {
+          packages = prev.haskell.packages // {
+            ${ghcVer} = prev.haskell.packages."${ghcVer}".override (oldArgs: {
+              overrides =
+                prev.lib.composeExtensions (oldArgs.overrides or (_: _: { }))
+                  (overlay prev);
+            });
+          };
+        };
+      };
+
+      out = system:
+        let
+          pkgs = import nixpkgs {
+            inherit system;
+            overlays = [ self.overlays.default ];
+            config.allowBroken = true;
+          };
+
+        in
+        {
+          packages = rec {
+            default = chi;
+            chi = pkgs.haskell.packages.${ghcVer}.chi;
+          };
+
+          checks = {
+            inherit (self.packages.${system}) chi;
+          };
+
+          # for debugging
+          # inherit pkgs;
+
+          devShells.default =
+            let haskellPackages = pkgs.haskell.packages.${ghcVer};
+            in
+            haskellPackages.shellFor {
+              packages = p: [ self.packages.${system}.chi ];
+              withHoogle = true;
+              buildInputs =
+                (with pkgs; [
+                  gnumake
+                  jasmin
+                  jre_minimal
+                ]) ++
+                (with haskellPackages; [
+                  haskell-language-server
+                  cabal-install
+                  alex
+                  happy
+                  BNFC
+                ]);
+              # Change the prompt to show that you are in a devShell
+              # shellHook = "export PS1='\\e[1;34mdev > \\e[0m'";
+            };
+        };
+    in
+    flake-utils.lib.eachDefaultSystem out // {
+      # this stuff is *not* per-system
+      overlays = {
+        default = makeHaskellOverlay (prev: hfinal: hprev:
+          let hlib = prev.haskell.lib; in
+          {
+            chi = hprev.callCabal2nix "chi" ./. { };
+
+            # here's how to do hacks to the package set
+            # don't run the test suite
+            # fast-tags = hlib.dontCheck hprev.fast-tags;
+            #
+            # don't check version bounds
+            # friendly = hlib.doJailbreak hprev.friendly;
+          });
+      };
+    };
+}