website | twitter

Tuesday, April 28, 2009

A Prolog In Haskell

Prolog In Haskell

I have been obsessed by Prolog language recent weeks. While I first learned Prolog long time ago, and actually I was attracted, I have never used it fluently because it's too hard to get familiar without any practical necessity. Although, there are a lot of interesting literatures which require certain knowledge of logic programming in computer science. So, I decided to do another approach; writing a Prolog interpreter to learn Prolog.

I chose Haskell as the implementation language because of its succinctness. I'm a beginner Haskell programmer, and I thought it was also a good opportunity to learn Prolog and Haskell same time! The starting point was a Prolog implementation in Hug98 distribution http://darcs.haskell.org/hugs98/demos/prolog/. I think this is a great Haskell program, but its too difficult to me. Rewriting it as my level would be a good exercise.

Data structures

Here is my version of Prolog in Haskell. Entire program is about 200+ lines. There is no cut operator but it has a list notation so that you can write [apple, orange | banana] stile literal. Let's take a look at the first part.

module Prolog
    (Term(..), Clause(..), w, s, cons,
     parse, parse',
     atom, variable, struct, list, nil, terms, arguments, term, clause, clauses, query,
     display,
     unify, unifyList, applyTerm, prove, rename, solveString) where

import Text.ParserCombinators.Parsec
import Data.Maybe
import Char

I used Parsec as a parser, and defined some data structures.

infix 6 :-
data Term    = Var String Int | Struct String [Term] deriving (Show, Eq)
data Clause  = Term :- [Term]                        deriving (Show, Eq)
data Command = Fact Clause | Query [Term] | ShowAll | Noop

type Rules = [Clause]
type Substitution = [(Term, Term)]

Term represents Prolog's term like "apple" or "father(abe, homer)". It can be a variable, or a structure. A variable has an index number which I used it later to distinct a same variable name in different contexts. A simple term like "apple" is also represented as a structure without elements like Struct "apple" [].

Clause is a Prolog rule like "mortal(X) :- man(X)". I stole a user defined operator constructor ":-" from original Hugs' Prolog to write a Haskell expression in Prolog like. So "mortal(X) :- man(X)" in Haskell expression becomes Struct "mortal" [Var "X" 0] :- [(Struct "man" [Var "X" 0])]. Well, it's not quite nice. Although the parser will provide better notation later, I have to use this expression when debugging the interpreter meanwhile. Its cumbersome. So I made up tiny utility functions to make Prolog data easier.

-- Utility constructors for debugging
w :: String -> Term
w s@(x:xs) | isUpper x = Var s 0
           | otherwise = Struct s []

s :: String -> [Term] -> Term
s n xs = Struct n xs

cons s cdr = (Struct "cons" [w s, cdr])
Using this functions, now "mortal(X) :- man(X)" is written as s"mortal" [w"X"] :- [s"man" [w"X"]] . It is much better, isn't it?

Unification

By the way, I like the word unification. It sounds peace and spiritual! Unification is one of two most peculiar concept in Prolog (another one is the control structure by depth first search). Unification is solving a logical equation. For example, the answer of "[X, orange] = [apple, Y]" must be X = apple, and Y = orange. It is almost same as variable binding in a normal programming language, but tricky part is that a direction is symmetry, so X = Y and Y = X is same meaning. How can it be possibly implemented?? Think about the data structure of the answer at first.

---- Unification ----

type Substitution = [(Term, Term)]
true = []

I used a list of tuples of terms, or an associate list to represent a substitution. For example, "X = apple, Y = orange" is represented as [(X, apple), (Y, orange)] (in actual Haskell code, [(w"X", w"apple"), (w"Y", w"orange")] ). A tuple of left hand side is always a variable name, and right hand side is any term, concrete value preferably. The goal of unification is making associations with variable and term. To make this process easier, "transitive" substitution is allowed. Think about an equation "X = Y, Y = banana". It is represented like [(X, Y), (Y, banana)], which is solved as X = banana, and Y = banana in apply function. Let's look at the implementation.

-- apply [(w"X", w"Y"), (w"Y", w"Z")] [(w"X"), (w"Y")] == [(w"Z"), (w"Z")]
apply :: Substitution -> [Term] -> [Term]
apply s ts = [applyTerm s t | t <- ts]

applyTerm [] (Var y n)                                  = Var y n
applyTerm ((Var x i, t):s) (Var y j) | x == y && i == j = applyTerm s t
                                     | otherwise        = applyTerm s (Var y j)
applyTerm s (Struct n ts)                               = Struct n (apply s ts)

