taktoa/atp-exercises.md

## atp-exercises.md

      
    Raw
  

              atp-exercises.md
            
          
    A Self-Taught Course in Automated Reasoning using Haskell

Variables, Terms, and Syntactic Unification

Resources


Introduction to Unification Theory Lecture 1
Sections 8.1 and 8.2 of The Handbook of Automated Reasoning

Exercises


Define a type Variable of metavariables.
Template: data Variable = …


Write a type FOOpenTerm of first-order open terms (essentially rose trees
where branches represent functions and leaf nodes represent metavariables
and constants, and a constant is just a 0-ary function). This type should
have one type parameter: a type of function symbols.
Template: data FOOpenTerm (fun ∷ ⋆) = …


Write a new type FOTerm that is like FOOpenTerm, but parameterized over
an arbitrary type of metavariables, so that you can represent closed terms
by setting the parameter to Void.
Template: data FOTerm (fun ∷ ⋆) (var ∷ ⋆) = …


Write a new type HOTerm, that is like FOTerm, but it supports binder
nodes, which can capture variables. Assume that each binder node can only
capture one variable. The type of binders should be a parameter; for example,
the lambda calculus would have data Binder = Lam as the parameter, whereas
first-order logic would have data Binder = ForAll | Exists as the
parameter.
Template: data HOTerm (fun ∷ ⋆) (var ∷ ⋆) (binder ∷ ⋆) = …


Redefine FOOpenTerm and FOTerm as type aliases in terms of HOTerm.


Write a function that computes the set of free variables in an HOTerm.
Template: freeVars ∷ (Ord v) ⇒ HOTerm f v b → Set v


Implement capture-avoiding substitution of a single variable on HOTerms.
Template: subst ∷ (v, HOTerm f v b) → HOTerm f v b → HOTerm f v b


Implement capture-avoiding simultaneous substitution on HOTerms.
Template: simulSubst ∷ [(v, HOTerm f v b)] → HOTerm f v b → HOTerm f v b


Write a type HOSubst of substitutions in terms of HOTerm
(essentially a partial function from variables to terms).
Template: data HOSubst (fun ∷ ⋆) (var ∷ ⋆) (binder ∷ ⋆) = …


Redefine simulSubst in terms of your type of substitutions.
Template: simulSubst ∷ HOSubst f v b → HOTerm f v b → HOTerm f v b


Define a type alias FOSubst of substitutions on first-order terms
in terms of HOSubst.


Implement syntactic matching on FOTerms.
Template: match ∷ FOTerm f Void → FOTerm f v → Maybe (FOSubst f v)


Implement syntactic unification (using the Robinson algorithm or the
Martelli-Montanari algorithm) on FOTerms.
Template: unify ∷ FOTerm f v → FOTerm f v → Maybe (FOSubst f v)


Term-Rewriting Systems

Resources:


Set Theory and Algebra in Computer Science by José Meseguer
Term Rewriting And All That by Franz Baader and Tobias Nipkow
Sections 9.1 through 9.6 of The Handbook of Automated Reasoning

Exercises


A transition system is a pair (S, →) of a set of states S and
a transition relation (→) ⊆ S². A labelled transition system is a
triple (S, Λ, →) where (→) ⊆ (S × Λ × S).
A term-rewriting system (TRS) is a transition system whose set of states is
given by a set of terms, and whose transition relation is given by a set of
rewrite rules, which, for our purposes, will be pairs p ↦ e where p is
a pattern (FO open) term and e is an expression (FO open) term, and the
set of free variables in e is a subset of the set of free variables in p.
If (a, b) is a pair of terms in a TRS, we say that a derives b
(denoted a →* b) when there exists a finite sequence of rewrites that
starts at a and ends with b. In other words, →* is the
reflexive-transitive closure of the → relation. Similarly, the transitive
closure of → is denoted by →⁺.
A pair of terms (a, b) in a TRS is joinable (denoted a ↑ b) iff there
exists a term c such that a →* c and b →* c.
A pair of terms (a, b) in a TRS is meetable iff there exists a term c
such that c →* a and c →* b.
A TRS is locally confluent if for every triple of terms (a, b, c)
such that a → b and a → c, there exists a term d such that
b →* d and c →* d.
A TRS is confluent (or satisfies the Church-Rosser property) if for every
triple of terms (a, b, c) such that a →* b and a →* c, there exists a
term d such that b →* d and c →* d.
Without referring to any outside resources (spoilers are easy to find),
come up with a term-rewriting system that is locally confluent but not
confluent.
Extra credit: come up with a term-rewriting system that has no cycles
(when thought of as a digraph) that is locally confluent but not confluent.


