CoALP-0.0.6: Coalgebraic logic programming library

Safe HaskellNone
LanguageHaskell2010

CoALP

Description

  • The CoALP top-level module.

Synopsis

Documentation

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) 

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 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

type Term1 = Term Ident Constant Var

Type of first-order term.

type Clause1 = Clause Ident Constant Var

Type of clause of first-order terms.

type Program1 = Program Ident Constant Var

Type of clause of first-order query

type Query1 = Query Ident Constant Var

Type of program of first-order term.

gc1 :: (Eq a, Eq c) => Program a b c -> Bool

Guardendes check GC1 on clauses

Given program P check that all program clauses are guarded, i. e. whenever C(ε) and C(i) have same predicate check that C(i) is a reduct of C(ε)

gc2 :: (Eq a, Eq b, Eq c, Ord c, Freshable c) => Program a b c -> Clause a b c -> Bool

Guardedness check GC2

Given program P and a clause C check guardednees of the rewriting tree

	rew (P, C, id)

gc3 :: (Freshable c, Ord c, Eq a, Eq b) => Program a b c -> Bool

Guradedness check GC3 according to Defintion 5.6 for the whole program