Gemini 2.5 Pro-Exp vibecoded some constructive mu-calculus

CMC.hs

{-# LANGUAGE OverloadedStrings #-}

module CMC (
  -- * Types
  Name,
  Formula(..),
  -- * Querying
  freeFVars,
  -- * Operations
  lift,
  substFVar,
  instantiate,
  unfoldMu,
  unfoldNu,
  -- * Helper (for creating terms)
  nu, mu
) where

import qualified Data.Text as T
import Data.Text (Text)
import qualified Data.Set as Set
import Data.Set (Set)
import Data.List (elemIndex) -- Used only for Show instance
import Prettyprinter

-- | Type alias for variable names (free variables and proposition names).
type Name = Text

-- | Represents formulas in the constructive modal mu-calculus (Locally Nameless).
data Formula
  = PropVar Name       -- ^ Propositional variables (atomic facts, e.g., p)
  | FVar Name          -- ^ Free formula variables (placeholders, e.g., X)
  | BVar Int           -- ^ Bound formula variables (de Bruijn index, #0, #1, ...)
  | Truth              -- ^ Top (True, ⊤)
  | Falsity            -- ^ Bottom (False, ⊥)
  | Conj Formula Formula -- ^ Conjunction (A ∧ B)
  | Disj Formula Formula -- ^ Disjunction (A ∨ B)
  | Impl Formula Formula -- ^ Implication (A → B)
  | Box Formula        -- ^ Box modality (□ A)
  | Diamond Formula    -- ^ Diamond modality (◇ A)
  | Mu Formula         -- ^ Least fixed point (μ. A). BVar 0 in A refers to this binding.
  | Nu Formula         -- ^ Greatest fixed point (ν. A). BVar 0 in A refers to this binding.
  deriving (Eq, Ord) -- Ord needed for Set

-- | Calculate the set of free *formula* variables (FVars) in a formula.
freeFVars :: Formula -> Set Name
freeFVars = go
  where
    go f = case f of
      FVar name    -> Set.singleton name
      BVar _       -> Set.empty
      PropVar _    -> Set.empty
      Truth        -> Set.empty
      Falsity      -> Set.empty
      Conj f1 f2   -> go f1 `Set.union` go f2
      Disj f1 f2   -> go f1 `Set.union` go f2
      Impl f1 f2   -> go f1 `Set.union` go f2
      Box f1       -> go f1
      Diamond f1   -> go f1
      Mu body'     -> go body' -- Binders don't affect free variables by name
      Nu body'     -> go body'

-- | lift k c formula: Add 'k' to indices of bound variables >= 'c'.
--   This is used to adjust indices when moving a term *under* 'k' new binders,
--   avoiding capture of variables bound *outside* the current context (>= 'c').
lift :: Int -> Int -> Formula -> Formula
lift k = go
  where
    go c f = case f of
      BVar i       -> if i >= c then BVar (i + k) else BVar i
      FVar name    -> FVar name
      PropVar name -> PropVar name
      Truth        -> Truth
      Falsity      -> Falsity
      Conj f1 f2   -> Conj (go c f1) (go c f2)
      Disj f1 f2   -> Disj (go c f1) (go c f2)
      Impl f1 f2   -> Impl (go c f1) (go c f2)
      Box f1       -> Box (go c f1)
      Diamond f1   -> Diamond (go c f1)
      -- When going under a binder, increment the cutoff 'c'
      Mu body'     -> Mu (go (c + 1) body')
      Nu body'     -> Nu (go (c + 1) body')

-- | substFVar name sub target: Substitute 'sub' for FVar 'name' in 'target'.
--   Capture-avoiding substitution for *free* variables.
substFVar :: Name -> Formula -> Formula -> Formula
substFVar name sub = go 0
  where
    -- 'c' tracks the number of binders we are currently under in 'target'
    go c f = case f of
      FVar v -> if v == name
                -- Found the free var: substitute 'sub', lifting it by 'c' levels
                -- to account for the binders we passed through in 'target'.
                then lift c 0 sub
                else FVar v
      BVar i -> BVar i -- Bound variables are unaffected by free var substitution
      PropVar p -> PropVar p
      Truth -> Truth
      Falsity -> Falsity
      Conj f1 f2 -> Conj (go c f1) (go c f2)
      Disj f1 f2 -> Disj (go c f1) (go c f2)
      Impl f1 f2 -> Impl (go c f1) (go c f2)
      Box f1 -> Box (go c f1)
      Diamond f1 -> Diamond (go c f1)
      -- Increase depth 'c' when going under a binder
      Mu body' -> Mu (go (c + 1) body')
      Nu body' -> Nu (go (c + 1) body')