Write a type Rule f v for first-order rewrite rules.


We can apply a rewrite rule p ↦ e to a term t by unifying p with t to
get a substitution θ, and then applying θ to e.
Write a function that does this.
Template: applyRule ∷ Rule f v → FOTerm f v → Maybe (FOTerm f v)


Write a type TRS f v for first-order term-rewriting systems in
terms of Rule. A term-rewriting system cannot contain the same rule twice.


Write a type LTRS f v l for labelled first-order term-rewriting systems.
The l parameter is for the type of labels.


Rewrite TRS f v as a type alias for LTRS f v ().


Write a function that computes the set of terms that are the result of
applying a rewrite rule to a given term.
Template: oneStepTRS ∷ TRS f v → FOTerm f v → Set (FOTerm f v)


Generalize the oneStepTRS function to the LTRS type.
Template: oneStepLTRS ∷ (Ord f, Ord v) ⇒ LTRS f v l → FOTerm f v → Map (FOTerm f v) l


We can compute the set of terms derivable from a given term in a TRS by doing
a breadth-first search using oneStepLTRS. The search may not terminate so
the output should be given through a callback. The callback will take the
current rule (the node in the search tree) and the list of rule labels used
so far (the path from the root to the current node in the search tree).
Template: forDerivable ∷ (Monad m) ⇒ LTRS f v l → FOTerm f v → (FOTerm f v → [l] → m a) → m ()


A critical pair in a term-rewriting system is a pair of terms (t₁, t₂)
such that there exists a term t for which two different applications of a
rewrite rule (either the same rule applied differently, or two different
rules) yield the terms t₁ and t₂.
More precisely, to compute the set of critical pairs of a term-rewriting
system, we do the following for every (not necessarily distinct) pair of
rules r₁ = (p₁ ↦ e₁) and r₂ = (p₂ ↦ e₂):


Simultaneously (i.e.: with the same substitution) rename the variables
in p₂ and e₂ so that the set of free variables of r₂ is disjoint
from that of r₁.


For each non-variable subterm s in p₁, try unifying s with p₂.
If unification succeeds, assume it returns a substitution θ
(if it fails, continue on in the loop).
Denote the application (i.e.: simultaneous substitution) of θ to a
term t by θ(t).
Define x to be θ(e₁).
Define y to be the result of replacing every instance of θ(s)
in θ(p₁) with θ(e₂).
Yield the critical pair (x, y) and continue the loops.


Implement this algorithm for the TRS type.
Template: criticalPairs ∷ TRS f v → Set (FOTerm f v, FOTerm f v)


A critical pair is convergent iff it is joinable. If all the critical pairs
of a term-rewriting system are convergent, then it is locally confluent.
Write a program, using criticalPairs and forDerivable, that automatically
checks if a given term-rewriting system is locally confluent. Do not worry
about the efficiency of the algorithm. It should terminate if the given
term-rewriting system is strongly-normalizing, but it may not if that is not
the case.
Template: isLocallyConfluent ∷ TRS f v → Bool


Implement the Knuth-Bendix completion algorithm, which computes a confluent
and terminating TRS with the same deductive closure as the input TRS.
The algorithm may not terminate. Try it on some simple TRSes: a theory with
only ground terms (no variables), the theory of monoids of size n, the
theory of groups of size n.
Template: knuthBendix ∷ TRS f v → TRS f v


FIXME: future exercises


Term indexing

see chapter 26 of The Handbook of Automated Reasoning
implement path indexing
implement a discrimination tree
implement a substitution tree


Logic programming

https://www.cs.cmu.edu/~fp/courses/lp/schedule.html
write a type of formulae in Horn logic (sets of Horn clauses)
implement a proof procedure for Horn logic (Prolog)
implement a proof procedure for hereditary Harrop logic (λProlog)
(link)


SAT solvers

write the type of formulae in first-order classical logic
(parameterized on types for relation and function symbols)
write a function to convert FO formulae to negation normal form
write a function to convert FO formulae to conjunctive normal form
using the Tseytin transformation
write a function to convert FO formulae to skolem normal form
write a simple resolution-based theorem prover for first-order
classical logic
write a SAT solver using DPLL
write a type of binary decision diagrams
(and associated functions and tests)


SMT solvers

extend your SAT solver with the quantifier-free theory of
syntactic equality (using your unification algorithm)
extend your SAT solver with the quantifier-free theory of the integers
implement Cooper's algorithm for quantifier elimination in
the theory of the integers
implement the Ferrante-Rackoff algorithm for quantifier elimination in
the theory of the rationals
extend your SAT solver with the quantifier-free theory of the rationals
implement the Nelson-Oppen method for combining decision procedures


