# Judgements

So far we’ve developed a grammar of expressions and a grammar of types and implemented a version of the Hindley-Milner type inference algorithm. Our goal is to use this as the object language for a natural deduction system so we can write machine-checked proofs about lambda calculus expressions. To that end, in this module we’ll develop yet another grammar – a grammar of judgements. These will be the atoms of logical proofs.

As usual we start with some module imports.

{-# LANGUAGE LambdaCase, FlexibleInstances, BangPatterns #-}
module Jud where

( ap, foldM )
import qualified Data.Map as M
( elems, keysSet, filter, lookup )
import Data.Proxy
( Proxy(..) )
import qualified Data.Set as S
( Set(), insert, fromList, member, disjoint, delete, toList
, empty, singleton, unions, union, difference, intersection )
import Test.QuickCheck
( Arbitrary(..), Gen, getSize, elements, oneof, listOf1 )

import Var
import Sub
import Expr
import Type
import Infer

## Judgements

A judgement is a statement which may be supported by evidence. What evidence means here is very narrow: an inference rule counts as evidence, as do assumptions made in the course of writing a proof. We’ll get to evidence later though; first we need a concrete grammar of judgements.

Our judgements will be built from nine basic parts. (We can ignore the Loc parameter for now; these will be used later.)

First we have the basic logical connectives; variables, negation, conjunction, disjunction, implication, and equivalence. These have the usual meaning.

data Jud
= JVar Loc (Var Jud) (Sub Expr)
| JNeg Loc Jud
| JConj Loc Jud Jud
| JDisj Loc Jud Jud
| JImpl Loc Jud Jud
| JEqui Loc Jud Jud

Next we have three connectives involving expressions.

  | JEq Loc Expr Expr
| JIs Loc [Expr] String
| JAll Loc (Var Expr) Jud
| JSome Loc (Var Expr) Jud
deriving (Show)

Equals represents the statement that two expressions have the same “value”, whatever that means. We can interpret this judgement as a rewrite rule – the left hand side of an equation can be rewritten to the right hand side, and vice versa.

The is connective will be used to wrap complicated statements behind a name, like injective. It will have no introduction or elimination rules, and can only be introduced in a definition.

The universal connective represents a judgement within which one expression variable is explicitly quantified with for all; the existential connective represents an expression quantified with there exists.

We haven’t derived an Eq instance for Judgements because we need it to account for renamings of the variable bound by foralls and there existss.

Here’s an Arbitrary instance for judgements analogous to the ones for Expr and MonoType.

instance Arbitrary Jud where
arbitrary = getSize >>= genDepth
where
genDepth :: Int -> Gen Jud
genDepth k
| k <= 0 = oneof
[ JVar <$> arbitrary <*> arbitrary <*> (return emptySub) , JIs <$> arbitrary <*> arbitrary
<*> (listOf1 $elements _is_chars) ] | otherwise = do let recur = genDepth =<< elements [0..(k-1)] oneof [ JNeg <$> arbitrary <*> recur
, JConj <$> arbitrary <*> recur <*> recur , JDisj <$> arbitrary <*> recur <*> recur
, JImpl <$> arbitrary <*> recur <*> recur , JEqui <$> arbitrary <*> recur <*> recur
, JEq <$> arbitrary <*> arbitrary <*> arbitrary , JAll <$> arbitrary <*> arbitrary <*> recur
, JSome <$> arbitrary <*> arbitrary <*> recur ] shrink = \case JVar _ _ _ -> [] JNeg loc q -> q : map (JNeg loc) (shrink q) JConj loc q1 q2 -> [ q1, q2 ] ++ shrink2 (JConj loc) q1 q2 JDisj loc q1 q2 -> [ q1, q2 ] ++ shrink2 (JDisj loc) q1 q2 JImpl loc q1 q2 -> [ q1, q2 ] ++ shrink2 (JImpl loc) q1 q2 JEqui loc q1 q2 -> [ q1, q2 ] ++ shrink2 (JEqui loc) q1 q2 JEq loc e1 e2 -> shrink2 (JEq loc) e1 e2 JIs _ _ _ -> [] JAll loc x q -> q : map (JAll loc x) (shrink q) JSome loc x q -> q : map (JSome loc x) (shrink q) where shrink2 f a b = [ f u v | u <- shrink a, v <- shrink b ] ++ [ f u b | u <- shrink a ] ++ [ f a v | v <- shrink b ] _is_chars = "abcdefghijklmnopqrstuvwxyz0123456789-_" instance Arbitrary (Var Jud) where arbitrary = do let makeVar i = Var$ 'Q' : show i
k <- getSize
makeVar <$> elements [0..k] Every judgement has a (possibly empty) set of free expression variables. Variables can only become bound via the JAll rule. freeExprVarsJ :: Jud -> S.Set (Var Expr) freeExprVarsJ = \case JVar !loc _ _ -> S.empty JNeg !loc p -> freeExprVarsJ p JConj !loc p q -> S.union (freeExprVarsJ p) (freeExprVarsJ q) JDisj !loc p q -> S.union (freeExprVarsJ p) (freeExprVarsJ q) JImpl !loc p q -> S.union (freeExprVarsJ p) (freeExprVarsJ q) JEqui !loc p q -> S.union (freeExprVarsJ p) (freeExprVarsJ q) JEq !loc e f -> S.union (freeExprVars e) (freeExprVars f) JIs !loc es _ -> S.unions$ map freeExprVars es

JAll !loc x q ->
S.difference (freeExprVarsJ q) (S.singleton x)
JSome !loc x q ->
S.difference (freeExprVarsJ q) (S.singleton x)

We need to be able to rename free expressions variables in a capture-avoiding way. As with expressions, this will generally change the meaning of a judgement but is useful as an intermediate step in computing alpha equivalence.

renameFreeJ :: (Var Expr, Var Expr) -> Jud -> Jud
renameFreeJ (u,v) = \case
JVar !loc x s ->
JVar loc x s
JNeg !loc p ->
JNeg loc (renameFreeJ (u,v) p)
JConj !loc p q ->
JConj loc (renameFreeJ (u,v) p) (renameFreeJ (u,v) q)
JDisj !loc p q ->
JDisj loc (renameFreeJ (u,v) p) (renameFreeJ (u,v) q)
JImpl !loc p q ->
JImpl loc (renameFreeJ (u,v) p) (renameFreeJ (u,v) q)
JEqui !loc p q ->
JEqui loc (renameFreeJ (u,v) p) (renameFreeJ (u,v) q)
JEq !loc e f ->
JEq loc (renameFreeExpr (u,v) e) (renameFreeExpr (u,v) f)
JIs !loc es m ->
JIs loc (map (renameFreeExpr (u,v)) es) m

JAll !loc x q -> if (x == u) || (x == v)
then
let
y = fresh
[ S.fromList [u,v]
, freeExprVarsJ q ]
in JAll loc y (renameFreeJ (u,v) $renameFreeJ (x,y) q) else JAll loc x (renameFreeJ (u,v) q) JSome !loc x q -> if (x == u) || (x == v) then let y = fresh [ S.fromList [u,v] , freeExprVarsJ q ] in JSome loc y (renameFreeJ (u,v)$ renameFreeJ (x,y) q)
else JSome loc x (renameFreeJ (u,v) q)

The only interesting bit happens with JAll. If the dummy variable x is equal to either u or v, we first swap it out with a fresh variable to avoid capturing any occurrences in q.

Next we tackle renaming bound variables.

renameBoundJ :: S.Set (Var Expr) -> Jud -> Jud
renameBoundJ avoid = \case
JVar !loc x s ->
JVar loc x s
JNeg !loc p ->
JNeg loc (renameBoundJ avoid p)
JConj !loc p q ->
JConj loc (renameBoundJ avoid p) (renameBoundJ avoid q)
JDisj !loc p q ->
JDisj loc (renameBoundJ avoid p) (renameBoundJ avoid q)
JImpl !loc p q ->
JImpl loc (renameBoundJ avoid p) (renameBoundJ avoid q)
JEqui !loc p q ->
JEqui loc (renameBoundJ avoid p) (renameBoundJ avoid q)
JEq !loc e f ->
JEq loc (renameBoundExpr avoid e) (renameBoundExpr avoid f)
JIs !loc es m ->
JIs loc (map (renameBoundExpr avoid) es) m

JAll !loc x q -> if S.member x avoid
then
let
y = fresh [S.singleton x, freeExprVarsJ q, avoid]
in JAll loc y
(renameBoundJ avoid $renameFreeJ (x,y) q) else JAll loc x (renameBoundJ avoid q) JSome !loc x q -> if S.member x avoid then let y = fresh [S.singleton x, freeExprVarsJ q, avoid] in JSome loc y (renameBoundJ avoid$ renameFreeJ (x,y) q)
else JSome loc x
(renameBoundJ avoid q)

These definitions make Jud an instance of HasExprVars.

instance HasExprVars Jud where
freeExprVars = freeExprVarsJ
renameFreeExpr = renameFreeJ
renameBoundExpr = renameBoundJ

We’re now prepared to define alpha equivalence on judgements. This is more or less the same as alpha equivalence for expressions.

instance Eq Jud where
j1 == j2 = case (j1,j2) of
(JVar _ x1 s1, JVar _ x2 s2) -> (x1 == x2) && (s1 == s2)
(JNeg _ p1, JNeg _ p2) -> p1 == p2
(JConj _ p1 q1, JConj _ p2 q2) -> (p1 == p2) && (q1 == q2)
(JDisj _ p1 q1, JDisj _ p2 q2) -> (p1 == p2) && (q1 == q2)
(JImpl _ p1 q1, JImpl _ p2 q2) -> (p1 == p2) && (q1 == q2)
(JEqui _ p1 q1, JEqui _ p2 q2) -> (p1 == p2) && (q1 == q2)
(JEq _ e1 f1, JEq _ e2 f2) -> (e1 == e2) && (f1 == f2)
(JIs _ e1 m1, JIs _ e2 m2) -> (e1 == e2) && (m1 == m2)

(JAll _ x1 q1, JAll _ x2 q2) -> if x1 == x2
then q1 == q2
else
let
y = fresh
[ freeExprVars q1
, freeExprVars q2 ]
in
(renameFreeExpr (x1,y) q1) == (renameFreeExpr (x2,y) q2)

(JSome _ x1 q1, JSome _ x2 q2) -> if x1 == x2
then q1 == q2
else
let
y = fresh
[ freeExprVars q1
, freeExprVars q2 ]
in
(renameFreeExpr (x1,y) q1) == (renameFreeExpr (x2,y) q2)

_ -> False

## Substitution

We’ll need to apply substitutions to judgements in two ways: for judgement variables and for expression variables. First we define substitution for expressions.

instance SubExpr Jud where
s $> p = case p of JVar !loc x s -> JVar loc x s JNeg !loc q -> JNeg loc (s$> q)
JConj !loc q1 q2 -> JConj loc (s $> q1) (s$> q2)
JDisj !loc q1 q2 -> JDisj loc (s $> q1) (s$> q2)
JImpl !loc q1 q2 -> JImpl loc (s $> q1) (s$> q2)
JEqui !loc q1 q2 -> JEqui loc (s $> q1) (s$> q2)
JEq !loc e1 e2 -> JEq loc (s $> e1) (s$> e2)
JIs !loc es str -> JIs loc (map (s $>) es) str JAll !loc x q -> let y = fresh [ S.singleton x , freeExprVars s , support s , freeExprVars q ] in JAll loc y (s$> (renameFreeExpr (x,y) q))

JSome !loc x q ->
let
y = fresh
[ S.singleton x
, freeExprVars s
, support s
, freeExprVars q ]
in
JSome loc y (s $> (renameFreeExpr (x,y) q)) As usual the only interesting bits happen for the JAll rule, where we have to rename the bound variable to avoid capture. Judgement substitutions inherit SubExpr and HasExprVars instances pointwise. instance SubExpr (Sub Jud) where s$> (Sub m) = Sub $fmap (s$>) m

instance HasExprVars (Sub Jud) where
freeExprVars (Sub m) =
S.unions . map freeExprVars . M.elems $m renameFreeExpr (u,v) (Sub m) = Sub$ fmap (renameFreeExpr (u,v)) m
renameBoundExpr avoid (Sub m) =
Sub $fmap (renameBoundExpr avoid) m Next we handle substitutions for judgement variables; as with expression and type substitutions, we’ll wrap this behind a type class. We also need an Arbitrary instance for judgement substitutions. class JudSub t where ($~) :: Sub Jud -> t -> t

instance Arbitrary (Sub Jud) where
arbitrary = Sub <$> arbitrary shrink (Sub m) = map Sub$ shrink m

We can apply judgement substitutions to judgements. This is made simpler by the fact that there are no binding constructs for judgement variables.

instance JudSub Jud where
s $~ p = case p of JVar !loc x t -> case applySub x s of Nothing -> JVar loc x t Just p' -> p' JNeg !loc q -> JNeg loc$ s $~ q JConj !loc q1 q2 -> JConj loc (s$~ q1) (s $~ q2) JDisj !loc q1 q2 -> JDisj loc (s$~ q1) (s $~ q2) JImpl !loc q1 q2 -> JImpl loc (s$~ q1) (s $~ q2) JEqui !loc q1 q2 -> JEqui loc (s$~ q1) (s $~ q2) JEq !loc e1 e2 -> JEq loc e1 e2 JIs !loc x str -> JIs loc x str JAll !loc x q -> let y = fresh [ S.singleton x , freeExprVars s , freeExprVars q ] in JAll loc y (s$~ (renameFreeExpr (x,y) q))

JSome !loc x q ->
let
y = fresh
[ S.singleton x
, freeExprVars s
, freeExprVars q ]
in
JSome loc y (s $~ (renameFreeExpr (x,y) q)) Again in the JAll and JSome cases we take care to avoid variable capture. We can also apply judgement substitutions to judgement substitutions pointwise: instance JudSub (Sub Jud) where s1$~ (Sub m2) = Sub $fmap (s1$~) m2

And this can be turned into a monoid structure on the set of judgement substitutions.

instance Semigroup (Sub Jud) where
s1 <> s2 = (s1 $~ s2) .& s1 instance Monoid (Sub Jud) where mempty = emptySub Finally, ‘judgement substitution application’ should be a monoid action, which we can test. test_subjud_identity :: (JudSub t, Eq t) => Proxy t -> t -> Bool test_subjud_identity _ j = j == emptySub$~ j

test_subjud_action
:: (JudSub t, Eq t) => Proxy t -> Sub Jud -> Sub Jud -> t -> Bool
test_subjud_action _ s1 s2 j =
(s1 $~ (s2$~ j)) == ((s1 <> s2) $~ j) captureJudSub :: Sub Jud -> Jud -> Jud captureJudSub s p = case p of JVar !loc x t -> case applySub x s of Nothing -> JVar loc x t Just p' -> t$> p'
JNeg !loc q -> JNeg loc $captureJudSub s q JConj !loc q1 q2 -> JConj loc (captureJudSub s q1) (captureJudSub s q2) JDisj !loc q1 q2 -> JDisj loc (captureJudSub s q1) (captureJudSub s q2) JImpl !loc q1 q2 -> JImpl loc (captureJudSub s q1) (captureJudSub s q2) JEqui !loc q1 q2 -> JEqui loc (captureJudSub s q1) (captureJudSub s q2) JEq !loc e1 e2 -> JEq loc e1 e2 JIs !loc x str -> JIs loc x str JAll !loc x q -> JAll loc x (captureJudSub s q) JSome !loc x q -> JSome loc x (captureJudSub s q) ## Matching We will need to match one judgement against another, as we did with Exprs. Eventually we’ll express inference rules in terms of judgements, and matching is how we’ll detect when a given inference rule is applied correctly. A judgement matching consists of two substitutions: a judgement substitution and an expression substitution. If $$J_1$$ and $$J_2$$ are matched by $$S_J$$ and $$S_E$$, then $J_2 = S_J \cdot (S_E \cdot J_1).$ We can construct matchings by case analysis. As with expression matching, we’ll need to keep track of a bound variable context along the way. matchJud :: Jud -> Jud -> Maybe (Sub Jud, Sub Expr) matchJud = matchJud' S.empty where match2 bound (p1,q1) (p2,q2) = do (js1,es1) <- matchJud' bound p1 p2 (js2,es2) <- matchJud' bound q1 q2 js <- unionSub js1 js2 es <- unionSub es1 es2 Just (js,es) First a utility: to match pairs of judgements, we match corresponding judgements and combine.  matchJud' bound j1 j2 = case (j1,j2) of (JVar _ x s, p) -> if s == emptySub then if S.disjoint bound (freeExprVars p) then Just (x --> p, emptySub) else Nothing else Nothing Judgement variables match any judgement, as long as no free variables become bound in context.  (JNeg _ p1, JNeg _ p2) -> matchJud' bound p1 p2 (JConj _ p1 q1, JConj _ p2 q2) -> match2 bound (p1,q1) (p2,q2) (JDisj _ p1 q1, JDisj _ p2 q2) -> match2 bound (p1,q1) (p2,q2) (JImpl _ p1 q1, JImpl _ p2 q2) -> match2 bound (p1,q1) (p2,q2) (JEqui _ p1 q1, JEqui _ p2 q2) -> match2 bound (p1,q1) (p2,q2) The logical connectives don’t bind any new variables, so matching proceeds recursively using the match2 utility.  (JEq _ e1 f1, JEq _ e2 f2) -> do es1 <- matchExprInContext bound e1 e2 es2 <- matchExprInContext bound f1 f2 es <- unionSub es1 es2 Just (emptySub, es) For equations, we match either side with the bound variable context and union.  (JIs _ e1 m1, JIs _ e2 m2) -> if m1 == m2 then do let m as bs s = case (as,bs) of ([],[]) -> Just (emptySub, s) (u:us,v:vs) -> do s2 <- matchExprInContext bound u v s3 <- unionSub s s2 m us vs s3 m e1 e2 emptySub else Nothing Is statements are similar to equations; match the expressions with the bound context.  (JAll _ x1 q1, JAll _ x2 q2) -> if x1 == x2 then matchJud' (S.insert x1 bound) q1 q2 else do let y = fresh [ bound , S.fromList [x1,x2] , freeExprVars q1 , freeExprVars q2 ] matchJud' (S.insert y bound) (renameFreeExpr (x1,y) q1) (renameFreeExpr (x2,y) q2) (JSome _ x1 q1, JSome _ x2 q2) -> if x1 == x2 then matchJud' (S.insert x1 bound) q1 q2 else do let y = fresh [ bound , S.fromList [x1,x2] , freeExprVars q1 , freeExprVars q2 ] matchJud' (S.insert y bound) (renameFreeExpr (x1,y) q1) (renameFreeExpr (x2,y) q2) JAlls and JSomes are similar to lambda expressions.  _ -> Nothing And no other pairs of judgements match. Judgement matching is a fundamental part of proof checking, so we’d do well to test it thoroughly. test_cases_jud_match :: Bool test_cases_jud_match = and [ (==) (matchJud (JVar Q (Var "P") emptySub) (JEq Q (EVar Q (Var "x")) (EVar Q (Var "y")))) (Just ( Var "P" --> (JEq Q (EVar Q (Var "x")) (EVar Q (Var "y"))) , emptySub)) This case matches the judgement variable $$P$$ against the judgement $$x = y$$.  , (==) (matchJud (JConj Q (JVar Q (Var "P") emptySub) (JEq Q (EVar Q (Var "x1")) (EVar Q (Var "x2")))) (JConj Q (JIs Q [EVar Q (Var "x0")] "crunchy") (JEq Q (ELam Q (Var "x0") (EVar Q (Var "x0"))) (EVar Q (Var "x2"))))) (Just ( Var "P" --> (JIs Q [EVar Q (Var "x0")] "crunchy") , (Var "x1" --> (ELam Q (Var "x0") (EVar Q (Var "x0")))) .& (Var "x2" --> EVar Q (Var "x2")))) This case matches the judgement $P \wedge (x_1 = x_2)$ against $(x_0\ \mathrm{is\ crunchy}) \wedge ((\lambda x_0 . x_0) = x_2)$  , (==) (matchJud (JImpl Q (JVar Q (Var "P") emptySub) (JVar Q (Var "P") emptySub)) (JImpl Q (JVar Q (Var "Q") emptySub) (JVar Q (Var "P") emptySub))) Nothing This case attempts to match $$P \Rightarrow P$$ against $$Q \Rightarrow P$$, which should fail.  , (==) (matchJud (JAll Q (Var "k") (JVar Q (Var "p") emptySub)) (JAll Q (Var "z") (JEq Q (EVar Q (Var "z")) (EVar Q (Var "x"))))) Nothing ] This case attempts to match a judgement variable inside a universally quantified statement against another universally quantified statement where the bound variable occurs. This should fail, because it is not possible to substitute a judgement for $$P$$ that correctly captures the bound variable. Property tests are also useful here; the trick is thinking of useful properties. We can of course test the equational property of matching; if $$S_J$$ and $$S_E$$ are a matching for $$J_1$$ and $$J_2$$, then we should have $J_2 = S_J \cdot (S_E \cdot J_1).$ test_jud_match :: Jud -> Jud -> Bool test_jud_match j1 j2 = case matchJud j1 j2 of Nothing -> True Just (js,es) -> j2 == js$~ (es $> j1) This test should pass if our implementation of matchJud is correct. The bad news is that the vast majority of generated test cases will hit the Nothing branch and pass trivially. To get some better coverage we’ll need to cook up some pairs of judgements that are set up to match. The simplest example I can think of is that every judgement should match itself via a trivial substitution on its set of free variables. test_jud_match_self :: Jud -> Bool test_jud_match_self j = case matchJud j j of Nothing -> False Just (_, es@(Sub m)) -> and -- [ (M.keysSet m) == (freeExprVars j) [ trivialExprSub es ] Barely less trivially, every judgement should still match itself after we rename the bound variables. test_jud_match_rename_bound :: S.Set (Var Expr) -> Jud -> Bool test_jud_match_rename_bound avoid j = case matchJud j (renameBoundExpr avoid j) of Nothing -> False Just (_, es@(Sub m)) -> and -- [ (M.keysSet m) == (freeExprVars j) [ trivialExprSub es ] Another way to cook up judgements that match is to make one an explicit substitution of the other; $$J$$ should match $$S_J \cdot (S_E \cdot J)$$ for any $$J$$, $$S_E$$ and $$S_J$$. test_jud_match_sub :: Sub Jud -> Sub Expr -> Jud -> Bool test_jud_match_sub js1 es1 j = case matchJud j (js1$~ (es1 $> j)) of Nothing -> False Just (js2,es2) -> (js2$~ (es2 $> j)) == (js1$~ (es1 $> j)) ## Type Checking Finally, we can also check that the expressions in a judgement can be consistently typed. instance TypeCheck Jud where typeCheck jud env = case jud of JVar _ _ _ -> return env JNeg _ q -> typeCheck q env JConj _ p q -> typeCheck p env >>= typeCheck q JDisj _ p q -> typeCheck p env >>= typeCheck q JImpl _ p q -> typeCheck p env >>= typeCheck q JEqui _ p q -> typeCheck p env >>= typeCheck q JEq _ e f -> do env2 <- introTypeVars (S.union (freeExprVars e) (freeExprVars f)) env (se,te) <- infer env2 e let env3 = se$. env2
(sf,tf) <- infer env3 f
let env4 = sf $. env3 case unifyTypes te tf of Left err -> throwU err Right w -> return (w$. env4)
JIs _ e _ -> do
env2 <- introTypeVars (S.unions $map freeExprVars e) env let m as env' = case as of [] -> return env' u:us -> do (se,_) <- infer env' u m us (se$. env')
m e env2
JAll _ x q -> do
let TypeEnv m = env
case M.lookup (Right x) m of
Nothing ->
introTypeVar x env
>>= typeCheck q
>>= elimTypeVar x
Just _ -> do
let
y = fresh
[ S.singleton x
, typedVarsIn env
, freeExprVars q ]
introTypeVar y env
>>= typeCheck (renameFreeExpr (x,y) q)
>>= elimTypeVar y
JSome _ x q -> do
let TypeEnv m = env
case M.lookup (Right x) m of
Nothing ->
introTypeVar x env
>>= typeCheck q
>>= elimTypeVar x
Just _ -> do
let
y = fresh
[ S.singleton x
, typedVarsIn env
, freeExprVars q ]
introTypeVar y env
>>= typeCheck (renameFreeExpr (x,y) q)
>>= elimTypeVar y