The function apply substitutes a variable name of its value. To support transitive apply, applyTerm is called recursively if the value is also a variable. But it can solve only one way. Think about opposite case "Y = banana, X = Y". Apply can't find the fact X = banana because "Y = banana" is appeared before. So what I should do is applying X = Y before adding the substitution.

EquationSubstitution(solution)
1Y = banana, X = Y
2X = YY = banana (append)
3X = banana (apply: Y = banana) Y = banana
4Y = banana, X = banana (append)

I suppose that this two fold way solve all of logical equation. Apply is always needed before append it to the solution. Actual source implementation seems to be complicated because there are cases where a variable can appears any side, and sometimes there is no solution. To represent no-answer case, a Maybe monad is used. So there are variations such as;

  • No Answer : Nothing
  • Always true (like apple = apple) : Just true (true is a synonym of empty list [])
  • Substitution found : Just [X = some answer...]
-- unify (w"X") (w"apple") == Just [(w"X", w"apple")]
unify :: Term -> Term -> Maybe Substitution
unify (Var x n) (Var y m) = Just [(Var x n, Var y m)]
unify (Var x n)      y    = Just [(Var x n,       y)]
unify      x    (Var y m) = Just [(Var y m,       x)]
unify (Struct a xs) (Struct b ys)
      | a == b = unifyList xs ys
      | otherwise   = Nothing