Intuitionistic type theory

implement an interpreter for the untyped lambda calculus
implement a typechecker for simply-typed lambda calculus
implement a typechecker for System F
implement a typechecker for the calculus of constructions
implement a typechecker for System F + automatic instantiation
implement a typechecker for System F + type class constraints
implement a typechecker for System F + quantified class constraints
(link)
implement a typechecker for System F + row polymorphism
(link)
implement a typechecker for System F + refinement ("liquid") types
(link)


Substructural logic

implement a proof checker for intuitionistic ordered linear logic
implement a proof checker for intuitionistic linear logic
implement a proof checker for dual light affine logic
(link)
implement a proof checker for the logic of bunched implications
write an automated theorem prover for intuitionistic linear logic
using the inverse method without focusing
(link)
speed up that theorem prover with focusing as described in the paper
write an automated theorem prover for the logic of bunched implications
using the inverse method without focusing
(link)


Hoare logic

all of this is explained in The Calculus of Computation
define a simple imperative language IMP
write an interpreter for IMP
add assert and preconditions and postconditions
and loop invariant annotations to IMP
write a function that computes weakest precondition
via symbolic execution
write a function that computes strongest postcondition
via symbolic execution
write a function that computes a verification condition
via symbolic execution
use SMT solver to automatically verify partial correctness of IMP code
add ranking function annotations to IMP
use SMT solver to automatically verify total correctness of IMP code


Separation logic

link
add heap allocation and separation logic annotations to IMP
write a type for formulae in the logic of bunched implications
reduce separation logic proof obligations in IMP to formulae in the
logic of bunched implications
extend IMP with concurrency and concurrent separation logic annotations
write a proof checker for concurrent separation logic


Modal logic

write a tableaux prover for S4 modal logic
express a situation in epistemic logic
modal μ-calculus?


Temporal logic

write the type of formulae in linear temporal logic (LTL)
write a function to convert LTL formulae to negation normal form
write a type of Büchi automata
write a function to convert LTL formulae to the associated Büchi automaton
write a function for the intersection of Büchi automata
write a model checker for LTL (easy once you have done the above)
write a type of Kripke structures
write a type of formulae in computation tree logic (CTL)
write a model checker for CTL


Abstract interpretation

write a function that does interval abstract interpretation on IMP
as described in section 12.2 of The Calculus of Computation)
write a function that bounds the complexity class of IMP code
using an abstract domain of countable ordinals
(link)


Higher order logic

implement second-order matching
(link)
implement higher-order matching
(link)
implement the (semidecidable and partial) DLS algorithm for reduction of
second-order logic to first-order logic
(link).
implement (semidecidable) higher order unification via Huet's algorithm
as described in section 16.4 of The Handbook of Automated Reasoning.


Conditional term-rewriting

define type of conditional TRSes
write algorithm eliminating conditional TRSes into unconditional TRSes
(link).


Equational unification

write a function to convert formulae in propositional classical logic
into ring sum normal form
write a function to do equational unification in the theory of
boolean rings
implement AC-unification using the algorithm that involves enumerating
maximal matchings in a bipartite graph
(link)
write a type of non-negative linear diophantine systems
reduce AC-unification to solving non-negative linear diophantine systems
implement equational/semantic unification (semidecidably) using narrowing


Termination and cotermination

implement a totality checker for STLC + a fixed point combinator using
guarded recursion (link)


Inductive theorem proving

explicit induction?
rippling?
inductionless (implicit) induction?


FIXME: notes

Decidable fragments of FOL

Sources:

https://logic.rwth-aachen.de/~graedel/kalmar.pdf
https://doi.org/10.1016/0022-0000%2880%2990027-6

Summary of decidable fragments:

the monadic predicate calculus
the prefix class ∃*∀* (the "Schönfinkel-Bernays class")
the prefix class ∃*∀∃* (the "Ackermann class")
the prefix class ∃*∀²∃* without equality (the "Gödel class")
[∃*∀*,   all, (0)]₌ (Bernays, Schönfinkel 1928)
[∃*∀²∃*, all, (0)] (Gödel 1932, Kalmár 1933, Schütte 1934)
[all,    (ω), (ω)] (Löb 1967, Gurevich 1969)
[∃*∀∃*,  all, all] (Gurevich 1973)
[all,    (ω), (1)]₌ (Rabin 1969)
[∃*∀∃*,  all, (1)]₌ (Shelah 1977)