datatypeterm=Constantofint|Variableofad_number|Compoundofint*(termlist)valmake_p=0valmake_q=1valmake_x=(Base 2.0)fun(Variable variable1) (Variable variable2)same=variable1<=variable2andalsovariable2<=variable1fun[] _binds=false|binds ((variable1, _)::substitution) variable2=ifsame variable1 variable2thentrueelsebinds substitution variable2funvariable1 ((variable2, value)lookup_value::substitution)=ifsame variable1 variable2thenvalueelselookup_value variable1 substitutionfunsubstitution (termapply_substitutionas(Constant _))=term|apply_substitution substitution (termas(Variable _))=ifbinds substitution termthenlookup_value term substitutionelseterm|apply_substitution substitution (Compound (function, terms))=Compound (function, (map (fnterm=>apply_substitution substitution term) terms))funsubstitution (p, term, terms)apply_substitution_to_clause=(p, (apply_substitution substitution term), (map (fnterm=>apply_substitution substitution term) terms))funvariable []member=false|member variable1 (variable2::set)=ifsame variable1 variable2thentrueelsemember variable1 setfun([], set)union=set|union ((element::set1), set2)=ifmember element set2thenunion (set1, set2)elseelement::(union (set1, set2))fun(Constant _)variables_in=[]|variables_in (termas(Variable _))=[term]|variables_in (Compound (function, terms))=foldl union [] (map variables_in terms)fun(p, term, terms)variables_in_clause=union ((variables_in term), (foldl union [] (map variables_in terms)))funvariable termoccurs=member variable (variables_in term)fun(Constant constant1) (Constant constant2)unify=ifconstant1=constant2thenSOME[]elseNONE|unify (term1as(Constant _)) (term2as(Variable _))=SOME[(term2, term1)]|unify (Constant _) (Compound _)=NONE|unify (term1as(Variable _)) (term2as(Constant _))=SOME[(term1, term2)]|unify (term1as(Variable _)) (term2as(Variable _))=SOME[(term1, term2)]|unify (term1as(Variable _)) (term2as(Compound _))=ifoccurs term1 term2thenNONEelseSOME[(term1, term2)]|unify (Compound _) (Constant _)=NONE|unify (term1as(Compound _)) (term2as(Variable _))=ifoccurs term2 term1thenNONEelseSOME[(term2, term1)]|unify (Compound (function1, terms1)) (Compound (function2, terms2))=iffunction1=function2thenletfun[] [] substitutionloop=SOMEsubstitution|loop (term1::terms1) (term2::terms2) substitution=(caseunify (apply_substitution substitution term1) (apply_substitution substitution term2)ofNONE=>NONE|SOMEsubstitution1=>loop terms1 terms2 (substitution1@substitution))|loop _ _ _=NONEinloop terms1 terms2 []endelseNONEfunf lmap_indexed=letfun[] iloop=[]|loop (h::t) i=(f h i)::(loop t (i+(Base 1.0)))inloop l (Base 0.0)endfunclause offsetalpha_rename=apply_substitution_to_clause (map_indexed (fnvariable=>(fni=>(variable, (Variable (offset+i))))) (variables_in_clause clause)) clausefunterm clausesproof_distribution=letvaloffset=foldl (fn(x, y)=>ifx<=ythenyelsex) (Base 0.0) (map (fn(Variable variable)=>variable) (foldl union [] (map variables_in_clause clauses)))infoldlop@[] (map (fnclause=>letval(p, term1, terms)=alpha_rename clause offsetinletfunp substitution termsloop=casesubstitutionofNONE=>[]|SOMEsubstitution=>casetermsof[]=>[(p, substitution)]|term::terms=>foldlop@[] (map (fn(p1, substitution1)=>loop (p*p1) (SOME(substitution@substitution1)) terms) (proof_distribution (apply_substitution substitution term) clauses))inloop p (unify term term1) termsendend) clauses)endfunsubstitution_distributionlikelihood=foldlop+(Base 0.0) (map (fn(p, _)=>p) substitution_distribution)fun_example=(gradient_ascent_F (fn[p0, p1]=>letvalclauses=[(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)])), [])]infoldlop*(Base 1.0) (map (fnobservation=>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=(letfuni resultloop=ifi<=(Base 0.0)andalso(Base 0.0)<=ithenresultelseletval([p0, p1], _, _)=example ()inloop (i-(Base 1.0)) [(write_real p0), (write_real p1)]endinloop (Base 1000.0) [(Base 0.0), (Base 0.0)]end; 0)

Generated by GNU enscript 1.6.4.