Loading [MathJax]/jax/output/HTML-CSS/jax.js

Monday, 3 June 2013

Substitution, Unification and Term Rewriting

Unification is the basis of term rewriting system, and unification algorithms is the heart of the computation model of logic programs.

Term:
terms are expressions which can be obtained from constant symbols, variables and function symbols. Constant symbols are the 0-ary functions, so no special syntactic class is needed for them.
  • Function symbols: one that has no other property than its name and arity
  • Terms that do not contain free variables are known as ground terms
  • A ground term of a formal system is a term that does not contain any free variables;
  • free variable: y is free variable in xX(x+y)>0
  • bound variable: x is bound variable in xX(x+y)>0
  • Hence xX(x+y)>0 is not a ground term, but xXx>0 is a ground term
  • x and y are variables, and f is a binary function symbol, then f(x,y) is a term
Arity - the number of arguments or operands the functions or operation accepts. For example, the arity of f(x)=x+1 is 1; the arity of f=3 is 0; the arity of f(x,y,z)=x+y+z is 3.
  • 0-ary function or operation: (arity == 0) constant symbols
  • unary function or operation: (arity == 1) such as f(x)=x2, (unary operator) x
  • binary function or operation: (arity == 2) such as f(x,y)=x+y
  • ternary function or operation: (arity == 3)
Signature:
A signature Σ is a set of function symbols, where each fΣ is associated with a non-negative integer n, the arity of f. Σ0 denotes a set of constant symbols, while Σn denotes a set of n-ary function symbols.
  • For example, group ΣG:={e,i,f} where e is 0-ary, i is 1-ary, and f is 2-ary
  • For example, a set of non-negative integers. e for smallest non-negative integer, i denotes the successor function succ(x)=x+1, and f denotes the addition function f(x,y)=x+y
Substitution:
Substitution is a syntactic transformation on strings of symbols of a formal language
  • a substitution is a finite set of the form θ={v1t1,...,vntn}, where 
    • vi: distinct variables; 
    • ti: terms with tivi;
    • viti: binding
  • Substitution application:  Eθ
    • E - expression
    • θ - substitution
    • Simultaneously replacing each occurrence of vi in E with ti
    • For example, E=p(x,y,f(a)), θ={xb,yx}, Eθ=p(b,x,f(a)).
  • Substitution Composition
    • Two substitutions:  θ={v1t1,...,vntn} σ={u1s1,...,unsn} θσ={v1t1σ,...,vntnσ,u1s1,...,unsn}
    • For example, θ={xf(y),yz}, σ={xa,yb,zy}, θσ={xf(b),zy}
  • Empty Substitution ε
  • Renaming substitution
    • θ={x1y1,...,xnyn} is a renaming substitution if yi are distinct variables
  • More general substitution (MGS)
    • a substitution θ is more general than a substitution σ, written θσ, iff there exists a substitution λ that θλ=σ
Abstract Reduction System:
  • An abstract reduction system is a pair (A,), where the reduction is a binary relation on the set A, i.e. →⊆A×A. Written ab, instead of (a,b)∈→
  • Program evaluation: a0a1.... Starting from the initial program a0, and try to reach a normal formal
  • Normal formal is the program which can not be reducible
  • Let Σ be a signature and V a countably infinite set of variables disjoint from Σ. A Σ-identity is a pair (s,t)T(Σ,V)×T(Σ,V). Identities will be written as st
  • reduction relation E, where E is a set of Σ-identity
Unification:
Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal. Unification is widely used in automated reasoning, logic programming and programming language type system implementation
  • Unification is the process of solving the satisfiability problem: given E, s and t, find a substitution θ such that θsEθt
  • For special case, where E=, this case of unification is called syntactic unification, because the unification aims to find a θ such that θs=θt i.e. θs and θt are syntactically identical.
  • If E, this is referred to semantic unification
  • Unifier of Expressions: a substitution θ is a unifier of expressions E and F iff θE=θF
    • For example, E=f(x,b,g(z)),F=f(f(y),y,g(u)). Then θ={xf(b),yb,zu} is a unifier of E and F since θE=f(f(b),b,g(u)) θF=f(f(b),b,g(u))
  • Unifier is a solution to the equation by substitution. Find a substitution to make two expressions E and F are equal and this substitution is a solution to this equation, named unifier.
Unification in Prolog:

Unification in Perl:

No comments :

Post a Comment