unifyList :: [Term] -> [Term] -> Maybe Substitution
unifyList [] [] = Just true
unifyList [] _ = Nothing
unifyList _ [] = Nothing
unifyList (x:xs) (y:ys) = do s <- unify x y
                             s' <- unifyList (apply s xs) (apply s ys)
                             return (s ++ s')

Note that I just use append (++) to add a new substation in unifyList. But if you design carefully, recursive apply is not necessary. Using something like a map is a better idea.

Solver

As a programming language, Prolog is unique as it has no explicit control structure. Instead, a Prolog program can be seen as a big nested if then else statement. This find and branch functions are implemented of this behavior. While unification is a technique of how to solve a equation, solver deals with when each equation should be solved. There are two most important concepts to understand control structures in Prolog.

  • Goals (AND relationship) : are terms which should be solved.
  • Branches (OR relationship) : are options which might have a solution

A proof's fate is decided by branch function, branch function returns a list of goals (with corresponding substitutions). If the list is empty, this branch is failed. If the list includes empty goal, it is actually succeed because empty goal means that it is unified against a fact like "food(apple).". Well, is it complicated?

  • If branch returns [] <--- this is failed
  • If branch returns [ [some goals] [some goals] [(empty)] <--- this is succeed! ]
The goal of find function is traverse all of goals to find whether if it is true or false.
---- Solver ----

prove :: Rules -> [Term] -> [Substitution]
prove rules goals = find rules 1 goals

-- Depth first search
-- find (parse' clauses "p(X):-q(X). q(a).") 1 [parse' term "p(X)"]
find :: Rules -> Int -> [Term] -> [Substitution]
find rules i [] = [true]
find rules i goals = do let rules' = rename rules i
                        (s, goals') <- branch rules' goals
                        solution <- find rules (i + 1) goals'
                        return (s ++ solution)

-- Find next branches. A branch is a pair of substitution and next goals.
-- branch (parse' clauses "n(z). n(s(X)):-n(X).") (parse' query "?-n(X).")
branch :: Rules -> [Term] -> [(Substitution, [Term])]
branch rules (goal:goals) = do head :- body <- rules
                               s <- maybeToList (unify goal head)
                               return (s, apply s (body ++ goals))

Find function has an argument for index number to show the depth of the tree. This number is used to rename all variables used in whole rules. This is necessary because same variable name in different clauses are actually represented different variables.

-- Rename all variables in the rules to split namespaces.
rename :: Rules -> Int -> Rules
rename rules i = [ renameVar head :- renameVars body | head :- body <- rules]
    where renameVar (Var s _)     = Var s i
          renameVar (Struct s ts) = Struct s (renameVars ts)
          renameVars ts           = [renameVar t | t <- ts]
I have only explained evaluator part of the REPL, but still there are reader, printer, and loop. You can browse and download whole source code from http://github.com/propella/prolog/tree. Someday I might write some of interesting topics in the program...

Sunday, April 05, 2009

Learning Erlang and Adobe Flash format same time part 2

I have already written most important part about SWF format and Erlang's bit syntax at previous post. But just for the record, I take a note of miscellaneous knowledge to construct an interesting Flash shape. This entire note doesn't have any practical value because there are already many other useful libraries to build a swf file. But some of historical esoteric magical peculiar internal might interests you.

In the previous example, I only made three control tags:

  • End (Tag type = 0)
  • ShowFrame (Tag type = 1)
  • SetBackgroundColor (Tag type = 9)

Here, I introduce you two additional tags,

  • DefineShape (Tag type = 2) defines a vector graphics, and
  • PlaceObject2 (Tag type = 26) shows the graphics to an actual screen.

I designed new data structure to represent a SWF shape. While spec/0 is almost same as previous program, I add sample_shape/0 to define DefineShape.

% an example shape.
spec() ->
    {{frame_size, 6000, 3000},
     {frame_rate, 16},
     {frame_count, 160},
     [{set_background_color, {rgb, 240, 250, 250}},
      sample_shape(),
      {place_object2, 1},
      {show_frame},
      {end_tag}]}.

sample_shape() ->
    {define_shape,
     {shape_id, 1},
     {bounds, {rectangle, 2000, 3000, 1000, 2000}},
     {shapes, {{fills, [{solid_fill, {rgb, 50, 200, 50}}]},
        {lines, [{line_style, 100, {rgb, 100, 255, 100}},
   {line_style, 100, {rgb, 50, 150, 50}}]},
        {shape_records,
  [{style_change, [{move_to, 2000, 2000}]},
   {style_change, [{line_style, 1},
     {fill_style0, 1}]},
   {straight_edge, 0, -1000},
   {straight_edge, 1000, 0},
   {style_change, [{line_style, 2},
     {fill_style0, 1}]},
   {straight_edge, 0, 1000},
   {straight_edge, -1000, 0},
   {end_shape}]
        }}}}.

It looks complicated though, it is actually very straightforward. A DefineShape has a shape ID (or character ID), its bounding box, and actual shapes. "shape_id", "bounds", and "shapes" tuples at sample_shape/0 denote these information. Shape ID is used later for a reference by PlaceObject2.

A Shapes part consists of further sub elements, fills, lines and shape records. Every style information are defined in advance, and referenced with corresponding ID. In this case, one solid fill and two line styles are defined. After styles are defined, shape records are followed. A shape record is the most interesting and complicated part. I'll draw a moss green rectangle in 1000 x 1000 twips (20 twips = 1 pixel) with light and dark green borders in a pseudo 3-D style.

This is an actual implementation of DefineShape and PlaceObject2. I'm afraid it seems to be complicated, but it is just a direct translation from the specification. Thanks to Erlang's pattern matching syntax, It is easy to add a new tag by putting a new pattern. But sometimes distinction between ; (semi colon is used between patterns in a function) and . (dot is used after a function definition) annoys me.

tag({define_shape,
     {shape_id, ShapeId},
     {bounds, Bounds},
     {shapes, ShapesWithStyle}}) ->
    BoundsBits = rectangle(Bounds),
    Shapes = shape_with_style(ShapesWithStyle),
    record_header_body(2, list_to_binary([<<ShapeId:16/unsigned-little>>, BoundsBits, Shapes]));

tag({place_object2, CharacterId}) -> 
    PlaceFlagHasClipActions = 0,
    PlaceFlagHasClipDepth = 0,
    PlaceFlagHasName = 0,
    PlaceFlagHasRatio = 0,
    PlaceFlagHasColorTransform = 0,
    PlaceFlagHasMatrix = 0,
    PlaceFlagHasCharacter = 1,
    PlaceFlagMove = 0,
    Depth = 1,
    record_header_body(26, <<PlaceFlagHasClipActions:1,
       PlaceFlagHasClipDepth:1,
       PlaceFlagHasName:1,
       PlaceFlagHasRatio:1,
       PlaceFlagHasColorTransform:1,
       PlaceFlagHasMatrix:1,
       PlaceFlagHasCharacter:1,
       PlaceFlagMove:1,
       Depth:16/unsigned-little,
       CharacterId:16/unsigned-little>>).

shape_with_style/1 is used to construct SHAPEWITHSTYLE structure in the specification.

shape_with_style({{fills, Fills}, {lines, Lines}, {shape_records, Shapes}}) ->
    FillBits = nbits_unsigned([length(Fills)]),
    LineBits = nbits_unsigned([length(Lines)]),
    ShapeRecords = shape_records({shape_records, Shapes}, FillBits, LineBits),
    [fill_style_array({fills, Fills}),
     line_style_array({lines, Lines}),
     <<FillBits:4,
      LineBits:4>>,
     ShapeRecords].

The tricky part is FillBits and LineBits. As I have already mentioned when explaining a rectangle format in previous post, the SWF format tries to shorten a file size by all means, bit by bit. FillBits defines maximum bit size needed by fill style id. For example, if you use only one fill style, one is enough for FillBits. But if you use seven, FillBits is three (because seven is 111 as a binary). After FillBits and LineBits are calculated, they are needed in next helper function shape_records/3. But before I show you shape_records/3, some simple functions to construct styles are followed.

fill_style_array({fills, FillStyleArray}) ->
    FillStyleCount = length(FillStyleArray),
    [<<FillStyleCount:8>>, [fill_style(X) || X <- FillStyleArray]].

fill_style({solid_fill, RGB}) -> [<<16#00:8>>, rgb(RGB)].

line_style_array({lines, LineStyleArray}) ->
    LineStyleCount = length(LineStyleArray),
    [<<LineStyleCount:8>>, [line_style(X) || X <- LineStyleArray]].

line_style({line_style, Width, RGB}) ->
    [<<Width:16/unsigned-little>>, rgb(RGB)].

I think these are straightforward. Perhaps, next is the most tricky part of the SWF shape. Shape records include a number of records, each record represents style change or position change or so. While a rectangle format must to be byte aligned, each record must not be aligned, but whole shape records including them must be aligned! This fact is described in the specification very obscure way, so I didn't find out what to do unless many try-and-errors. Although, I might misunderstood what is a shape record...

Each individual shape record is byte-aligned within an array of shape records; one shape record is padded to a byte boundary before the next shape record begins. --- SWF File Format Specification Version 10

To concatenate many bit strings into one, and align whole bits, I made two functions padding/1 and concat_bits/1 (padding/1 is same one as previous post). It is likely that concatenating bitstrings exists already, but I couldn't find out from the library.

shape_records({shape_records, ShapeRecords}, FillBits, LineBits) ->
    padding(concat_bit([shape_record(X, FillBits, LineBits) || X <- ShapeRecords])).

padding(Bits) ->
    Padding = 8 - bit_size(Bits) rem 8,
    <<Bits/bitstring, 0:Padding>>.

concat_bit(XS) -> lists:foldl(fun(X, Y) -> <<Y/bitstring, X/bitstring>> end, <<>>, XS).
Rest of the source is definitions of each record. I omitted a lot of features to the explanation purpose. EndShapeRecord and StraightEdgeRecord are quite simple.
shape_record({end_shape}, _, _) -> <<0:1, 0:5>>;

shape_record({straight_edge, DeltaX, DeltaY}, _, _) ->
    NumBits = nbits_signed([DeltaX, DeltaY]),
    GeneralLineFlag = 1,
    <<1:1, 1:1, (NumBits - 2):4, GeneralLineFlag:1, DeltaX:NumBits, DeltaY:NumBits>>;

But StyleChangeRecord is the second tricky and daunting part in spite of Erlang's succinct syntax. A part of reasons of the complexity is that StyleChangeRecord allows to define a couple of operations at once optionally; line style, fill style, and pen move. So we need some data structure to represent such option.

In object oriented languages, a dictionary or a map is commonly used while an associated list is popular in functional languages. In Erlang, a list of tuples might be enough. lists:keysearch/3 find a tuple in a list where first argument is matched, so we can use it as a dictionary like structure. In our example, [{line_style, 1}, {fill_style0, 1}] means we want to change line style and fill style same time. and lists:keysearch(line_style, 1, ChangeSpec) detects a line style change option.

shape_record({style_change, ChangeSpec}, FillBits, LineBits) ->
    TypeFlag = 0,
    StateNewStyles = 0,
    StateFillStyle1 = 0,

    {StateLineStyle, LineStyleData} =
 case lists:keysearch(line_style, 1, ChangeSpec) of
     {value, {_, LineStyle}} -> {1, <<LineStyle:LineBits>>};
     false -> {0, <<>>} end,

    {StateFillStyle0, FillStyle0Data} =
 case lists:keysearch(fill_style0, 1, ChangeSpec) of
     {value, {_, FillStyle0}} -> {1, <<FillStyle0:FillBits>>};
     false -> {0, <<>>} end,

    {StateMoveTo, MoveData} =
 case lists:keysearch(move_to, 1, ChangeSpec) of
     {value, {_, MoveDeltaX, MoveDeltaY}} ->
  MoveBits = nbits_signed([MoveDeltaX, MoveDeltaY]),
  {1, <<MoveBits:5,
       MoveDeltaX:MoveBits/signed,
       MoveDeltaY:MoveBits/signed>>};
     false -> {0, <<>>} end,

    <<TypeFlag:1,
     StateNewStyles:1,
     StateLineStyle:1,
     StateFillStyle1:1,
     StateFillStyle0:1,
     StateMoveTo:1,
     MoveData/bitstring,
     FillStyle0Data/bitstring,
     LineStyleData/bitstring>>.
I uploaded final program http://languagegame.org/pub/swf.erl.
 
Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.