Safe Haskell	Safe-Inferred
Language	Haskell2010

CoALP.Program

Contents

Tier 1 structures
Tier 2 structures
Tier 3 structures
Concrete types
- Identifier, Variable, and Constant
- Datatype synonyms

Description

Basic program datatypes

Synopsis

Tier 1 structures

data Term a b c

A term for any type of functional symbol and any type of variable.

Term over Σ is a total function from a non-empty tree to Σ ⋃ Var

Notation:

T(ε) is a predicate of term
subterm(t, w) - subtree at a word w

Constructors

Var c	a variable
Fun a [Term a b c]	a function symbol

Instances

Functor (Term a b)
Foldable (OrNode (Clause a b c) (Term a b c))
Foldable (AndNode (Clause a b c) (Term a b c))
(Eq a, Eq c) => Eq (Term a b c)
(Show a, Show b, Show c) => Show (Term a b c)
NFData (OrNode (Clause a b c) (Term a b c) (Vr d))
NFData (Term a b c) => NFData (AndNode (Clause a b c) (Term a b c) (Vr d))
NFData (Term a b c)

subtermOf :: (Eq a, Eq c) => Term a b c -> Term a b c -> Bool

Test whether first argument is a subterm of second argument

propSubtermOf :: (Eq a, Eq c) => Term a b c -> Term a b c -> Bool

Test whether first argument is a proper subterm of second argument

mapSubst :: (c -> c') -> [(c, Term a b c)] -> [(c', Term a b c')]

map over substitution TODO make subst either newtype or such and this into an instance

data Clause a b c where

A clause

Notation:

clause C over Σ is a total function from finite tree language L of depth 1 to terms (term trees)
C(ε) is a head of clause
C(i) is a n-th term (for i =/= ε)

Constructors

Clause :: Term a b c -> [Term a b c] -> Clause a b c

Instances

Bifunctor (OrNode (Clause a b c))
Bifunctor (AndNode (Clause a b c))
Functor (Clause a b)
Foldable (OrNode (Clause a b c) (Term a b c))
Foldable (AndNode (Clause a b c) (Term a b c))
(Eq a, Eq c) => Eq (Clause a b c)
(Show a, Show b, Show c) => Show (Clause a b c)
NFData (OrNode (Clause a b c) (Term a b c) (Vr d))
NFData (Term a b c) => NFData (AndNode (Clause a b c) (Term a b c) (Vr d))
NFData (Clause a b c)

type Subst a b c = [(c, Term a b c)]

Substitution on terms

type Program a b c = [Clause a b c]

A program consisting of clauses

Notation:

program P over Σ is total function {0..n} ∈ N to non-goal clauses
P(i) is n-th clause

Tier 2 structures

data RewTree a b c d

Rewriting tree

This datatype represents the Definition 3.3

Constructors

RTEmpty
RT (Clause a b c) (Subst a b c) [AndNode (Clause a b c) (Term a b c) (Vr d)]

Instances

(Show a, Show b, Show c, Show d, Integral d) => Show (RewTree a b c d)

data AndNode a b c

AndNode a its is an atom with a possibly partial mapping from clauses to or-subtrees. Each of those or-subtrees corresponds to some clause number i such that the head of that clause has been unified with a and its unified body atoms label the roots of the and-subtrees of the i-th OrNode.

Or nodes in the list correspond to clauses in program

This datatype represents the Definition 3.3 3)

Constructors

AndNode b [OrNode a b c]

Instances

Bifunctor (AndNode (Clause a b c))
Foldable (AndNode (Clause a b c) (Term a b c))
(Eq a, Eq b, Eq c) => Eq (AndNode a b c)
NFData (Term a b c) => NFData (AndNode (Clause a b c) (Term a b c) (Vr d))

data OrNode a b c

OrNode ts is the or-subtree corresponding to unification against a clause in the logic program where ts are the trees built by matching against the body terms of that clause.

A separate case is the topmost ONode which contains the list of _goals_ to be unified against a logic program.

This datatype represents the Definition 3.3 2)

Constructors

OrNode a [AndNode a b c]
OrNodeEmpty c

Instances

Bifunctor (OrNode (Clause a b c))
Foldable (OrNode (Clause a b c) (Term a b c))
(Eq a, Eq b, Eq c) => Eq (OrNode a b c)
NFData (OrNode (Clause a b c) (Term a b c) (Vr d))

newtype Vr a

Type of Rew tree Variable

Constructors

Vr
Fields unVr :: a

Instances

Functor Vr
Eq a => Eq (Vr a)
(Integral a, Show a) => Show (Vr a)
NFData (Vr d)
NFData (OrNode (Clause a b c) (Term a b c) (Vr d))
NFData (Term a b c) => NFData (AndNode (Clause a b c) (Term a b c) (Vr d))

type Loop a b c = (Term a b c, Term a b c, Int)

Loop in Rewritng trees

Captures Definition 5.2

Tier 3 structures

data DerTree a b c d

Derivation tree

This datatype represents Definition 3.6

Constructors

DT (RewTree a b c d) [Trans a b c d]

data Trans a b c d

Transition between rewriting trees

see Definition 3.5

Constructors

Trans (Program a b c) (RewTree a b c d) (Vr d) (Maybe (Int, Subst a b c, Term a b c)) (DerTree a b c d)

type GuardingContext a b c = [(Int, Term a b c, [Int])]

GuardingContext gathered for every transition between rewritng trees

data OTree a b c d

Helper datatype for Observation tree

see Definition 5.5

Constructors

ODT (RewTree a b c d) [OTrans a b c d]
UNRT (RewTree a b c d)

data OTrans a b c d

Helper datatype for transition in Observation tree Guarded transition carries it's guarding context

see Definition 5.5

Constructors

OTrans (Program a b c) (RewTree a b c d) (Vr d) (Maybe (Int, Subst a b c, Term a b c)) (OTree a b c d)
GTrans (Vr d) [GuardingContext a b c] (GuardingContext a b c)

Concrete types

Identifier, Variable, and Constant

type Ident = String

Type of identifier

Identifiers start with a lower-case Latin letter or a symbol drawn from a limited set not containing the colon which is reserved to the "from" separator :- written exactly like in conventional LP. The rest of the identifier may also contain uppercase Latin letters. Examples of identifiers are

tYPE     p     <=     0th

type Var = Integer

Type of variable

Variables are essentially non-negative integers. However, the user interface allows denoting variables with names that start with an upper-case Latin letter followed by any Latin letters, symbols (same as in identifiers) or decimal digits. The parser then converts variable names to variable numbers. When arbitrary terms are printed, each variable is denoted by a name starting from V_ followed by the number of that variable. e.g.: