probabilistic-prolog-F-smlnj.sml

datatype term = Constant of int
	      | Variable of ad_number
	      | Compound of int*(term list)

val make_p = 0

val make_q = 1

val make_x = (Base 2.0)

fun same (Variable variable1) (Variable variable2) =
    variable1<=variable2 andalso variable2<=variable1

fun binds [] _ = false
  | binds ((variable1, _)::substitution) variable2 =
    if same variable1 variable2 then true else binds substitution variable2

fun lookup_value variable1 ((variable2, value)::substitution) =
    if same variable1 variable2
    then value
    else lookup_value variable1 substitution

fun apply_substitution substitution (term as (Constant _)) = term
  | apply_substitution substitution (term as (Variable _)) =
    if binds substitution term then lookup_value term substitution else term
  | apply_substitution substitution (Compound (function, terms)) =
    Compound (function, (map (fn term => apply_substitution substitution term)
			     terms))

fun apply_substitution_to_clause substitution (p, term, terms) =
    (p,
     (apply_substitution substitution term),
     (map (fn term => apply_substitution substitution term) terms))

fun member variable [] = false
  | member variable1 (variable2::set) =
    if same variable1 variable2 then true else member variable1 set

fun union ([], set) = set
  | union ((element::set1), set2) =
    if member element set2
    then union (set1, set2)
    else element::(union (set1, set2))

fun variables_in (Constant _) = []
  | variables_in (term as (Variable _)) = [term]
  | variables_in (Compound (function, terms)) =
    foldl union [] (map variables_in terms)

fun variables_in_clause (p, term, terms) =
    union ((variables_in term), (foldl union [] (map variables_in terms)))

fun occurs variable term = member variable (variables_in term)

fun unify (Constant constant1) (Constant constant2) =
    if constant1=constant2 then SOME [] else NONE
  | unify (term1 as (Constant _)) (term2 as (Variable _)) =
    SOME [(term2, term1)]
  | unify (Constant _) (Compound _) = NONE
  | unify (term1 as (Variable _)) (term2 as (Constant _)) =
    SOME [(term1, term2)]
  | unify (term1 as (Variable _)) (term2 as (Variable _)) =
    SOME [(term1, term2)]
  | unify (term1 as (Variable _)) (term2 as (Compound _)) =
    if occurs term1 term2 then NONE else SOME [(term1, term2)]
  | unify (Compound _) (Constant _) = NONE
  | unify (term1 as (Compound _)) (term2 as (Variable _)) =
    if occurs term2 term1 then NONE else SOME [(term2, term1)]
  | unify (Compound (function1, terms1)) (Compound (function2, terms2)) =
    if function1=function2
    then let fun loop [] [] substitution = SOME substitution
	       | loop (term1::terms1) (term2::terms2) substitution =
		 (case unify (apply_substitution substitution term1)
			     (apply_substitution substitution term2) of
		      NONE => NONE
		    | SOME substitution1 =>
		      loop terms1 terms2 (substitution1@substitution))
	       | loop _ _ _ = NONE
	 in loop terms1 terms2 [] end
    else NONE

fun map_indexed f l =
    let fun loop [] i = []
	  | loop (h::t) i = (f h i)::(loop t (i+(Base 1.0)))
    in loop l (Base 0.0) end

fun alpha_rename clause offset =
    apply_substitution_to_clause
	(map_indexed
	     (fn variable => (fn i => (variable, (Variable (offset+i)))))
	     (variables_in_clause clause))
	clause

fun proof_distribution term clauses =
    let val offset = foldl (fn (x, y) => if x<=y then y else x)
			   (Base 0.0)
			   (map (fn (Variable variable) => variable)
				(foldl union
				       []
				       (map variables_in_clause clauses)))
    in foldl op @
	     []
	     (map (fn clause =>
		      let val (p, term1, terms) = alpha_rename clause offset
		      in let fun loop p substitution terms =
				 case substitution of
				     NONE => []
				   | SOME substitution =>
				     case terms of
					 [] => [(p, substitution)]
				       | term::terms =>
					 foldl op @
					       []
					       (map (fn (p1, substitution1) =>
							loop (p*p1)
							     (SOME (substitution@
								    substitution1))
							     terms)
						    (proof_distribution
							 (apply_substitution
							      substitution
							      term)
							 clauses))
			 in loop p (unify term term1) terms end end)
		  clauses) end

fun likelihood substitution_distribution =
    foldl op + (Base 0.0) (map (fn (p, _) => p) substitution_distribution)

fun example _ =
    (gradient_ascent_F
	 (fn [p0, p1] =>
	     let val clauses = [(p0, (Compound (make_p, [(Constant 0)])), []),
				(((Base 1.0)-p0),
				 (Compound (make_p, [(Variable make_x)])),
				 [(Compound (make_q, [(Variable make_x)]))]),
				(p1, (Compound (make_q, [(Constant 1)])), []),
				(((Base 1.0)-p1),
				 (Compound (make_q, [(Constant 2)])),
				 [])]
	     in foldl op *
		      (Base 1.0)
		      (map (fn observation =>
			       likelihood
				   (proof_distribution
					(Compound (make_p,
						   [(Constant observation)]))
					clauses))
			   [0, 1, 2, 2]) end)
	 [(Base 0.5), (Base 0.5)]
	 (Base 1000.0)
	 (Base 0.1))

fun run _ =
    (let fun loop i result =
	     if i<=(Base 0.0) andalso (Base 0.0)<= i
	     then result
	     else let val ([p0, p1], _, _) = example ()
		  in loop (i-(Base 1.0)) [(write_real p0), (write_real p1)] end
     in loop (Base 1000.0) [(Base 0.0), (Base 0.0)] end; 0)