typeterm=Constantofint|Variableofad_number|Compoundofint*(termlist)letmake_p=0letmake_q=1letmake_x=(Base 2.0)letsame (Variable variable1) (Variable variable2)=variable1<=variable2 && variable2<=variable1letrecbinds p1 variable2=match p1with[]->false|((variable1, _)::substitution)->ifsame variable1 variable2thentrueelsebinds substitution variable2letreclookup_value variable1 ((variable2, value)::substitution)=ifsame variable1 variable2thenvalueelselookup_value variable1 substitutionletrecapply_substitution substitution p2=match p2with((Constant _)asterm)->term|((Variable _)asterm)->ifbinds substitution termthenlookup_value term substitutionelseterm|(Compound (f, terms))->Compound (f, (map (funterm->apply_substitution substitution term) terms))letrecapply_substitution_to_clause substitution (p, term, terms)=(p, (apply_substitution substitution term), (map (funterm->apply_substitution substitution term) terms))letrecmember variable1 p=match pwith[]->false|(variable2::set)->ifsame variable1 variable2thentrueelsemember variable1 setletrecunion p1 set2=match p1with[]->set2|(element::set1)->ifmember element set2thenunion set1 set2elseelement::(union set1 set2)letrecvariables_in p=match pwith(Constant _)->[]|((Variable _)asterm)->[term]|(Compound (f, terms))->fold_left union [] (map variables_in terms)letrecvariables_in_clause (p, term, terms)=union (variables_in term) (fold_left union [] (map variables_in terms))letoccurs variable term=member variable (variables_in term)letrecunify p1 p2=match p1, p2with(Constant constant1), (Constant constant2)->ifconstant1=constant2thenSome []elseNone|((Constant _)asterm1), ((Variable _)asterm2)->Some [(term2, term1)]|(Constant _), (Compound _)->None|((Variable _)asterm1), ((Constant _)asterm2)->Some [(term1, term2)]|((Variable _)asterm1), ((Variable _)asterm2)->Some [(term1, term2)]|((Variable _)asterm1), ((Compound _)asterm2)->ifoccurs term1 term2thenNoneelseSome [(term1, term2)]|(Compound _), (Constant _)->None|((Compound _)asterm1), ((Variable _)asterm2)->ifoccurs term2 term1thenNoneelseSome [(term2, term1)]|(Compound (function1, terms1)), (Compound (function2, terms2))->(iffunction1=function2thenletrecloop p1 p2 substitution=(match p1, p2with[], []->Some substitution|(term1::terms1), (term2::terms2)->(match unify (apply_substitution substitution term1) (apply_substitution substitution term2)withNone->None|Some substitution1->loop terms1 terms2 (substitution1@substitution))|_, _->None)inloop terms1 terms2 []elseNone)letmap_indexed f l=letrecloop p i=match pwith[]->[]|(h::t)->(f h i)::(loop t (i+.(Base 1.0)))inloop l (Base 0.0)letalpha_rename clause offset=apply_substitution_to_clause (map_indexed (funvariable->(funi->(variable, (Variable (offset+.i))))) (variables_in_clause clause)) clauseletrecproof_distribution term clauses=letoffset=fold_left (funyx->ifx<=ythenyelsex) (Base 0.0) (map (fun(Variable variable)->variable) (fold_left union [] (map variables_in_clause clauses)))infold_left (@) [] (map (funclause->let(p, term1, terms)=alpha_rename clause offsetinletrecloop p substitution terms=match substitutionwithNone->[]|Some substitution->match termswith[]->[(p, substitution)]|term::terms->fold_left (@) [] (map (fun(p1, substitution1)->loop (p*.p1) (Some (substitution@substitution1)) terms) (proof_distribution (apply_substitution substitution term) clauses))inloop p (unify term term1) terms) clauses)letlikelihood substitution_distribution=fold_left (+. ) (Base 0.0) (map (fun(p, _)->p) substitution_distribution)letexample _=(gradient_ascent_F (fun[p0; p1]->letclauses=[(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)])), [])]infold_left (*. ) (Base 1.0) (map (funobservation->likelihood (proof_distribution (Compound (make_p, [(Constant observation)])) clauses)) [0; 1; 2; 2])) [(Base 0.5); (Base 0.5)] (Base 1000.0) (Base 0.1))let_=(letrecloop i result=ifi<=(Base 0.0) && (Base 0.0)<=ithenresultelselet([p0; p1], _, _)=example ()inloop (i-.(Base 1.0)) [(write_real p0); (write_real p1)]inloop (Base 1000.0) [(Base 0.0); (Base 0.0)]; 0)

Generated by GNU enscript 1.6.4.