Safe Haskell | None |
---|---|
Language | Haskell98 |
This package aims to perform the fiddly details of instantiating induction
schemas for algebraic data types. The library is parameterised over
the type of variables (v
), constructors (c
) and types (t
).
Let's see how it looks if you instantiate all these three with String and want
to do induction over natural numbers. First, one needs to create a type
environment, a TyEnv
. For every type (we only have one), we need to list its
constructors. For each constructor, we need to list its arguments and whether
they are recursive or not.
testEnv :: TyEnv String String testEnv "Nat" = Just [ ("zero",[]) , ("succ",[Rec "Nat"]) ] testEnv _ = Nothing
Now, we can use the subtermInduction
to get induction hypotheses which are
just subterms of the conclusion. Normally, you would translate the Term
s from
the proof Obligation
s to some other representation, but there is also
linearisation functions included (linObligations
, for instance.)
natInd :: [String] -> [Int] -> IO () natInd vars coords = putStrLn $ render $ linObligations strStyle $ unTag (\(x :~ i) -> x ++ show i) $ subtermInduction testEnv typed_vars coords where typed_vars = zip vars (repeat "Nat")
The library will create fresh variables for you (called Tagged
variables),
but you need to remove them, using for instance unTag
. If you want to sync
it with your own name supply, use unTagM
or unTagMapM
.
An example invocation:
*Mini> natInd ["X"] [0] P(zero). ! [X1 : Nat] : (P(X1) => P(succ(X1))).
This means to do induction on the zeroth coord (hence the 0
), and the variable
is called X. When using the library, it is up to you to translate the
abstract P
predicate to something meaningful.
We can also do induction on several variables:
*Mini> natInd ["X","Y"] [0,1] P(zero,zero). ! [Y3 : Nat] : (P(zero,Y3) => P(zero,succ(Y3))). ! [X1 : Nat] : (P(X1,zero) => P(succ(X1),zero)). ! [X1 : Nat,Y3 : Nat] : (P(X1,Y3) & P(X1,succ(Y3)) & P(succ(X1),Y3) => P(succ(X1),succ(Y3))).
In the last step case, all proper subterms of succ(X1),succ(Y3)
are used as
hypotheses.
A bigger example is in example/Example.hs
in the distribution.
- subtermInduction :: Ord c => TyEnv c t -> [(v, t)] -> [Int] -> [TaggedObligation c v t]
- caseAnalysis :: TyEnv c t -> [(v, t)] -> [Int] -> [TaggedObligation c v t]
- data Obligation c v t = Obligation {
- implicit :: [(v, t)]
- hypotheses :: [Hypothesis c v t]
- conclusion :: Predicate c v
- type TaggedObligation c v t = Obligation c (Tagged v) t
- type Predicate c v = [Term c v]
- type Hypothesis c v t = ([(v, t)], Predicate c v)
- data Term c v
- type TyEnv c t = t -> Maybe [(c, [Arg t])]
- data Arg t
- data Tagged v = v :~ Integer
- tag :: Tagged v -> Integer
- unTag :: (Tagged v -> v') -> [TaggedObligation c v t] -> [Obligation c v' t]
- unTagM :: Applicative m => (Tagged v -> m v') -> [TaggedObligation c v t] -> m [Obligation c v' t]
- unTagMapM :: (Functor m, Monad m) => (Tagged v -> m v') -> [TaggedObligation c v t] -> m ([Obligation c v' t], Map (Tagged v) v')
- linObligations :: Style c v t -> [Obligation c v t] -> Doc
- linObligation :: Style c v t -> Obligation c v t -> Doc
- linTerm :: Style c v t -> Term c v -> Doc
- data Style c v t = Style {}
- strStyle :: Style String String String
- render :: Doc -> String
- text :: String -> Doc
Induction with subterms as hypotheses
subtermInduction :: Ord c => TyEnv c t -> [(v, t)] -> [Int] -> [TaggedObligation c v t] Source
Subterm induction: the induction hypotheses will contain the proper subterms of the conclusion.
Case analysis (no induction hypotheses)
caseAnalysis :: TyEnv c t -> [(v, t)] -> [Int] -> [TaggedObligation c v t] Source
Does case analysis on a list of typed variables. This function is equal
to removing all the hypotheses from subtermInduction
.
Obligations
data Obligation c v t Source
Quantifier lists are represented as tuples of variables and their type.
Example:
Obligation { implicit = [(x,t1),(y,t2)] , hypotheses = [([],[htm1,htm2]) ,([(z,t3)],[htm3,htm4]) ] , conclusion = [tm1,tm2] }
Corresponds to the formula:
forall (x : t1) (y : t2) . (P(htm1,htm2) & (forall (z : t3) . P(htm3,htm4)) => P(tm1,tm2))
The implicit variables (x and y) can be viewed as skolemised, and use these three formulae instead:
P(htm1,htm2).
forall (z : t3) . P(htm3,htm4).
~ P(tm1,tm2).
Obligation | |
|
type TaggedObligation c v t = Obligation c (Tagged v) t Source
type Predicate c v = [Term c v] Source
A list of terms.
Example: [tm1,tm2]
corresponds to the formula P(tm1,tm2)
type Hypothesis c v t = ([(v, t)], Predicate c v) Source
Quantifier lists are represented as tuples of variables and their type.
Example:
([(x,t1),(y,t2)],[tm1,tm2])
corresponds to the formula
forall (x : t1) (y : t2) . P(tm1,tm2)
Terms
The simple term language only includes variables, constructors and functions.
Typing environment
type TyEnv c t = t -> Maybe [(c, [Arg t])] Source
Given a type, return either that you cannot do induction on is type
(Nothing
), or Just
the constructors and a description of their arguments
(see Arg
).
The function should instantiate type variables. For instance, if you look
up the type [Nat]
, you should return the cons constructor with arguments
Nat
and [Nat]
(see Arg
).
Examples of types not possible to do induction on are function spaces and
type variables. For these, return Nothing
.
Arguments
An argument to a constructor can be recursive (Rec
) or non-recursive
(NonRec
). Induction hypotheses will be asserted for Rec
arguments.
For instance, when doing induction on [a]
, then (:)
has two arguments,
NonRec a
and Rec [a]
. On the other hand, if doing induction on [Nat]
,
then (:)
has NonRec Nat
and Rec [Nat]
.
Data types can also be exponential. Consider
data Ord = Zero | Succ Ord | Lim (Nat -> Ord)
Here, the Lim
constructor is exponential. If we describe types and
constructors with strings, the constructors for this data type is:
[ ("Zero",[]) , ("Succ",[Rec "Ord"]) , ("Lim",[Exp ("Nat -> Ord") ["Nat"]) ]
The first argument to Exp
is the type of the function, and the second
argument are the arguments to the function.
Tagged (fresh) variables
Removing tagged variables
unTag :: (Tagged v -> v') -> [TaggedObligation c v t] -> [Obligation c v' t] Source
Removing tagged (fresh) variables
unTagM :: Applicative m => (Tagged v -> m v') -> [TaggedObligation c v t] -> m [Obligation c v' t] Source
Removing tagged (fresh) variables in a monad. The remove function is exectued at every occurence of a tagged variable. This is useful if you want to sync it with your own name supply monad.
unTagMapM :: (Functor m, Monad m) => (Tagged v -> m v') -> [TaggedObligation c v t] -> m ([Obligation c v' t], Map (Tagged v) v') Source
Remove tagged (fresh) variables in a monad.
The remove function is exectued only once for each tagged variable,
and a Map
of renamings is returned.
This is useful if you want to sync it with your own name supply monad.
Linearising (pretty-printing) obligations and terms
linObligations :: Style c v t -> [Obligation c v t] -> Doc Source
Linearises a list of Obligation
, using a given Style
.
linObligation :: Style c v t -> Obligation c v t -> Doc Source
Linearises an Obligation
using a given Style
. The output format is
inspired by TPTP, but with typed quantifiers.
strStyle :: Style String String String Source
An example style where constructors, variables and types are represented as String
.