Pure Haskell Evaluator for Interaction Calculus

Source:https://chatgpt.com/share/67a15a00-b670-8004-a5d1-552bc9ff2778

Below is a complete Haskell file that implements an Interaction Calculus evaluator in a pure style. The evaluator uses a global substitution map (variables are “pointers” updated in O(1) time) and a state monad to track both the substitution map and a fresh variable counter as well as an interaction‐step counter. (Comments indicate which rule is being applied.) You can compile this file (say, as IC.hs) and run it with a term passed as a command‐line argument.Below is the full code:

haskell

{-# LANGUAGE OverloadedStrings #-} module Main where import Control.Monad.State import qualified Data.Map as Map import Data.Map (Map) import System.Environment (getArgs) import Data.Char (isSpace, isAlpha, isDigit) -------------------------------------------------------------------------------- -- Data Types and Global State -------------------------------------------------------------------------------- type Name = String type Label = String -- | The syntax of Interaction Calculus terms. data Term = Var Name -- ^ Variable (global; substitution via global map) | Lam Name Term -- ^ Lambda abstraction: λx. term | App Term Term -- ^ Application: (f a) | Sup Label Term Term -- ^ Superposition (dual of dup): !K{u v} | Dup Label Name Name Term Term -- ^ Duplication: dup #K {p q} = t; body -- (duplicates term t for use in body, binding names p and q) deriving (Eq) -- Pretty printing of terms in a clear IC syntax. showTerm :: Term -> String showTerm term = case term of Var x -> x Lam x t -> "λ" ++ x ++ " " ++ showTermParen t App t1 t2 -> "(" ++ showTerm t1 ++ " " ++ showTerm t2 ++ ")" Sup l t1 t2 -> "!" ++ l ++ "{" ++ showTerm t1 ++ " " ++ showTerm t2 ++ "}" Dup l p q t body -> "dup #" ++ l ++ " {" ++ p ++ " " ++ q ++ "} = " ++ showTerm t ++ "; " ++ showTerm body where showTermParen t@(Lam _ _) = "(" ++ showTerm t ++ ")" showTermParen t@(Dup _ _ _ _ _) = "(" ++ showTerm t ++ ")" showTermParen t = showTerm t -------------------------------------------------------------------------------- -- Evaluation State and Helpers -------------------------------------------------------------------------------- -- | Global substitution map from names to Terms. type SubstMap = Map Name Term -- | The evaluation state tracks: -- - subs: the global substitution map (each binding is a constant-time pointer update) -- - fresh: counter to generate fresh variable names -- - steps: count of interactions performed. data EvalState = EvalState { subs :: SubstMap , fresh :: Int , steps :: Int } deriving (Show) type Eval a = State EvalState a -- | Generate a fresh variable name by appending the fresh counter to the base. freshVar :: Name -> Eval Name freshVar base = do st st { steps = steps st + 1 } -------------------------------------------------------------------------------- -- Evaluation: Weak Head Normal Form (wnf) and Full Normalization -------------------------------------------------------------------------------- -- | wnf reduces a term to weak head normal form by performing a single -- interaction at the head (if possible). It uses the global substitution map. wnf :: Term -> Eval Term wnf term = case term of -- Variables: look up in the global substitution map. Var x -> do sMap return (Var x) Just term' -> wnf term' -- follow pointer (one substitution step) -- Lambda abstraction is already a WHNF. Lam x t -> return (Lam x t) -- Superposition is a value. Sup l u v -> return (Sup l u v) -- Application: can trigger APP-LAM or APP-SUP. App f a -> do f' do incSteps modify $ \st -> st { subs = Map.insert x a (subs st) } wnf t -- APP-SUP: (!K{u v}) a → create a dup node to split a. Sup k u v -> do incSteps x0 return (App f' a) -- Duplication: try to interact with the target term. Dup k p q t body -> do t' do incSteps -- Create fresh names for splitting the lambda's parameter. x0 st { subs = Map.insert p (Lam x0 (Var r)) (Map.insert q (Lam x1 (Var s)) (Map.insert x (Sup k (Var x0) (Var x1)) (subs st))) } -- Now build a new duplicator to split f into r and s. let newDup = Dup k r s f body wnf newDup -- DUP-SUP: dup #k {p q} = !j{r s}; body Sup j r s -> do incSteps if k == j then do -- Labels match: simply substitute p with r and q with s. modify $ \st -> st { subs = Map.insert p r (Map.insert q s (subs st)) } wnf body else do -- Labels differ: commute the duplicator. a0 st { subs = Map.insert p (Sup j (Var a0) (Var a1)) (Map.insert q (Sup j (Var b0) (Var b1)) (subs st)) } -- Build new duplicators to push the dup into r and s. let dupR = Dup k a0 a1 r (Var "_") -- placeholder continuation let dupS = Dup k b0 b1 s body -- We “chain” the two by replacing the placeholder. let dupR' = case dupR of Dup kk aa0 aa1 rr (Var "_") -> Dup kk aa0 aa1 rr dupS _ -> dupR wnf dupR' -- Otherwise, if t' is not a lambda or superposition, no interaction occurs. _ -> return (Dup k p q t' body) -- | Recursively normalize a term by reducing its head and then normalizing its subterms. normalize :: Term -> Eval Term normalize term = do t do body' do f' do u' do t'' return (Var x) -------------------------------------------------------------------------------- -- Simple Parser (for demonstration purposes) -------------------------------------------------------------------------------- -- Note: This parser is minimal and expects a very “regular” input. -- For example, use the following syntax: -- λx . term -- (term term) -- !K{ term term } for superpositions (K is a label) -- dup #K { p q } = term ; term -- Variables are sequences of letters/digits/underscores. -- | Parse a term from a string. parseTerm :: String -> Either String Term parseTerm s = case parseExpr (dropSpaces s) of Just (t, rest) | all isSpace rest -> Right t | otherwise -> Left $ "Leftover input: " ++ rest Nothing -> Left "Parse error." -- | Parse an expression along with the remaining string. parseExpr :: String -> Maybe (Term, String) parseExpr s0 = parseLambda s0 parseDup s0 parseSuper s0 parseAppOrVar s0 -- | Try parsing a lambda abstraction. parseLambda :: String -> Maybe (Term, String) parseLambda ('λ':cs) = let (var, cs1) = span isIdentChar (dropSpaces cs) cs2 = dropSpaces cs1 in case cs2 of ('.':rest) -> do (body, rest') Nothing parseLambda _ = Nothing -- | Try parsing a dup node. parseDup :: String -> Maybe (Term, String) parseDup s = case stripPrefix "dup" s of Just rest1 -> let rest2 = dropSpaces rest1 in case stripPrefix "#" rest2 of Just rest3 -> let (label, rest4) = span isIdentChar rest3 rest5 = dropSpaces rest4 in case stripPrefix "{" rest5 of Just rest6 -> let (p, rest7) = span isIdentChar (dropSpaces rest6) rest8 = dropSpaces rest7 (q, rest9) = span isIdentChar rest8 rest10 = dropSpaces rest9 in case stripPrefix "}" rest10 of Just rest11 -> let rest12 = dropSpaces rest11 in case stripPrefix "=" rest12 of Just rest13 -> do (t, rest14) do (body, rest17) Nothing Nothing -> Nothing Nothing -> Nothing Nothing -> Nothing Nothing -> Nothing Nothing -> Nothing -- | Try parsing a superposition. parseSuper :: String -> Maybe (Term, String) parseSuper s = case stripPrefix "!" s of Just rest1 -> let (label, rest2) = span isIdentChar (dropSpaces rest1) rest3 = dropSpaces rest2 in case stripPrefix "{" rest3 of Just rest4 -> do (t1, rest5) return (Sup label t1 t2, rest8) Nothing -> Nothing Nothing -> Nothing Nothing -> Nothing -- | Parse either an application or a variable/parenthesized expression. parseAppOrVar :: String -> Maybe (Term, String) parseAppOrVar s = case s of ('(':_) -> parseParens s _ -> parseVar s -- | Parse a parenthesized expression or an application. parseParens :: String -> Maybe (Term, String) parseParens ('(':cs) = do (t, rest) -- Check for application following the paren. let rest3 = dropSpaces rest2 in case parseExpr rest3 of Just (t2, rest4) -> return (App t t2, rest4) Nothing -> return (t, rest2) _ -> Nothing parseParens _ = Nothing -- | Parse a variable (identifier). parseVar :: String -> Maybe (Term, String) parseVar s = let (var, rest) = span isIdentChar s in if null var then Nothing else Just (Var var, rest) -- | Helpers for parsing. dropSpaces :: String -> String dropSpaces = dropWhile isSpace isIdentChar :: Char -> Bool isIdentChar c = isAlpha c || isDigit c || c == '_' -- | Helper: like Data.List.stripPrefix. stripPrefix :: String -> String -> Maybe String stripPrefix [] ys = Just ys stripPrefix (x:xs) (y:ys) | x == y = stripPrefix xs ys stripPrefix _ _ = Nothing -- | Alternative choice combinator. infixr 3 () :: Maybe a -> Maybe a -> Maybe a Nothing r = r l _ = l -------------------------------------------------------------------------------- -- Main: Parse input, run evaluation, and print result and interaction count. -------------------------------------------------------------------------------- main :: IO () main = do args case parseTerm input of Left err -> putStrLn ("Parse error: " ++ err) Right termAst -> do let initState = EvalState { subs = Map.empty, fresh = 0, steps = 0 } (normTerm, finalState) = runState (normalize termAst) initState putStrLn (showTerm normTerm) putStrLn ("Interactions: " ++ show (steps finalState)) _ -> putStrLn "Usage: ./ic \"\""

Explanation

  • Data Types & Pretty–printing:
    The Term data type captures variables, lambdas, applications, superpositions (written as !K{u v}), and duplicators (written as dup #K {p q} = t; body). The showTerm function converts our AST back into a human–readable IC term.

  • Global Substitution Map & EvalState:
    The EvalState record holds the global substitution map (subs), a counter for fresh variable names (fresh), and a counter for the number of interactions (steps). The freshVar function generates fresh names.

  • Evaluation Functions (wnf and normalize):
    The wnf function examines the head of the term and applies one of the interaction rules in O(1) time by updating the substitution map or creating new nodes:

  • APP-LAM: When the head is a lambda, the argument is “substituted” by a map update.

  • APP-SUP: When the head is a superposition, a new duplicator is built to split the argument.

  • DUP-LAM: When duplicating a lambda, fresh names are generated and the substitution map is updated.

  • DUP-SUP: When a duplicator meets a superposition, either a direct substitution (if labels match) or a commutation (if they don’t) is performed. The normalize function recursively applies wnf to ensure that all parts of the term are reduced.

  • Parsing:
    A simple parser is provided that accepts input using the following syntax:

  • Lambda: λx . term

  • Application: (term term)

  • Superposition: !K{ term term }

  • Duplication: dup #K { p q } = term ; term
    (Variables are sequences of letters, digits, or underscores.)
    This parser is minimal and meant only as a demonstration.

  • Main Function:
    The program expects a single command–line argument (the IC term), parses it, runs the normalization (tracking interactions in the process), and then prints the resulting normal form and the total interaction count. Compile this file (for example, with ghc --make IC.hs) and run it with a term string such as:

bash

./ic "((λf . (λx . (!f{ (f x) }))) (λy . y))"

(The exact syntax must match the parser’s expectations.) The evaluator will print the normalized term followed by a line like Interactions: 7.This implementation uses global substitutions and fresh variable generation to ensure that each interaction rule runs in constant time, capturing the essential idea of the Interaction Calculus distinct from traditional lambda–calculus evaluators.