-- | instantiate sub body: Replaces BVar 0 in 'body' with 'sub', adjusting indices.
--   This performs the core step of substituting a term for the variable bound
--   by the innermost binder. It's used for unfolding fixed points.
instantiate :: Formula -> Formula -> Formula
instantiate sub = go 0
  where
    -- 'c' tracks the current binding depth within 'body'
    go c f = case f of
      BVar i
        | i == c    -> lift c 0 sub -- Found BVar 0 relative to depth 'c', substitute & lift 'sub'
        | i > c     -> BVar (i - 1) -- Bound var referred outside this scope; decrement index
        | otherwise -> BVar i       -- Bound var refers inside this scope (i < c); leave index
      FVar name -> FVar name
      PropVar name -> PropVar name
      Truth -> Truth
      Falsity -> Falsity
      Conj f1 f2 -> Conj (go c f1) (go c f2)
      Disj f1 f2 -> Disj (go c f1) (go c f2)
      Impl f1 f2 -> Impl (go c f1) (go c f2)
      Box f1 -> Box (go c f1)
      Diamond f1 -> Diamond (go c f1)
      -- Increase depth 'c' when going under a binder
      Mu body' -> Mu (go (c + 1) body')
      Nu body' -> Nu (go (c + 1) body')

-- | Unfolds a least fixed point one step: unfoldMu (μ.A) = A[μ.A / #0]
unfoldMu :: Formula -> Formula
unfoldMu formula = case formula of
  Mu body -> instantiate formula body -- Substitute the whole formula for BVar 0 in the body
  _       -> error "unfoldMu called on non-Mu formula"

-- | Unfolds a greatest fixed point one step: unfoldNu (ν.A) = A[ν.A / #0]
unfoldNu :: Formula -> Formula
unfoldNu formula = case formula of
  Nu body -> instantiate formula body -- Substitute the whole formula for BVar 0 in the body
  _       -> error "unfoldNu called on non-Nu formula"


-- == Pretty Printing (more complex with names for bound vars) ==

findFreshName :: Set Name -> Name
findFreshName used = head $ filter (`Set.notMember` used) baseNames
  where baseNames = map T.pack $ ["X", "Y", "Z"] ++ [ l : show i | i <- [0..], l <- ['X', 'Y', 'Z'] ]

-- | Pretty-print a Formula using the prettyprinter library.
--   Use this function or the Pretty instance.
prettyDoc :: Formula -> Doc ann
prettyDoc = prettyPrec 0 [] -- Start with lowest precedence (0) and empty context

-- | Pretty-print with precedence and context for bound variable names.
prettyPrec :: Int       -- ^ Outer precedence level
           -> [Name]    -- ^ Context mapping BVar indices to names (innermost is head)
           -> Formula   -- ^ Formula to print
           -> Doc ann
prettyPrec d ctx f = maybeParens $ -- Add parens if needed based on precedence
  case f of
    PropVar name -> pretty name
    FVar name    -> pretty name
    BVar i       -> if i < length ctx
                    then pretty (ctx !! i)            -- Use name from context
                    else pretty ("#" <> T.pack (show i)) -- Fallback (shouldn't happen often)
    Truth        -> pretty '⊤'
    Falsity      -> pretty '⊥'
    Conj f1 f2   -> prettyPrec precConj ctx f1 <+> pretty '∧' <+> prettyPrec precConj ctx f2
    Disj f1 f2   -> prettyPrec precDisj ctx f1 <+> pretty '∨' <+> prettyPrec precDisj ctx f2
    Impl f1 f2   -> prettyPrec precImpl ctx f1 <+> pretty '→' <+> prettyPrec (precImpl - 1) ctx f2 -- Right associative
    Box f1       -> pretty '□' <+> prettyPrec precPrefix ctx f1
    Diamond f1   -> pretty '◇' <+> prettyPrec precPrefix ctx f1
    Mu body'     ->
      let fvBody = freeFVars body'
          usedNames = Set.fromList ctx `Set.union` fvBody
          varName = findFreshName usedNames
          newCtx = varName : ctx
      -- Nicer layout for binders using nest and group
      in group $ nest 2 (pretty 'μ' <> pretty varName <> dot <> line <> prettyPrec 0 newCtx body')
         -- Simpler alternative (single line):
         -- pretty 'μ' <> pretty varName <> dot <+> prettyPrec 0 newCtx body'
    Nu body'     ->
      let fvBody = freeFVars body'
          usedNames = Set.fromList ctx `Set.union` fvBody
          varName = findFreshName usedNames
          newCtx = varName : ctx
      -- Nicer layout for binders using nest and group
      in group $ nest 2 (pretty 'ν' <> pretty varName <> dot <> line <> prettyPrec 0 newCtx body')
         -- Simpler alternative (single line):
         -- pretty 'ν' <> pretty varName <> dot <+> prettyPrec 0 newCtx body'

  where
    -- Define operator precedences (adjust if needed)
    precConj   = 3
    precDisj   = 2
    precImpl   = 1
    precPrefix = 9 -- Higher than infix
    precAtom   = 10 -- Higher than prefix

    -- Determine the precedence of the current formula node
    currentPrec = case f of
      Conj {}   -> precConj
      Disj {}   -> precDisj
      Impl {}   -> precImpl
      Box {}    -> precPrefix
      Diamond {}-> precPrefix
      Mu {}     -> 0 -- Binders have low precedence
      Nu {}     -> 0
      _         -> precAtom -- Vars, constants have highest precedence

    -- Add parentheses if outer precedence `d` > current precedence
    maybeParens :: Doc ann -> Doc ann
    maybeParens doc = if d > currentPrec then parens doc else doc

-- Make Formula an instance of the Pretty class
instance Pretty Formula where
  pretty = prettyDoc

-- == Helpers for constructing terms ==
-- These abstract over a variable name and place BVar 0 in the body

abstract :: Name -> Formula -> Formula
abstract name = go 0
  where
    go c f = case f of
      FVar v -> if v == name then BVar c else FVar v
      BVar i -> BVar i -- Assuming no shadowed bound vars during construction, should be fine
      PropVar p -> PropVar p
      Truth -> Truth
      Falsity -> Falsity
      Conj f1 f2 -> Conj (go c f1) (go c f2)
      Disj f1 f2 -> Disj (go c f1) (go c f2)
      Impl f1 f2 -> Impl (go c f1) (go c f2)
      Box f1 -> Box (go c f1)
      Diamond f1 -> Diamond (go c f1)
      Mu body' -> Mu (go (c + 1) body') -- Important: increase depth
      Nu body' -> Nu (go (c + 1) body') -- Important: increase depth

-- | Smart constructor for Mu that abstracts a free variable name.
--   `mu "X" body` creates `μ. A` where A is `body` with `FVar "X"` replaced by `BVar 0`.
mu :: Name -> Formula -> Formula
mu name body = Mu (abstract name body)

-- | Smart constructor for Nu that abstracts a free variable name.
--   `nu "Y" body` creates `ν. A` where A is `body` with `FVar "Y"` replaced by `BVar 0`.
nu :: Name -> Formula -> Formula
nu name body = Nu (abstract name body)

out.txt

Formula 1: μX. p ∨ ◇ X
Unfolding 1: p ∨ ◇ (μX. p ∨ ◇ X)
Free vars F1: []
Free vars Unfolding 1: []

Formula 2: νX. p ∧ □ X
Unfolding 2: p ∧ □ (νX. p ∧ □ X)
Free vars F2: []
Free vars Unfolding 2: []

Formula 3 (free Y): μX. X ∧ Y
Substituted Y->q in F3: μX. X ∧ q
Free vars F3: [Y]
Free vars Substituted F3: []

Term (mu Z. (Z and X)): μY. Y ∧ X
Subst X->Z in term: μX. X ∧ Z
Free vars trickySub: [Z]