Prolog
 Systems
 Examples
 Typeclass
 Topics
 SLD resolution
 Interesting predicates
 Imperative analogies
 Abstract Machines / Implementation
 Modes
 Verification
 Modules
 meta interpreters
 Delimitted Continuations
 Tabling
 Attributed Variables
 Constraint Logic Programming (CLP)
 Parallel
 Coroutines
 Indexing
 DCG  Definite Clauses Grammars (DCG)
 CHR
 Answer Set Programming s(CASP)
 Extralogical features
 Lambda
 Semantics
 History
 Expert Systems
 Lambda Prolog
 LogTalk
 Linear Logic Programming
 Coinductive Logic Programming
 inductive logic programmingh
 Probablistic Logic Programming
 Abductive logic programming
 Theorem Proving
 Misc
See also:
 Datalog
 Constrained Horn Clauses
 Constraint Programming (Answer Set programming in particular)
 Scheme (Minikanren)
Systems
 Swi prolog  I think this is a good default choice.
 ciao
 sicstus requires commercial license manual
 gnu prolog
 scryrer
 tau prolog  javascript web enabled
 hprolog
 binprolog
 XSB  fancy tabling.
 YAP
 Bprolog
 ECLiPSe  can talk to minizinc
 Quprolog
 trealla prolog interpreter in C. Not WAM based. treewalking, structuresharing, deep binding whatever that means
Relatives:
 Minikanren
 minizinc
 picat
 Mercury  mode declarations and type declarations. Allows reordering, but deals with IO using lionear types?
 Curry  Haskell syntax like language.
 Lambda prolog  teyjus, elpi, makam
 Hilog
 Godel
 Hyprolog  abduction
 ergo AI, flora2
 guan https://github.com/microsoft/Guan c# prolog?
Ciao
main(_) : format("hellow world").
main(_) : print([1,2,3]),
append(A,A,A), print(A)
.
assertions and auto documetation ciao and design philosphy ciaopp  preprocessor and veirfier? PLAI
Examples
Hello World
: initialization(main,main).
main(_) : format("hello world ~p\n", [foo(8)]).
Things that are prolog
 Typeclasses
 Inductive data types
 Inference rules
 CSS?
Lists
append([], X, X).
append([H  X], Y, [H  Z]) : append(X, Y, Z).
Difference Lists
Differece lists are related to singlylinked that maintain a pointer to the last element.
// something like this.
struct diff_list {
list * head;
list * end;
};
You have fast append because you don’t have to traverse the list to find the end.
append(XY,YZ,XZ).
Rewriting in prolog
Copy Term and Structural Matching
copy_term is super useful, but questionable from a purist perspective. https://www.swiprolog.org/pldoc/man?predicate=copy_term/2
I think the issue is moding? copy_term only works in one mode. “proper” prolog works in all modes, or at least has termination issues in some modes. https://www.metalevel.at/prolog/purity
copy_term can in principle be define by cases however…? No wait. it can’t. We can copy ground terms, which is almost meaningless. It’s an equality predicate also.
copy_term1([],[]). copy_term1([XXs], [XYs]) : copy_term(Xs,Ys).
eq([],[]). eq([XXs], [YYs]) : X=Y, eq(Xs,Ys).
Term rewriting
https://www.youtube.com/watch?v=b2Px7cu2a68 The context technique is nice. It’s a generic representation of context. This is showing a generic approach where rewrite rules are repreented as a data structure. But a specialization/partial evaluation is writing them directly in
step(fact(0), 1).
step(fact(N), N * fact(N')) : N #> 0, N' #= N + 1.
normal_form(T,T1) :
map(normal_form, Args),
step()
conc(F,Ls,Rs) is f(l3,l2,l1, _, r1, r2, r3)
What is demand driven egglog? It may have a relation to provenance. Naive equality proof search.
Expect lots of loops and overlap. memoization is useful.
DCG stye proof for depth control? But then Ah answer subsumption tabling can keep just first answer. Yes.
The rewrite proof reconstruction and this process are related.
> [], .
A == A > !, [refl].
add(X,Y) == add(Y,X) > [add_comm].
add(X,add(Y,Z) == add(Y,X) > [add_assoc].
% generic form
A == B > {rule(name, A ==> A1)}, [ruleL(name)], A1 == B.
A == B > {rule(name, B ==> B1)}, [ruleR(name)], A == B1.
X == Y > [eq_comm], Y == X.
f(X) == f(A) > [cong].
T1 == T2 > {T1 ..= [F  Args1], T2 ..= [F  Args2]}, [cong], map(==, Args1, Args2).
% If I used explicit context, this could be tail recursive?
: initialization(main,main).
: op(900, xfx, user:(===)).
rule(fact(N), fact(N1)).
: initialization(main,main).
: op(900, xfx, user:(===)).
rule(A + B, B + A, add_comm).
birule(A + (B + C), (A + B) + C, add_assoc).
A === A > [refl].
A === B > {rule(A ,A1, R)}, [left(R)], A1 === B.
% it is slightly simpler to just rewrite one side and leave the other as a stopping condition.
%A === B > {rule(A ,A1, R)}, [right(R)], A === B1.
% A === B > [eq_symm], B === A.
println(X) : format("~w\n", [X]).
main(_) : phrase(1 === 1, Pf), format("~w\n",Pf),
phrase(1 + 2 === 2 + 1, Pf2), println(Pf2),
length(Pf3, 0), phrase(1 + 2 === 3 + 1, Pf3), println(Pf3).
Typeclass
implements(clone,life(A,T))
impl(tostring, life(A,i64)).
impl(tostring, vec(T)) : impl(tostring, T).
% associate what trait owns fields
traitfield(tostring, tostring).
dotcall( foo, tostring ) : type(foo, T), traitfield(Trait, tostring), impl(Trant, T).
% dotcall(TEnv, foo, tostring)
% annotate everything with lifetimes?
% https://stevedonovan.github.io/rustifications/2018/09/08/commonrusttraits.html
% display, default, format, clone,
% sized
% borrow
% from to
% iterator
Type checking / inference
I probably have something like this somewhere else in my notes
This has something of the flsvor of a declarative statement of the typing rules, readin :
as horizontal line.
I’m not being careful about moding.
Not that de bruijn isn’t really necessary in the type checking process. Explicit names works ok because I’m not doing any substitution.
type(Env, nat(X), int).
type(Env, tt, unit).
type(Env, var(X), TX) : lookup(Env, X, TX).
type(Env, lam(X, B), TA > TB ) : type([X  TA Env], B, TB ).
type(Env, app(F,X), TB ) : type(Env, F, TA > TB ), type(Env, X, TA).
Hmm. in the lambda prolog encdoing of this, thye use implication for var(X). So env is more of the form [ forall Env, type(E,X,TA)  Env] but actuall maybe we want to encode that only refining environments.
type(EnvE, lam(X,B), TX > TB) : type( [forall E1, type(EnvE1, X, TX)  Env]  E, ) 
type(E,X,Tx) : var(E), forallE_type(X,Tx). forallE_type(X,Tx) : lookup(Env, forallE_type(X,Tx)) forallE_type(X,Tx) : type(E,X,Tx).
fvar(X) onto the assertion environment list.
strcturally recursive copy_term is pure and can produce fresh vars. Kindo f it builds new vars by refining a fhresness source var(X)
[]
instead of putting it in the type(var(X)) rule.
Relationship to HindleyMilner. We are using prolog uvars as type variables. This is tricky though.
https://github.com/bertas/hm_prolog/blob/master/src/type.pl This is not right to my eye for example. Using var(A) is cheating. https://www.swiprolog.org/pack/list?p=type_check a package for typechecking prolog itself with HM http://kyagrd.github.io/tiper/ Executable Relational Specifications of Polymorphic Type Systems Using Prolog Let generalization Is generalize even good prolog?
type(Env, let(X,E,B), TB) : type(Env, E, T1), generalize(T1,T2), type([X  T2  Env], B, TB).
generalize(tVar(A), )
generalize(A > B)
Topics
SLD resolution
Interesting predicates
comparson and unification of terms
=@=
, variant==
=

/=
a weaker version of dif. Uses negation as fialure in kind of unsatisfactory way 
=..
destructures a term numbervar
vanumber concretize terms. gensym suggests using content based identifiers
 termhash
variant_sha1
a cyrptographic hash? This is acceptable?
Imperative analogies
Unification variables are pointers. Unifying them is aliasing them. Unification is bidirectional pattern matching
Prolog predicates are like function calls. The fact that fields can be both input and output is like using output pointers in C. These pointers come in as arguments often.
Prolog as a Procedural Programming Language
 Assign Once variables  because of this assignment can be symmetrical
We can abuse the precedure calls of a host languages. This is related to minikanren, but minkanren doesn’t use depth first search
Manual Prolog
Proplog is even weaker than datalog. Pure propositional variables with no arguments.
# We use sequencing as , and function calls as heads.
# We could envelope in try catch blocks for calls that don't work out
# a : b, c.
def a():
b()
c()
# b : c.
def b():
c()
# c.
def c():
pass
a() # succeeds.
For nondeterminism python generators are a decent guess. Need to undo unifications. Can do Cells without persay doing generic unification. Use python case statements or if then else.
# no path compression
# `is` is python reference equality
class BadUF(): # Cell
def __init__(self): # *args
self.parent = self
def find(self):
x = self
while x.parent is not x: # or x is not instance(Cell)
x = x.parent
return x
def union(self,rhs):
p = self.find()
p2 = rhs.find()
p.parent = p2
return p2
x = BadUF()
y = BadUF()
z = BadUF()
x.union(y)
print(x.find() is y.find())
print(x.find() is z.find())
# a(Stuff) : b(Stuff), c(Stuff).
# a(Stuff) : c(Stuff)
def a(s):
for s in b(s.copy()):
for s in c(s.copy()):
yield s
for s in c(s.copy()):
yield s
class Env(dict):
def find():
def __set__(self):
#calls find
#does unification.
def __get__(self):
#calls find.
def fresh(self):
self[len(self)] = len(self)
return len(self)
def append(x,y,z,s):
s1 = s.copy()
s1[x] = []
s1[y] = s1[z]
yield s1
a, b, c = freshes(s, 3)
s[x] = (a,b)
s[z] = (a,c)
yield from append(b,y,c,s)
Yeah. This amounts to a goofy minikanren where I’ve inlined combinators.
Abstract Machines / Implementation
Warren’s Abstract Machine: A Tutorial Reconstruction.
Paul Tarau showing an interesting compilation strategy. https://popl21.sigplan.org/details/PADL2021papers/5/AFamilyofUnificationobliviousProgramTransformationsandTheirApplications https://github.com/ptarau/LogicTransformers
binprolog. Translate to binary relations
structure copying vs structure sharing
Term indexing
Original Dec10 prolog paper
BAM  berkeley abstract machine Can Logic Programming Execute as Fast as Imperative Programming? Peter Van Yoy’s thesis http://lambdatheultimate.org/classic/message1618.html#11082 Andrew Taylor’s thesis  high performance prolog implementation
VAM
TOAM  tree oriented abstract machine
global optimization in a prolog compiler for TOAM
Modes
In some ideal world, it’s great if every predicate is reversible, but it isn’t the case. Different variable positions can be used in different ways, input, output, both. They can also have total functional character (exactly one answer), partial functional character (one or zero), of nondeterminisitc (many answers). Modes are required to use predicates correctly. Annotating them may allow the compiler to be more efficient. The compiler may infer them. They are conceptually interesting also in theorem proving contexts. See bidirectional typing.
mercury ciao prolog
DIY Prolog
https://curiositydriven.org/prologinterpreter
Prolog and es6 generators https://curiositydriven.org/prologinterpreter
https://news.ycombinator.com/item?id=2152570
1985 pascal design and implementation of prolog interpreter
Verification
Modules
meta interpreters
power of prolog  A Couple of Metainterpreters in Prolog video
metapredicates
call/N
in principle could be implemented in prolog itself.
: initialization(main,main).
foo(7).
main(_) : call(foo(X)), print(X).
Things you can do:
 tracing parameter “proof”
 Change evaluation order of goals or clauses
 Change unification  occurs check, attributed vars
 continuations
 fair interleaving
 abstract interpetation
 partial evaluation
absorption and reification
: initialization(main,main).
% surprisingly raw Goal is implicit call/1
mi0(Goal) : Goal.
main(_) : mi0(mi0(append([12],[42],X))), print(X).
Advantages to not using prolog syntax.
metacircular interpeter  interpreter can interpret self https://news.ycombinator.com/item?id=19283803
: initialization(main,main).
mi([]). % empty goal stack
mi([G,Gs]) : clause_(G,Body), mi(Body), mi(Gs).
% define rules of metainterpreter itself
clause_(mi([]), []).
clause_(mi([G  Gs]), [clause_(G,Body), mi(Body), mi(Gs)]).
% what does this mean? This is a weird one.
clause_(clause_(G,Body), []) : clause_(G,Body).
Prolog metainterpreter with difference lists
: initialization(main,main).
mi([]).
mi([GGs]) :
mi_clause(G, Rest, Gs),
mi(Rest).
Same idea but the body of a clause is represented as a difference list in clause_
clause/2
is a way to get the rules of a clause.
: initialization(main,main).
clause_(append([],Y,Y), []).
clause_([X  Xs],Ys, [X  Zs]), [append(Xs, Ys, Zs)]).
%mi(Sig, all(X, Body)) : X = fvar(Sig), Sig1 is Sig + 1, mi(Sig1, Body).
%mi(all(X, Body)) : gensym(Sig), X = fvar(Sig), mi(Sig1, Body).
%mi(P, S, A => Body) : assertz(A), mi(Body), retract(A).
%mi(Sig, ex(X, Body)) : X = fvar(Sig), Sig1 is Sig + 1, mi(Sig1, Body).
mi(P,S,pi(X, Body)) : gensym(fvar, Y), X = fvar(Y), mi(P, [XS], Body). % could use numbering.
mi(P,S,D => G) : mi([DP],S,G).
mi(P,S,sigma(X,G)) : mi(P,S,G), forall( subterm(X,fvar(Y)), member(fvar(Y),S) )
mi(P,S,+G) :
This is wrong.
: initialization(main,main).
: use_module(library(occurs)).
: op(1200, xfx, \).
: op(900, xfy, =>).
% copy_term?
pi(X \ Body) : gensym(fvar,Y), X = fvar(Y), fvar(Y) => Body.
A => Body : asserta(A), Body, retract(A).
% https://www.swiprolog.org/pldoc/man?section=occurs
% https://www.swiprolog.org/pldoc/man?section=forall2
ex(X \ Body) : Body, forall(fvar(Y), free_of_var(fvar(Y), X)). % this is checking the wrong thing right?
A /\ B : A, B.
A \/ B : A; B.
% seperate the notions?
goal_and().
prog_and().
sterile(J) : pi(X \ (bug(X) => (in(X,J) => dead(X)))).
dead(B) : ex(J \ (heated(J) /\ in(B,J) /\ bug(B))).
heated(j).
main(_) : sterile(j), \+ bug(_B), \+ fvar(_X).
Hmm. when I asserta with a variable, I’m asserting the universal thing, not something tied to the variables in scope. That seems really bad.
Oh wow. Also asserta doesn’t cleanup on fail. asserta(bar(7)), fail. still leaves bar(7) asserted
chr as the store of new facts.
foo_q(X,Y,Z) \ foo(X,Y,Z) <=> true. foo_q(X,Y,Z) <=> { foo(x,y,z)}. foo_q(X,Y,Z) <=> {fail}.
or turn it around
foo(X) : foo_q_chr(X). % see if chr query succeeds % else regular other clauses.
CHR +
How can I automatically associate chr with
assert_chr(foo, Args) retract_chr(foo, Args), assert(foo, Args) <=> true. assert_chr(T,Args) \ query_chr(T, Args) <=> true. % hmm. does this unify the stuff in the assert, destroying it’s universal quantification? % https://www.swiprolog.org/pldoc/man?section=compare assert(T) \ query(T1) <=> { unifiable(T1, T), copy_term(T, Tc), Tc = T1 }. This might fix that problem. Very ugly.
Does this have proper backtracking semantics though? No. Probably not. I don’t think chr makes choice points. If unificable fails, great it continutes, but if something later fails it won’t backtrack. We could try and control which rule applies via some kind of number, a choice point placed before we call chr_query. Getting quite arcane. assert(T) \ query(T1) <=> { unifiable(T1, T), copy_term(T, Tc), Tc = T1 ; fail}.
This is insanity. Wow, shallowly embedding harrop clauses in prolog is hard/impossible.
Naw, why even seaprate out the args? Maybe better indexing, but screw it for now. assert_chr(foo(Args)). I might be building a prolog (meta?) interpreter in chr.
Delimitted Continuations
Continuations are a reification of a call stack. The call stack in prolog is a goal stack. When you
swipl manual entry schrivers et al disjunctive delimited control
 effect handlers  implicit state
 definite clause grammars
 coroutines
Tabling
Tabling is a kind of automemoization. It can make queries terminate that no longer did, and the caching can speed others up.
Tabling as a Library with Delimited Control Swi prolog manual Programming in Tabled Prolog  Warren Tabling as Concurrent Machines
Tabling with Answer Subsumption: Implementation, Applications and Performance
Tabling with Sound Answer Subsumption Fixing nondeterminsim
Simplifying dynamic programming via modedirected tabling Modedirected tabling for dynamic programming, machine learning, and constraint solving
: table path/2.
edge(1,2).
edge(2,3).
edge(3,1).
edge(3,4).
path(X,Y) : edge(X,Y).
path(X,Z) : edge(X,Y), path(Y,Z).
: initialization(main,main).
main(_) : path(1,4).
: use_module(library(tabling)).
: table a/0.
a : a.
https://www.swiprolog.org/pldoc/man?section=tablingmodedirected. Mode difreced tabling. Can take minimum answer, first answer, etc. Good for dynamic programming
Longest common subsequence
%: use_module(library(tabling)).
: table lcs(_,_,lattice(longest/3)).
lcs([], _Ys, []).
lcs(_Xs, [], []).
lcs([XXS], [XYS], [XZs]) : lcs(XS,YS,Zs).
lcs([XXS], [YYS], Zs) : dif(X,Y), (lcs([XXS],YS, Zs); lcs(XS,[YYS],Zs)).
longest(P1, P2, P):
length(P1, L1),
length(P2, L2),
( L1 > L2
> P = P1
; P = P2
).
: initialization(main,main).
main(_) : lcs([1,2,3], [2,7,1,4,2,3,6,5], LCS), print(LCS).
%lcs([1,2,3], Ys, LCS1), print(LCS1).
Hmm. Tabling comes from earley parsing historically. That’s interesting. “Earley deduction”
tabling and packrat parsing DCGs + Memoing = Packrat Parsing But is it worth it? tabling vs memoing
Memoisation: Purely, Leftrecursively, and with (Continuation Passing) Style More declarative tabling in Prolog using multiprompt delimited control
Queries and Answers as separate concepts.
 Variant Tabling  lookup in the table only allows for renaming of variables in the query
 Subsumptive tabling  lookup can also succeed on anything that is
Call similarity vs answer similarity. User defined subsumption
Variant storage and query seems relevant to harrop datalog
Tabling makes an entry in the table when it encounters a goal. When it encounters this goal again it reads from the table
Eddie modelled prolog as a “memoized” (Pred > Bool). Maybe really (Pred > Maybe Bool) where the table contains lattice values. (Pred > Set). SUbsumptive tabling makes Pred ordered too (slash a lattice?). The arrow has to be monotonic.
tnot. Stratified negation. Is this what all the continuations are about? Suspend this goal until the table is complete. Tabling as a server. The table can store continuations of who is expecting answers next?
Tabling needs to record continuations in order to know who to tell when it discovers a new answer for that query.
edges = [(1,2), (2,3), (3,4), (4,1), (2,1), (14,24)]
ptable = {}
# assert ans as possibility in response to question q
def add_ptable(q, ans):
answers, conts = ptable[q]
if ans not in answers: # don't repeat answers already seen. Inductively, consumers already informed
answers.add(ans) # add to answer set
# inform consumers of this question of new answer
for k in conts:
k(ans)
# request information about paths starting at x.
def path(k, x): # y unknown aka path(x,Y) with continuation k
if x in ptable:
answers, conts = ptable[x]
conts.append(k)
for a in answers:
k(a)
else:
ptable[x] = (set(),[k])
# path(X,Y) : edge(X1,Y), X1 = X.
for (x1,y) in edges:
if x1 == x:
add_ptable(x, (x,y))
# path(X,Z) : edge(X1, Y), X1 = X, path(Y,Z)
for (x1,y) in edges:
if x1 == x:
path(lambda ans: add_ptable(x, (x, ans[1])), y)
# query paths starting from 1
path(lambda ans : print("starts from 1", ans), 1)
#path(lambda ans : print(ans), 1)
add_ptable(1, (1,8))
print(ptable) # note 14,24 data not in there. Not bottom up
path(lambda ans : print("starts from 3", ans), 3)
print(ptable)
path(lambda ans : print("starts from 3", ans), 14)
print(ptable)
This somehow didn’t have a problem with the recursive answer. A failing computation may later succeed. Is it not a problem that we are filling the continuation table excessively?
To make it less spooky, the continuation could be defunctionalized maybe? This would allow us to deduplicate the continuations as we can make a set of the
Very coroutiney. Memoized coroutines?
bounded term depth property. all terms have bounded depth. tabling is guaranteed to terminate definite programs  no negation normal programs
A TermBased Global Trie for Tabled Logic Programs give reasoning a trie cool summary of indexing structures
consumers vs generators. First time goal is reached it is egenerator. subsequent are consumers
To what degree can the parts of magic set be seen as analogs of tabling
variant tabling  the magic predicates may be storage of tabling keys / queries
Tabling is “memoized coroutines” Memoing
There is more variation available in memoizing than I realized.
fib_table = {0:1, 1:1}
def fib(n):
if n in fib_table:
return fib_table[n]
res = fib(n1) + fib(n2)
fib_table[n] = res
return res
print(fib(3))
There are two very distinct sites of interaction with the table. Checking if a query is in the table, vs filling in the table once you know.
If you’re worried about a non terminating computation because you end up callign yourself in a loop, you can mark a question as already asked in the table. We lift a nonterminating query to and Option[int] returning query that for some examples of nontermination instead returns None
.
fib_table = {0:1, 1:1}
def fob(n):
if n in fib_table:
#if fib_table[n] == None:
# return None
return fib_table[n]
else:
fib_table[n] = None # mark question as asked
x = fob(n) # now this is an infinite loop
if x == None: # error handling
return None
y = fob(n1)
if y == None:
return y
res = x + y
fib_table[n] = res
return res
print(fob(3))
What about memoizing coroutines
Above was tabling/memoizing a determinstic computation Tabling semideterminstic is easier than full nondeterminism.
path query in semideterministic mode. Either fails or succeeds. Not multiple values.
edge = {0:1, 1:2, 2:0}
path_table = {(x,y) for i,j in edge.items()}
def path(x,z):
if (x,z) in path_table:
return True
for y in edge[x]:
p = path(y,z)
if p == True:
return True
return False
print(path(0,0))
XSB
XSB prolog has some unsusual features and supposedly the most advanced implementation of tabling.
The manual is quite nice.manual vol 1
http://xsb.sourceforge.net/research.html
john[spouse>mary, child>>{bob,bill}]
translates to
fd(john,spouse,mary)
mvd(john,child,bob)
mvd(john,child,bill)
model checking
termsets {Var:Goal} let’s you talk about the set that corresponds to Goal.
{X : member(X,[a,b,c])}
This is related to “first class sets” in datalog
Prolog has setof
termsets  save space if factorable in this way compared to “extensionalizing”
egraph equality infects everywhere. equals is equals. termsets aren’t saying terms are equal.
egraphs for parse trees?
a(a(a(b(b(b))))) as a string Or maybe symmetric comp form?
S > aSb
S > eps
There are different mechanisms for table size restrictions / improve terminating. radial,
incrmenetal table mainatence. Has a dependency graph. Something like seminaive? Trie based vs not?
Weaker semantics and choosing semantics.
Attributed Variables
Attaching extra info to variables. This can be be used to implement CLP as a library
https://www.metalevel.at/prolog/attributedvariables https://sicstus.sics.se/sicstus/docs/3.7.1/html/sicstus_17.html https://www.swiprolog.org/pldoc/man?section=attvar
Attributed variables are a union find dict?
Constraint Logic Programming (CLP)
 CLP(B)  constraint over boolean variables. Sometimes bdd based
 CLP(FD)
 CLP(Z)
Indexing dif/2
reif
if_/
tfilter/3
eclipse talks to minizinc? clp examples
Prolog II, III IV.
Cyclic terms. Rational terms. See Condicutive logic programming swi prolog comments on rational trees
introduction to prolog III prolog and infinite trees
Parallel
https://en.wikipedia.org/wiki/Parlog 50 years of datalog talks about stuff.
Coroutines
dif/2
? Test is delyed until terms are sfufcient different or have become identicalfreeze/2
 equivalent to call is Var is bound frozen when call_residue_vars
delay block
Indexing
https://www.youtube.com/watch?v=FZLofckPu4A&ab_channel=ThePowerofProlog
 first argument indexing
 deep indexing
 multi argument indexing

JIT
 exchange arguments
 use specific functor not default ones  https://www.metalevel.at/prolog/data#clean clean vs dirty reps. For example reprrsent integer by lit(N) rather than raw N. default args + nonlogical preds are nodet. not good. “defaulty” representation. We can’t symbolically express lit(X) + lit(Y). monotonic mode of clp(z)
 pull unifications into head (should happen by default)
 decompose arguments  use auxiliary predicates if system doesn’t offer deep indexing
 lagged arguments  one case is subsumed by another. list_last convert to auxliary that remebed what you’ve seen. Check if foldl is applicable
 reification. zcompare, if_. library(reif), tfilter
redundant choice points are an indication of lost performance or poor indexing
Indexing dif/2 Consider a removal predicate on a list. it involves dif.
first zargument indexing eclipse: from LP to CLP demand driven indexing of prolog clauses preindexed terms for prolog See also tabling
DCG  Definite Clauses Grammars (DCG)
https://www.youtube.com/watch?v=CvLsVfq6cks&t=3811&ab_channel=ThePowerofProlog
Anne Ogborn tutorial hakank picat triska dcg primer swi manual  comments are good too
DCGs look a bit like CFG grammars. They make threading an input and remainder list implicit. The input and remainder are considered a difference list.
DCGs describe sequences. They can be used to serialize and deserialize, parse and pretty print.
You call a DCG via phrase/2
. phrase/3
gives you access to the remainder. phrase/2 specializes phrase/3 with a [] terminator. DCGs are annotated as double slashes as//0
.
as > [].
as > [a], as.
: initialization(main,main).
main(_) : phrase(as, [a,a,a]), print("passed"),
phrase(as, [a,b,a]), print("doesn't pass").
{ mygoal }
is a way to lift a prolog goal that doesn’t touch the input lists.
Triska suggests turning on double quoted strings becomes lists. It appears swi has some behavior like this by default.
: set_prolog_flag(double_quotes, chars).
% even number of as
as > "".
as > "aa", as.
: initialization(main,main).
main(_) : phrase(as, "aaaa"), print("passed").
seqq describes concatenating a sequence of lists.
seq
 semicontext
 DCGs are useful also for implicilty carrying state.
 State trasnformation is a sequence of states when considered purely functionally.
state(S), [S] > [S]. state(S0, S), [S] > [S0].
Being able to implicilty pass state makes DCGs reminscent of monads. I’ve not seen a proof of equivalence however. State is a very powerful construct. Me dunno. Maybe you could even pass around continuations in there.
This is showing context notation. Lists on the left hand sides of rules are pushed onto the stream after the rule works (I guess that means it unifies the head of the remained with this quantity). It looks very much like a form of lookahead.
library dcg/basics, dcg/high_order
library pio  pure io. phrase_from_file phrase_to_stream
Triska shows an interesting trick to improve nontermination. You can parametrize your dcg such that it knows it is consuming the input stream. The recursion depth should be bounded by the stream size itself. Very reasonable. The decreasing argument is the stream itself.
expr([_  Rs], Rs) –> “1”. shows that expr consumes one character Called via phrase(expr(Rs, _),Rs).
Or more easily, use tabling.
Reporting errors  add error streat arguments to dcg
regexp interpreter. dcg rexp//1
Longest match firsat behavior  order rules for longest match
Bussproofs printing
proof(bin(G, Rule, PX,PY)) > proof(PX), proof(PY),
,"\RightLabel{", rule(Rule) ,"}", "\BinaryInfC{", sequent(G), "}".
proof(un(G, Rule, PX)) > proof(PX),
,"\RightLabel{", rule(Rule) ,"}", "\UnaryInfC{", sequent(G), "}".
proof(ax(G, Rule)) >
,"\RightLabel{", rule(Rule) ,"}", "\AxiomC{", sequent(G), "}".
height(ax(_,_), 0).
height(un(_,_,PX), N) : N := NX+1, height(PX,NX).
height(bin(_,_,PX,PY), N) : N := max(NX,NY)+1, height(PX,NX), height(PY,NY).
Categorical Prover
%sequent( Hyp, Conc, Var )
: use_module(library(clpfd)).
%: table prove/2.
: use_module(library(solution_sequences)).
%: op(600, xfy, i ).
prove(S, ax(S, id)) : S = (A > A).
prove(S, ax(S, fst)) : S = (A /\ _B > A).
prove( A /\ B > B, ax(A /\ B > B, snd)).
prove( S, ax(S, inj1 )) : S = (A > A \/ _B).
prove( S, ax(S, inj2 )) : S = (B > _A \/ B).
prove( false > _ , initial ).
prove( _ > true , terminal ).
prove( A > B /\ C, bin(A > B /\ C, pair, P1, P2)) : prove(A > B, P1), prove(A > C, P2).
prove( A \/ B > C , bin(A \/ B > C, case, P1, P2)) : prove( A > B, P1), prove( A > C, P2).
prove( A > C, bin(A > C, comp, P1, P2)) : prove(A > B, P1), prove(B > C, P2).
height(ax(_,_), 1).
height(un(_,_,PX), N) : N #> 1, N #= NX+1, height(PX,NX).
height(bin(_,_,PX,PY), N) : N #> 1, N #= max(NX , NY) + 1, height(PX,NX), height(PY,NY).
% maybe explicilty taking proof steps off of a list. using length.
% use dcg for proof recording?
prove(A > A) > [id].
prove(A /\ _ > A) > [fst].
prove(_ /\ B > B) > [snd].
prove(A > A \/ _) > [inj1].
prove(B > _ \/ B) > [inj2].
prove(false > _) > [initial].
prove( _ > true) > [terminal].
prove(A > B /\ C) > [pair], prove(A > B), prove(A > C).
prove(A \/ B > C) > [case], prove(A > C), prove(B > C).
prove(A > C) > [comp], prove(A > B), prove(B > C).
: initialization(main).
%main : format("hello world", []).
%main : between(1, 10, N), height(Pf, N), writeln(Pf), prove( w /\ x /\ y /\ z > w, Pf ), print(Pf), halt.
main : length(Pf, _), phrase(prove(w /\ x /\ y /\ z > w \/ y),Pf), print(Pf), halt.
main : halt.
Yes, the dcg form is very pretty. It’s a writer monad of sorts. It is recording a minimal proof certificate that is reconstructable to the full thing pretty easily.
G > [tag], D1, D2
Should be read as
D1 D2
 tag
G
prove(Sig , A > B) > { insert(A,Sig,Sig1) }, [weaken(A)], prove(Sig1, A > B).
prove(A > forall(X,B)) > , prove(weak(X, A) > B).
prove(A > forall(X,B)) > {insert(X,Sig,Sig2) }, prove(Sig1, A > B).
prove(Sig, forall(X,A) > ) > , prove(weak(X, A) > B)
Maybe start with implication prove((A > (B > C) ) –> [curry], prove( A /\ B > C). prove((A /\ (A > B) > B ) –> [eval].
Catlog
Instruction selection
A model of Instruction selection can be viewed as related to a parsing problem. A parse is building a tree out of a linearized sequence. Instruction selection is finding a linear sequence of machine instructions to represent an expression or sequence of high level statements.
% isel(R0, select( ,A + B)) > {B := }
isel(R0, lit(A)) > [mov(R0, A)]. % {integer(A)},
isel(R0, A + A) > [lsl(R0, R1)], isel(R1, A).
isel(R0, A + B * C) > [fma(R0, RA,RB, RC)], isel(), sel().
isel(R0, A + B) > [add(R0, R1, R2)], isel(R1, A), isel(R2, B).
isel(R0, A * B) > [mul(R0, R1, R2)], isel(R1, A), isel(R2, B).
%isel(R0, binop(Op, A, B)) > [mul(R0, R1, R2)], isel(R1, A), isel(R2, B).
% note storage restrictions.
% isel(reg(R0), A + B) > [add(reg(R0), reg(R1), reg(R2))], isel(reg(R1), A), isel(reg(R2), B).
% spill?
% isel(R0, A) > [mv(R0, R1)], isel(R1, A). %optional copy. Bad rule
% liveness.
% isel(LiveSet, ) > [add(R0,R1,R2)], { Live1 = Live \ R0 + R1 + R2 } , isel(LiveSet)
% maybe use bitvector?
% No give varoables unique identifiers, skolem style? id(1, Expr), id(2, Expr),
: initialization(main,main).
main(_) : phrase(isel(R0, lit(2) + lit(7)), Asm), print(Asm), halt.
CHR
forward chaining, chr comes up
swipl manual section Anne Ogborn’s tutorial Schrijver’s ICLP tutorial
Constraint handling rules A question I never had an answer for https://twitter.com/notjfmc/status/1422215450675535877?s=20&t=RyHMtBS3ySaALLC9MuGmUA . CHR afaik are a way of integrating eager rewriting into prolog https://en.wikipedia.org/wiki/Constraint_Handling_Rules
I’m not sure this is even persay a prolog topic. But the prolog community is the most engaged
http://www.informatik.uniulm.de/pm/fileadmin/pm/home/fruehwirth/constrainthandlingrulesbook.html chr.js chr what else
Where is the CHR constraint store?
Some cool examples. Gaussian, fourier, rational trees, equation solvers
https://github.com/brog45/chrplay
compiler to sql statements. Makes sense. Multiset rewriting?
sql Man what hope is there of compiling a 7 year old haskell project?
cchr efficient implementation in C
yihong’s egraph in chr. awesome
Automatic Differentiation using Constraint Handling Rules in Prolog Build up dataflow graph. Huh.
Pros and Cons of Using CHR for Type Inference https://twitter.com/flippac/status/1567622246025383938?s=20&t=7jEZQlMkI3Jdw1lLGSjg
Toward a FirstOrder Extension of Prolog’s Unification using CHR
Extending Arbitrary Solvers with Constraint Handling Rules
Compiling
KU leuven system : implementation and application. Hmm. Is CHR compiled into prolog code?
CCHR: the fastest CHR Implementation, in C
Idle thoughts, what about time dataflow.
attributed data for chr indexing
Examples
CHR parsing “Analysing graph transformation systems through Constraint Handling Rules” by Frank Raiser and Thom Frühwirth “As time goes by: Constraint Handling Rules — A survey of CHR research from 1998 to 2007” by Jon Sneyers, Peter Van Weert, Tom Schrijvers and Leslie De Koninck
https://stackoverflow.com/questions/67771845/prologgetalistofalltherulesanentityverifies
: use_module(library(chr)).
: chr_constraint snore/1, sleep/1, breathe/1.
: chr_constraint eat/1, live/1, rest/1, collect/2, pull/2.
snore(X) ==> breathe(X).
snore(X) ==> sleep(X).
sleep(X) ==> rest(X).
breathe(X) ==> live(X).
eat(X) ==> live(X).
sleep(X) ==> live(X).
live(X) \ live(X) <=> true. % eliminates duplicates
collect(Who,L),snore(Who) <=> collect(Who,[snoreL]).
collect(Who,L),sleep(Who) <=> collect(Who,[sleepL]).
collect(Who,L),breathe(Who) <=> collect(Who,[breatheL]).
collect(Who,L),eat(Who) <=> collect(Who,[eatL]).
collect(Who,L),live(Who) <=> collect(Who,[liveL]).
collect(Who,L),rest(Who) <=> collect(Who,[restL]).
pull(Who,L) \ collect(Who2,L2) <=> Who = Who2, L = L2.
: module(leq,[leq/2]).
: use_module(library(chr)).
: chr_constraint leq/2.
reflexivity @ leq(X,X) <=> true.
antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y.
idempotence @ leq(X,Y) \ leq(X,Y) <=> true.
transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).
/*
? leq(X,Y), leq(Y,Z).
leq(X, Z),
leq(Y, Z),
leq(X, Y).
*/
finite domain solver.
: module(dom,[dom/2]).
: use_module(library(chr)).
: chr_constraint dom(?int,+list(int)).
: chr_type list(T) > [] ; [Tlist(T)].
dom(X,[]) <=> fail.
dom(X,[Y]) <=> X = Y.
dom(X,L) <=> nonvar(X)  memberchk(X,L).
dom(X,L1), dom(X,L2) <=> intersection(L1,L2,L3), dom(X,L3).
% ? dom(A,[1,2,3]), dom(A,[3,4,5]).
% A = 3.
CHR debugging chr tracing chr_show_store
https://www.swiprolog.org/pldoc/man?section=chrguidelines Don’t bind rules in head mode declarations of chr affect performance. Huh c \ c <=> true is often desirable. Set semantics instead of multiset.
You can ignore the
: initialization(main,main).
main(_) : whatever
as noise that I do to make my prolog programs run from the command line instead of interactively.
Basics
: use_module(library(chr)).
: chr_constraint rain/0, wet/0, umbrella/0.
rain ==> wet.
rain ==> umbrella.
: initialization(main,main).
main(_) : rain, chr_show_store(true).
: use_module(library(chr)).
: chr_constraint rain/0, wet/0, umbrella/0.
rain <=> wet.
rain <=> umbrella.
: initialization(main,main).
main(_) : rain, chr_show_store(true).
% just wet
: use_module(library(chr)).
: chr_constraint left/0, right/0, forward/0, backward/0.
left,right <=> true.
forward, backward <=> true.
: initialization(main,main).
main(_) : forward, left, right, backward, left, chr_show_store(true).
% just left
Pairing
: use_module(library(chr)).
: chr_constraint male/1, female/1, pair/2.
% <=> makes a pairing
% this makes all pairs
% male(X),female(Y) ==> pair(X,Y).
male(X) \ female(Y) <=> pair(X,Y).
% hmm cransto gets farbus.
: initialization(main,main).
main(_) : male(gary), female(zirkin), male(cransto), female(farbus), chr_show_store(true).
Paths from edges
: use_module(library(chr)).
: chr_constraint edge/2, path/2.
base @ edge(X,Y) ==> path(X,Y).
trans @ edge(X,Y), path(Y,Z) ==> path(X,Z).
pset @ path(X,Y) \ path(X,Y) <=> true.
: initialization(main,main).
main(_) : edge(1,2), edge(3,4), edge(3,2), edge(1,3), chr_show_store(true).
Minimum
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint min/1, findmin/1.
findmin(_), min(N) \ min(M) <=> N < M  true.
findmin(Min), min(N) <=> Min = N.
main(_) : min(7), min(14), min(13), findmin(Min), print(Min), chr_show_store(true).
GCD
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint gcd/1.
gcd(N) \ gcd(M) <=> 0 < N, M>=N  Z is M  N, gcd(Z).
% hmm not working
main(_) : gcd(15), gcd(5), chr_show_store(true).
Sort
bubble sort
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint a/2.
a(I,V), a(J,W) <=> I>J, V<W  a(I,W), a(J,V).
main(_) : a(1,6), a(2,4), a(3,14), chr_show_store(true).
merge sort
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint next/2.
next(A,B) \ next(A,C) <=> A < B, B < C  next(B,C).
main(_) : next(0,7), next(0,2), next(0,5), chr_show_store(true).
Get foo
Fibonacci
merge sort
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint fib/2.
fib(0,M) <=> M = 1.
fib(1,M) <=> M = 1.
%fib(N,M) <=> N >= 2, ground(N)  fib(N1, M1), fib(N2, M2), when((ground(M1),ground(M2)), M is M1 + M2).
fib(N,M) <=> N >= 2, ground(N)  N1 is N  1, N2 is N  2, fib(N1, M1), fib(N2, M2), M is M1 + M2.
main(_) : fib(5,M), print(M), chr_show_store(true).
: use_module(library(chr)).
: use_module(library(clpfd)).
: initialization(main,main).
: chr_constraint fib/2.
fib(0,M) <=> M #= 1.
fib(1,M) <=> M #= 1.
fib(N,M) <=> ground(N), N #>= 2  N1 #= N  1, N2 #= N  2, fib(N1, M1), fib(N2, M2), M #= M1 + M2.
main(_) : fib(5,M), print(M), chr_show_store(true).
top down memo
: use_module(library(chr)).
: use_module(library(clpfd)).
: initialization(main,main).
: chr_constraint fib/2.
cong @ fib(N,M1) \ fib(N,M1) <=> M1 #= M2.
fib(0,M) ==> M #= 1.
fib(1,M) ==> M #= 1.
fib(N,M) ==> ground(N), N #>= 2  N1 #= N  1, N2 #= N  2, fib(N1, M1), fib(N2, M2), M #= M1 + M2.
main(_) : fib(5,M), print(M), chr_show_store(true).
% store is not empty. Contains memoized fib entries.
Boolean Propagators
Lattice
lat(A), lat(B) <=> lat(join(A,B))
Propagators are monotonic functions between lattices. CHR was built for propagation BitSet CHRs? Other fast propagators?
Assignment
Union Find
From furhwith book. Generalized union find is also interesting.
: use_module(library(chr)).
: initialization(main,main).
% hmm are these annotations ok?
: chr_constraint make(+int), find(+int,), root(+int,+int), union(+int,+int), link(+int,+int), pto(+int,+int).
make(A) <=> root(A,0).
union(A,B) <=> find(A,X), find(B,Y), link(X,Y).
pto(A, B), find(A,X) <=> find(B,X), pto(A,X).
root(A,_) \ find(A,X) <=> X=A.
link(A,A) <=> true.
link(A,B), root(A,N), root(B,M) <=> N>=M  pto(B,A), K is max(N,M+1), root(A,K).
link(B,A), root(A,N), root(B,M) <=> N>=M  pto(B,A), K is max(N,M+1), root(A,K).
main(_) : make(1), make(2), make(3), union(1,2), find(2,X), find(3,Y),
print(X),print(Y), union(1,3), chr_show_store(true).
EGraphs
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint eclass/2.
fcong @ eclass(f(X), E1) \ eclass(f(X), E2) <=> E1 = E2.
acong @ eclass(a, E1) \ eclass(a, E2) <=> E1 = E2.
main(_) : eclass(a, A), eclass(f(A), FA), eclass(f(FA), FFA), FA=A, chr_show_store(true).
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint eclass/2, gas/2.
pcong @ eclass(X + Y, E1) \ eclass(X + Y, E2) <=> E1 = E2.
% nothing should produce this? Well...
% ncong @ eclass(num(X), E1) \ eclass(num(X), E2) <=> E1 = E2.
% pcong @ eclass(T, E1) \ eclass(T, E2) <=> E1 = E2.
gas(_, 0) <=> true.
comm @ eclass(X + Y, E) \ gas(comm, N) <=> N > 0  N1 is N  1, gas(assocl, N1), eclass(Y + X, E).
assocl @ eclass(X + YZ, E), eclass(Y + Z, YZ) \ gas(assocl, N) <=> N > 0  N1 is N  1, gas(assocr, N1), eclass(X + Y, XY), eclass(XY + Z, E).
assocr @ eclass(X + Y, XY), eclass(XY + Z, E) \ gas(assocr, N) <=> N > 0  N1 is N  1, gas(comm, N1), eclass(X + YZ, E), eclass(Y + Z, YZ).
main(_) : eclass(1, E1), eclass(2,E2), eclass(3,E3), eclass(E1 + E2, E12), eclass(E12 + E3, E123), gas(comm,5), chr_show_store(true).
% hmm we're only getting to the first rule... I see. We can of course get around this. but not elegantly.
% hmm we're also not runnign fairly on deeper facts. Cripes.
pcong is only one step away from structure sharin? No. it really is just structure sharing… Hmm.
Hmm. gas is yet another form of demand based pulling. but only in CHR
A list of all things to retain in gas. Delete anything that fires. No we don’t have to delete. ok ok ok. This isn’t so bad. We just need to batch. reassert when done. Difference list useful? gas(L) <=> L = [X  L1], gas(L1), But now is there a fair chance for the rules? Maybe if we scramble the list. it’s a mess.
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint eclass(?,), eclass2(?,), col/1, kill/0, count/1.
cong @ eclass(T, E1) \ eclass(T, E2) <=> E1 = E2.
% rewrite rules.
comm @ eclass(X + Y, E) ==> eclass2(Y + X, E).
assocl @ eclass(X + YZ, E), eclass(Y + Z, YZ) ==> eclass2(X + Y, XY), eclass2(XY + Z, E).
assocr @ eclass(X + Y, XY), eclass(XY + Z, E) ==> eclass2(X + YZ, E), eclass2(Y + Z, YZ).
% made it way worse
% eclass(T,E) \ eclass2(T,E) <=> true.
% eclass2(T,E) \ eclass2(T,E) <=> true.
% To collect up new eclasses
collect @ eclass2(T,E), col(L) <=> L = [eclass3(T,E)  L1], col(L1).
done @ col(L) <=> L = [].
% helpers to cleanup eclass2
kill @ kill \ eclass2(_,_) <=> true.
killdone @ kill <=> true.
% helper to count eclasses
count @ count(N), eclass(_,_) <=> N1 is N + 1, count(N1).
% Take rhs list and inject them as CHR constraints
process([]).
process([eclass3(T, E) L]) : eclass(T,E), process(L).
% Do N rewriting runs
batch() : col(L), process(L). % print(L)
batch(0).
batch(N) : batch(), N1 is N 1, batch(N1).
init_add(N) : eclass(N,E), N1 is N  1, init_add_aux(N1,E).
init_add_aux(0,_).
init_add_aux(N,E) :
eclass(N, EN), eclass(EN + E, E2), N1 is N1, init_add_aux(N1, E2).
insert( T , E) :
ground(T),
var(E),
T =.. [F  Args],
length(Args, N), length(Es, N),
T2 =.. [F  Es],
eclass(T2, E),
maplist(insert, Args, Es).
main(_) :
% insert(f(a), Fa), insert(a, A), Fa = A, insert(f(f(a)), FFa),
% chr_show_store(true).
% eclass(1, E1), eclass(2,E2), eclass(3,E3), eclass(E1 + E2, E12), eclass(E12 + E3, E123),
N = 5,
init_add(N),
Num is 3**(N)  2**(N+1) + 1 + N, print(Num),
BNum is N,
time(batch(BNum)), kill, count(0), chr_show_store(true).
%rhs([]).
%rhs([T  L]) : flatten(T), rhs(L).
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint eclass(?,), eclass2(?,), col/1, kill/0, count/1.
insert( T , E) :
ground(T),
var(E),
T =.. [F  Args],
length(Args, N), length(Es, N),
T2 =.. [F  Es],
eclass(T2, E),
maplist(insert, Args, Es).
main(_) : insert(1 + 2 + 3 + 4, E), chr_show_store(true).
We can also perform rules like find(t1), find(t2) ==> E1 = E2. These will always finish since they only compress egraph.
It is quite possible that translating to integers and using CHR union find is faster.
Semi naive?
eclass2 is somewhat like new_eclass We could perhaps find delta_eclass
: use_module(library(chr)).
: initialization(main,main).
: chr_constraint eclass(?,), declass/2, eclass2(?,), col/1, kill/0, count/1.
% Take rhs list and inject them as CHR constraints
process([]).
process([eclass3(T, E) L]) : declass(T,E), process(L).
% Do N rewriting runs
batch() : col(L), process(L). % print(L)
batch(0).
batch(N) : batch(), N1 is N 1, batch(N1).
init_add(N) : eclass(N,E), declass(N,E), N1 is N  1, init_add_aux(N1,E).
init_add_aux(0,_).
init_add_aux(N,E) : eclass(N, EN), eclass(EN + E, E2), declass(N, EN), declass(EN + E, E2), N1 is N1, init_add_aux(N1, E2).
insert( T , E) : ground(T), var(E), T =.. [F  Args], length(Args, N), length(Es, N), T2 =.. [F  Es],
eclass(T2, E), maplist(insert, Args, Es).
cong @ declass(T, E1), eclass(T, E2) ==> E1 = E2.
cong2 @ eclass(T, E1) \ eclass(T, E2) <=> E1 = E2, declass(T,E1).
% rewrite rules.
comm @ declass(X + Y, E) ==> eclass2(Y + X, E).
assocl1 @ declass(X + YZ, E), eclass(Y + Z, YZ) ==> eclass2(X + Y, XY), eclass2(XY + Z, E).
assocl2 @ declass(Y + Z, YZ), eclass(X + YZ, E) ==> eclass2(X + Y, XY), eclass2(XY + Z, E).
assocr1 @ declass(X + Y, XY), eclass(XY + Z, E) ==> eclass2(X + YZ, E), eclass2(Y + Z, YZ).
assocr2 @ declass(XY + Z, E), eclass(X + Y, XY) ==> eclass2(X + YZ, E), eclass2(Y + Z, YZ).
% made it way worse
% eclass(T,E) \ eclass2(T,E) <=> true.
% eclass2(T,E) \ eclass2(T,E) <=> true.
% To collect up new eclasses
collect @ eclass2(T,E), col(L) <=> L = [eclass3(T,E)  L1], col(L1).
collect @ col(_) \ declass(_,_) <=> true.
done @ col(L) <=> L = [].
% helpers to cleanup eclass2
kill @ kill \ eclass2(_,_) <=> true.
kill2 @ kill \ declass(_,_) <=> true.
killdone @ kill <=> true.
% helper to count eclasses
count @ count(N), eclass(_,_) <=> N1 is N + 1, count(N1).
main(_) :
N = 2,
init_add(N),
Num is 3**(N)  2**(N+1) + 1 + N, print(Num),
BNum is N,
time(batch(BNum)), % kill(), count(0),
chr_show_store(true).
Is there a way to encode seminaive eval maybe? Even for datalog this is not clear you can. The folding of delta back into the main relationseems problematic.
leansmt egraph + clp(R) + clp(FD) + clp(B). How far from SMT is that?
Embedding into CHR
 TRS
 Prolog and CLP
 Graph trasnfomation
 Petri nets
GAMMA general abstract mnodel for multiset manipulation
Answer Set Programming s(CASP)
https://swish.swiprolog.org/example/scasp.swinb “Tabling and s(CASP) are quite different beasts. They both address reasoning in cyclic domains including negation. Tabling provides Well Founded Semantics where s(CASP) provides Stable Model Semantics. s(CASP) stresses creating an explanation. Tabling does not. Tabling scales a lot better than s(CASP). It all depends …”
https://gitlab.software.imdea.org/ciaolang/sCASP Constraint Answer Set Programming without Grounding Justifications for GoalDirected Constraint Answer Set Programming ERGO AI uses justification trees https://coherentknowledge.com/ using XSB
s(ASP) was just ASP https://personal.utdallas.edu/~gupta/ . S(CASP) includes constraints tutorial slides tutorail paper
Extralogical features
Database manipulation
swi sicstus database manip retract  take out of database assert  put into database/ set_prolog_falg dynamic predicates. recorded database
A = A, assert(foo(A)), A = x
what does this do. Does it make a clause foo(A).
or does it make foo(x).
Ah ok. The term is copied. So it makes the first on
a declarative alternative to assert in logic programming
fib(0,1).
fib(1,1).
fib(M,N) : M > 1, M1 is M  1, M2 is M  2, fib(M2, N2), asserta(fib(M2,N2)),
fib(M1, N1), asserta(fib(M1,N1)), N is N1 + N2.
% hmm. Infinite answers...
Program reflection. Partial evaluation.
Cuts and Such
cut green cut
findall bagor setof are aggregation of solutions. They are reifying predicates kind of.
Finding all Solutions to a Goal
Lambda
Oh sweet mysterious lambda
The minikanren evalo
eval(E1*E2, R) : eval(E1, E1R), eval(E2,E2R), copy_term(E1R,(E2R>Body)),
eval(Body,R).
eval(E,E).
One is tempted to attempt to use prolog variables for lambda variables. Requires extralogical copying primitives
copy_term
swipl lambda expressions.
[X] >> B
as lam(X,B)
.
the elpi paper argues for de bruijn levels?
% locally nameless
term(lam(X,X)).
% convert lam(X,X) form to gensym lam(fvar(x123),fvar(x123)) form
% I should just use numbervar/1
concrete( lam(X,B) , lam(X, B2) ) : gensym(x, X), debruijn(B, B2). % copy term maybe
% Turn X into bvar(N).
close(N, X, X, bvar(N)).
close(N, X, lam(Y, B), lam(Y,B2) ) : Y /= X, N2 is N + 1, close(N2, B,B2).
close(N, X, T, T2) : T /= lam(), T /= X,
T ..= [F  Args],
maplist(close(N,X), Args, Args2),
T2 .== [F  Args2].
abstract(X, T, blam(T2)) : close(0,X,T,T2).
instantiate(N, V, bvar(N), V).
instantiate(X)
% norm(T,T2)
% miller(T,T2). % :=: or some other special equals.
% miller(X,X).
% miller(blam(T1), blam(T2)) : miller(T1,T2)
% miller(app(F, Args), T) : var(F), reabstract(T, Args, F). % maybe throw a norm in there?
% miller(X,Y) : X ..= [F  Args1], Y ..= [F  Args2], maplist(miller, Args1, Args2).
% F @ [X,Y,Z] infix application
% norm(lam(X,X) @ 3, 3).
The question is, can lambda prolog be implemented as a library?
HiLog
My impression is this is a bit like “first order functional” programming. All predicates need names. You can achieve this via defunctionalization, lambda lifting, etc.
“X(a, b)
is just an (external) shorthand for the Prolog compound term: apply(X, a, b)
“
Alpha prolog
https://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/
Nominal logic https://arxiv.org/pdf/1012.4890.pdf nominal unification revsitied Urban
https://johnwickerson.github.io/dissertation.pdf “atoms” are a thing that are less free than unification vars but more free than ground terms. They are alpha renamable
freshness constraint a # t says that a appears in no subterm in t. a # X when X is a variable can’t be concluded.
freshness judgement equational judgements
nominal unification returns substitution and new freshness constrains
A relative of miller pattern. They can be encoded into each other it says and gives references
J. Cheney. Relating Nominal and HigherOrder Pattern Unification. J. Levy and M. Villaret. Nominal Unification from a HigherOrder Perspective
==(A \ X, B \ Y) : dif(A,B), X == swap(A,B,Y), A # Y.
A # A \ Y.
https://easychair.org/publications/preprint/DLVk Efficiency of a good but not linear nominal unification algorithm
Semantics
Completion semantics
Wellfounded Well founed semantcis 1991 WellFounded Semantics, Generalized two different ordering realtions, truth and knowledge. We always move from unknown to more known. well founded tutorial
Completion semantics
History
Resolution in automatc theorem provers came earlier. Kowalski and Colmerauer
Flotd nondeterminstic algorithms 9167 PLANNER Hewitt
Prolog 0 Prolog 1
metamorphisis grammars > DCG Dec10 prolog Ediburgh prolog
structure copying vs structure sharing
fifth generation computing
Extensions to unification prolog II Prolog III
CLP Jaffar Lassez 1987
Expert Systems
See Also:
 Databases Knowledge Representation https://en.wikipedia.org/wiki/Rete_algorithm
Lambda Prolog
lambda prolog page Implementations
 Teyjus  seems to maybe not be developed anymore
 elpi  alive and well. Coq metaprogamming
 Makam  a variant on lambda prolog with some cooll paper tutorials
elpi: fast embeddable lmabda prolog interpreter
 using de bruijn levels means pattern matching doesn’t need to do anything? elpi vs code extension
Install as opam install elpi
. Run as elpi test
to run with main query
main : print "hello world".
A little bit of an odd encoding. Why fact
? Oh I see. Because they have an outer loop that is inserting facts.
kind entry type.
type fact entry > o.
%type false o.
kind person type.
type kim,dana person.
type finished person > int > entry.
type cs_major, graduates person > entry.
fact (finished kim 102) & fact (finished dana 101).
fact (finished kim 210) & fact (finished dana 250).
fact (cs_major X) : (fact (finished X 101); fact (finished X 102)),
fact (finished (X 250)), fact (finished X 301).
false : fact (finished X 210), fact (finished X 250).
kind jar, bug type.
type j jar.
type sterile, heated jar > o.
type dead, bugs bug > o.
type in bug > jar > o.
sterile J : pi x\ bugs x => in x J => dead x.
dead B : heated J, in B J, bugs B.
heated j.
main : sterile J, print J.
type rain prop.
type wet prop.
type umbrella prop.
%mode (rain i).
%mode (wet i).
%mode (umbrella i).
rain : !, declare_constraint rain [_].
wet : !, declare_constraint wet [_].
umbrella : !, declare_constraint umbrella [_].
main : std.append [] [] X, print X,
std.length [1,3,4] L, print L,
std.take 2 [1,2,3,4] L1, print L1,
std.map [1,2,3] (x\ y\ y is 2 * x) L2, print L2,
std.iota 10 L3, print L3, % range of numbers
true,
Z is 1 i+ 2, print Z,
Z1 is (cos 3.0) + (int_to_real ((rhc "a") + (size "hello"))), print Z1,
fst (pr 1 2) One, print One,
dprint (pr (some 3)),
var V, var (V1 3) A B, print A, print B, % so it destructures a vairable application
some T == some T,
trace.counter "foo" I, print I, trace.counter "foo" I1, print I1,
%print app [lam (x \ const "a"), const "b"],
declare_constraint wet [W],
declare_constraint rain [R],
declare_constraint umbrella [U],
R = 7,
print "ok"
.
constraint rain wet {
rule rain <=> wet.
}
kind unit type.
type tt unit.
type lam (unit > unit) > unit.
main : (x\ x) = (y\ F y), print F,
(x\ x) = (y\ y),
% fails (x\ x) = (y\ F), % this is exists F, \x x = y\ F. Which is not solvable
% pi (y\ X = y) % fails
(x\ tt) = (y\ F2), print F2
.
main : (x \ x) = (x \ F_ x),
(x \ y \ x y) = (z \ G z), print G.
% church encoding
kind i type.
type zero, one, two ((i > i) > i > i) > o.
type add ((i > i) > i > i) > ((i > i) > i > i) > ((i > i) > i > i) > o.
zero F : F = f\ x\ x.
one F : F = f\ x\ f x.
two F : F = f\ x\ f (f x).
add X Y Z : Z = f\ x\ (X f (Y f x)).
main : two(T), one(O), add T T Z, print Z,
% add Q T T, print Q. % unification problem outside patern fragment. Flexflex?
add T Q T, print Q. % no prob
Some built in elpi files
 builtin surprising that even very basic stuff is defined in here.
 i+ i r+ mod div infix operations. + is overloaded it looks le
 regular expresions rex. Like Str module
 print dprint raw terms?
 quotation? https://github.com/LPCIC/elpi/blob/master/src/elpiquoted_syntax.elpi lam, app, const, clause, arg
 same_term same_var var name  geiventbaraibe, ground_term, closed_term, constant,
 if/3
 random.int
 int.map, std.string.map, std.string.set, std.map takes in a comp function,
 gc functions. trace,counter
 stdlib
 mem, exsits, map2, filter, fold, zip, unzip, intersperse, max, findall
std.do notation?
kind term type.
kind ty type.
type app term > term > term.
type lam (term > term) > term.
type arr ty > ty > ty.
pred of i:term o:ty.
of (app H A) T : of H (arr S T), of A S.
of (lam F) (arr S T) : pi x \ of x S => of (F x) T.
cbn (lam F) (lam F).
cbn (app (lam F) N) M : cbn (F N) M.
 named clauses
:clausename
 namespaces
 typeabbrev
 seperate compilation?
 w.elpi algorithm W?
 ndprover
look at teyjus test folders?
external
fields. Interesting
a tutorial on lambda prolog and is applications to theorem provin  Amy Felty thesis implementing lambda prolog in ciao prolog
Implementing Type Theory in Higher Order Constraint Logic Programming longer elpi paper. describes chr.
 macro directives
 delay directives
HO Unification
forall exists forall problems Raising vs Skolemization
LF
LF is of some relation to lambda prolog (being a prologish system with lambdas in it) although with some different aims. It is dependently typed (pi 2 I think?) in a way different from coq etc.
Twelf. dedukti. lambda  pi https://www.youtube.com/watch?v=XnZTADrsiHQ&list=PL2IiUBbPiuoY22PjECQscRQ81LaR0lgdh&index=2&ab_channel=TYPES2022 dedukti workshop Intermidate “assembly” for interchange between proof formats. Logical framework lambda pi  has dependent types. But not types that depend on types. Pi only quantifies over terms. kocheck  fast rust
beluga is this kind of twelf? beluga paper abella. These are all related I guess? abella might not be LF
Logical frameworks is a general vague concept I think. It is a system in which it is easy to model logical language nad inference rules. but ELF the edburgh logical fraemwork is more specific. Related to Pi2 a corner of the lambda cube.
The Next 700 Challenge Problems for Reasoning with HigherOrder Abstract Syntax Representations
Twelf
http://twelf.plparty.org/live/ http://twelf.org/wiki/About_The_Twelf_Project
Twelf is a depnedelty typed landguage that is also a logic programming langfuage. Because it has a totality checker and termination checker, prolog clauses can be considered proofs.
https://core.ac.uk/download/pdf/82649367.pdf Normalization for the SimplyTyped LambdaCalculus in Twelf
Rust Chalk Harrop
https://github.com/rustlang/chalk https://rustlang.github.io/chalk/book/
http://smallcultfollowing.com/babysteps/blog/2017/01/26/loweringrusttraitstologic/#typecheckinggenericfunctionsbeyondhornclauses https://internals.rustlang.org/t/blogseriesloweringrusttraitstologic/4673/12 internals thread
http://smallcultfollowing.com/babysteps/blog/2017/04/23/unificationinchalkpart2/ how chalk handles type normalization
LogTalk
logtalk is it’s own curious kind of universe. github repo It adds object oriented programming to prolog. https://logtalk.org/2009/12/08/lambdaexpressionsinlogtalk.html lambdas
Linear Logic Programming
See linear logic prolog rules destroy the body. Good for modeling state Chris martens ceptre
The interaction of linear logic and logic programming was very inlfluential on the concept of focusing
Coinductive Logic Programming
Actually fairly unrelated to inductive logic programming. Dealing with infinite terms and streams.
inductive logic programmingh
popper https://arxiv.org/abs/2005.02259 https://github.com/metagol/metagol metagol http://andrewcropper.com/ muggleton https://arxiv.org/pdf/2102.10556.pdf inductive logic programming at 30 hakank examples
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis. Includes a g4ip
Hakank symbolic function induction picat
Louise https://github.com/stassa/louise/blob/09a06e081b8933bbdb999424bf1a62673e88a3d6/src/louise.pl line 465 for metainterpreter prove. multi clause inductive learning. “inductive”
Metarules
P(A,B) : Q(A,C), R(C,B)
. second order qauntified variables
metainterpretive learning (MIL)  a prolgo metainterpreter
Probablistic Logic Programming
Abductive logic programming
https://en.wikipedia.org/wiki/Abductive_logic_programming
Infer ground facts given results
https://stackoverflow.com/questions/41274692/discussionaboutabductivelogicprogrammingvsanswersetprogramming “Any logic programing that supports hypothetical reasoning can support ALP”
assumez(P) : assertz(P).
assumez(P) : retract(P), fail.
abducible : (assumez(amount(glucose,low));assumez(amount(glucose,medium))),
(assumez(amount(lactose,medium));assumez(amount(lactose,hi))).
feed(lactose) : amount(glucose,low), amount(lactose,hi).
feed(lactose) : amount(glucose,medium), amount(lactose,medium).
% ? abducible, feed(lactose), listing(amount/2).
Abduction in Logic Programming  Denecker Kakas
A different variation https://swiprolog.discourse.group/t/nonmonotonicitydefeasibilitystrategiesandotherstuff/6038/23
/* SWIProlog 9.1.0 */
solve(true) > !.
solve((A,B)) > !, solve(A), solve(B).
solve(A) > {abducible(A)}, !, [A].
solve(H) > {clause(H, B)}, solve(B).
Theorem Proving
Leantap Jens Otten How to Build an Automated Theorem Prover. Invited Tutorial at TABLEAUX in London/UK
A simple version of this implemented in tau prolog Prdocues proofs translated to bussproofs latex
a pearl on SAT and SMT solving in prolog code
Backjumping is Exception Handling throw and catch implement backjumping for a sat solver
PRESS: PRolog Equation Solving System as described in the art of prolog book. also has an lp solver? Pretty interesting tehcniques. If a variable is in a single position, you can unfold the expression. 2. you can apply quadratic equations and stuff 3. Is it kind of a zipper to isolate a variable?
Dyckhoff g4ip
Misc
tar parsing in prolog rethinking prolog  oleg unification variables are an optimization
An interactive semantics of logic programming https://twitter.com/davidad/status/1567780900284387329?s=20&t=jW6J2ukuizpdkb11CCe3bQ
ICLP proceedings  lots of ASP stuff
https://github.com/mthom/scryerprolog/pull/838 scryer as a library?
.type Lifted = Lit {x : symbol}  Y {x : Lifted, y : Lifted} 
.decl r(x : Lifted, y : Lifted) .decl a(x : Lifted) r(x1, $Y(x1,x2)), a($Y(x1,x2)) : r(x1,x2).
defeasible logic programming
Okeefe  An Elementary Prolog Library some suggestions about unicode and other test stuff. Higher order operators
https://github.com/Anniepoo  Annie ogborn has some cool seeming tutorials
https://github.com/philzook58/lipsminikanren trying to use lips sccheme for minikanren in browser
https://github.com/aprologlang/aprolog alpha prolog. Nominal logic. What the heck is that again?
old title: prolog, scheme,racket, lambdaprolog, What the Hell is LogicT / Guanxi notes Minikanren, Unification, Resolution
BAP universal valures OCaml typeclasss system Oleg modellign typeclasses as prolog https://inbox.ocaml.org/camllist/20190904152517.GA2014@Melchior.localnet/ http://okmij.org/ftp/ML/index.html#trep
canonical structures and unification hints. Can we make a metaintepreter for this?
Hmm. Gauntlet thrown. Byrd is not sure how prolog can? do this stuff. https://www.youtube.com/watch?v=aS8oj2GXras&feature=youtu.be&ab_channel=LecturesbyProf.EadesatAU XSB prolog “complicated tabling and abstract interpretation tabling has a notion of subsumption? when are two calls the same? conductive logic over streams tree automata lvars. fixpoint over lattices
meta interpeter, sure. That’s one way to get com,plketeness What if one defunctionalizes the minikanren pause mechanism. What does it look like? Oh there’s a first order kanren paper that does this
Hmm. Could one do barliman style in lambda prolog? F, ex1, ex2, ex3. 2012 quine ppaper 2017 barliman paper
Tree automa, lvar, language for fixpoints. Not depth first, not breadth first, coniductive logic programming UT Dallas Abstract Interpretation ~ tabling. What does that mean?
nada Amin lambda kanren defeasible logic
proof checker running backwards
Scheme workshop
https://git.sr.ht/~sforman/PrologJunkyard/tree/master/miscellaneous/itc.pl interval tree clocks in prolog https://www.metalevel.at/trs/ knuth bendix completion https://arxiv.org/abs/1706.00231 auto differentiating using constraint handling rules
http://adam.chlipala.net/papers/MakamICFP18/MakamICFP18.pdf prototpying functional language using higher order logic programing makam chlipala https://www.tweag.io/blog/20191128PCFmakamspec/
Egraphs in prolog Unification variables give native union find data strcuture Hash consing  ?? equal( (t, E1), (t2,E2) : E1 = E2. % union find joining
Great. But then we need to possibly union find parents
t(x,y) ====> t(E1,E2)
equal( t1, t2 ) : lookup( t1 )
file:///home/philip/Downloads/ODonnell1987_Chapter_TermrewritingImplementationOf.pdf
https://core.ac.uk/download/pdf/81972151.pdf Logic programming with equations.
Eqlog  goguen and mesegaer?
assert_equal(EGraph, ,EGraph’) : lookup(t1, E1), lookup(t2, E2), E1 = E2, EGraph’ = EGraph assert_eqyal( ) : lookup(t1, E1), lookup(t2, E2)
rebuild(EGraph, EGraph’ ) :
rebuild(EGraph) : EGraph = ( , Map )
To miss a parent inference isn’t wrong, it’s just wasteful
If we do no hash consing, we do have to store every known term. We also need a map from Eclasses back to terms don’t we?
What if we broke apart. are association lists so bad? f(g(y)) ===> [ f(G) => F , g(Y) => G, y => Y ]
Or we could use the HEADS as keys in assoc. and then assoc list the leftovers. This isunder the assumptyiong that variables
== for search [ == , ]
We may want to prune duplicates occasionally If we interweave
Can we even achieve apttern matching without an index from ENodes => terms? Yessss…..? Given a pattern ( EClass, g(f(A)) ) We can look in g/1 for Eclass on the right hand side. For those matches, we build a subproblem of matching the pieces of the left hand size ENodes.
With tabling? Tabling gives us some kind of memoization
equal?(Egraph, t1,t2) : lookup(EGraph, t1, E1), lookup(EGraph, t2, E2). equal?(arg1( ) : eqwal?(args1, args2), assert_equal(EGraph, t1, t2)
Stratified prolog predciates. This euqation paper mentions this and this tabling thing mentions it https://www.swiprolog.org/pldoc/man?section=tablingnontermination
Datalog and program analysis https://www2.cs.sfu.ca/CourseCentral/721/jim/DatalogPaper.pdf  What you always wanted to know about datalog http://rightingcode.org/tutorials/popl20/ popl 2020  reasoning tools using llvm and z3 Z3 has a datalog style reasoning engine in it
First you need to get a program as a mapping
The Chase  get existentials in the head. Wisnesky says somethign to do with jkabn extensions and lawvere theory What was up with the notion of quantifiers as adjoints anyway? Maybe also some kind of completion? Datalog + Formulog Bap KB as datalog What
Typeclasses vs Canonical Structures. I don’t get it. Could I make a model? Maybe in prolog? Diamond problem Inheritance. What are typeclasses? “Kind of like prolog” Things are incompatible for some reason? Canonical structures add unification hints? https://hal.inria.fr/hal00816703v1/document canonical structures ofr the working coq user
So what is the synctatic condition that precludes search?
 nonoverlapping
Would it be more interesting to just What am I understanding here?
Canonical structures was suggesting that some kind of inconstency would manifest. Maybe lambda prolog gets us closer. We can have existential variables and such.
extensible unification
nat === (carrier nat_abGrp) : A === A.
nat == carrier(Eq) : Eq == natEq. carrier(Eq,nat).
nonunifiable(L) : all( /= , L ).
% haskell has no backtracking % every case has a cut. eq(tup()) : !. eq(tup(A,B)) : !, eq(A), eq(B)
%
eq(int, prim__equal_int). eq(tup(A,B), lambda( x, case( x, tup(a,b) => bool_and( apply(EqualA, a) , apply(EqualB, b ) ) ) ) ) : eq(A, EqualA), eq(B, EqualB). eq(tup(A,B), comp(and, par(EqualA,EqualB)))
eq(int). eq() eq(tup(A,B)) : eq(A), eq(B).
ord(bool). ord().
functor( maybe ) functor(compose(F,G)) := functor(F), functor(G)
traversable :
% superclass class(ord(A)) : call(ord, A), class(eq(A))
“diamonds appear evertwhere. See pullbacks” ~ Hale
Transcribing rules to prolog and coq. In Coq the cookbook is that you make an inductive. One constrctor per rule. If you call eauto, coq will perform prolog style backchaining search. See Chlipala You could write these as functions rather than as The data type is the proof structure.
Prolog is the same thing. It’s less imposing than coq though. You make predicates and : for each condition. Prolog has built in nondtermisnion and unification.
Tying rules in prolog. I did the pointfree simply typed lambda calculus type(fst, tup(A,B), A).
type(Gamma   plus(A,B) : nat ) :  
type(Gamma   A : nat), type(Gamma   B : nat) 
type(Gamma, lam(X, Body)   fun(A,B )) : type() , type( [X  Gamma] 
http://www.coli.unisaarland.de/projects/milca/esslli/comsem.pdf computational semantics. some interesting material here https://samples.jbpub.com/9780763772062/PrologLabBook09.pdf  prolog experiment in discretem mathemtiacs logic and computatilbitly
They start with defining a set of atoms like
var(x). var(y).
forall(x, stupid(x)).
https://www.youtube.com/watch?v=RwBiHLoQ3E4&ab_channel=PapersWeLove niko matsakis  lambda prolog
https://rustlang.github.io/chalk/book/recursive.html chalk. harrop formula
The Otten sequent calculus prover is very similar to a meta circular intepreter for prolog
Horn clauses (or harrop formula)
Lambdamu calculus and prolog. Focusing is relevant. Prolog has an imperative reading
Executing the Algebra of Programming
type(fst, prod(A,B) > A ). type(snd, prod(A,B) > B ). type(id, A > A).
interp(fst, tup(A,B), A ).
interp(snd, tup(A,B), B).
interp(id, A , A).
interp(fan(F,G), A, tup(B,C)) := interp( F, A, B) , interp(G, B, C).
interp(comp(F,G), A, C ) : interp( F, A, B ), interp(G, B, C).
interp(conv(F), A, B) : interp(F, B, A).
interp(cata(F) , fix(A) , C ) : interp(map(cata(F)), A, B) , interp(F, B, C)
% map instance for ListF interp(map(F), cons(A,B) , cons(A,B2) ) : interp(F, B, B2). interp(map(F), nil, nil).
% in constrast to map instance for list interp(map(F), [], []). interp(map(F), [X  XS], [Y  YS] ) : interp(F, X, Y), interp(map(F), XS, YS).
% convert to listf form listf([], nil). listf([A  XS ], cons(A,fix(L)) ) : listf(XS, L).
Different style
cata(F, fix(A), C) : map(cata(F), A, B), call(F, B, C). fst(pair(A,B), A).
comp(F, G, A, B) : call() , call()
% define what it means to be a functional relation functional( fst, fst). functional( snd, snd). function( )
% prolog is database stuff ~ relation algebra. It makes perfect sense.
interp( map )
Converting prolog to abstract machine form step( Stack Result ) :
oprolog veriffication
Warrne and Maier 1988 textboook proplog  propsitional goals only. datalog  constants only prolog  functional symbols
% tail recursive formulations factorial(N,F) : factorial(0, N,1,F) factorial(I,N,T,F) : I < N, I1 is I+1, T1 is T * I1, factorial(I1, N, T1,F) factorial(N,N,F,F).
hitchikers guide to prolog machine https://drops.dagstuhl.de/opus/volltexte/2018/8453/pdf/OASIcsICLP201710.pdf
ref a ref b
https://formal.iti.kit.edu/beckert/leantap/leantap.html Beckert posegga leantap https://link.springer.com/chapter/10.1007%2F3540363777_6 metacircular abstarct interpretation in prolog https://www.metalevel.at/acomip/
Pfenning constructive logic course http://www.cs.cmu.edu/~fp/courses/15317f17/schedule.html Programs as proof search He considers the prolog predictaes as the judgements themeselves As compared to considering the pile of predicates as entedcedents of a sequent Bottom up search ius forward reasoning, top down is backward reasonining bidrectional type checking  https://arxiv.org/pdf/1908.05839.pdf
Prolog semantics  Since prolog can not terminate you can take that denotational semantics perspective. https://www.swiprolog.org/pldoc/man?section=WFS well founded semantics.  True/False/unknown https://en.wikipedia.org/wiki/Wellfounded_semantics http://www.cse.unsw.edu.au/~cs4415/2010/resources/gelder91wellfounded.pdf http://dai.fmph.uniba.sk/~sefranek/links/FixPointSurvey.pdf fixpoitn semantics for logic programming a survey. melvin fitting Melvin fitting has a number of interesting bokos http://melvinfitting.org/
So prolog already has belnap bools in it.
What does it look like to mix prolog with exact reals?
Modes and determinism annotations.
Kowalski  hgistory of prolog https://www.researchgate.net/publication/277670164_History_of_Logic_Programming
tabling  Tabling is some kind of memoization. It is connected to bottom up strategies swi prolog https://www.swiprolog.org/pldoc/man?section=tabling https://www.metalevel.at/prolog/memoization https://biblio.ugent.be/publication/6880648/file/6885145.pdf tabling as a library with delimited control https://www.cambridge.org/core/journals/theoryandpracticeoflogicprogramming/article/abs/delimitedcontinuationsforprolog/DD08147828169E26212DFAF743C8A9EB delimitted continuations for prolog https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.294.9440&rep=rep1&type=pdf XSB extending prolog with tabled logic programming. XSB prolog is the most advanced tabling implementation (still? maybe that is old information) https://github.com/SWIProlog/tabledprologbook warren wrote a book draft https://www3.cs.stonybrook.edu/~warren/xsbbook/book.html ok This may not be being finished anytime soon Tabled typeclass resolution
http://www.covingtoninnovations.com/mc/plcoding.pdf  coding guidelines for prolog
https://swiprolog.discourse.group/t/algebrainprolog/1849  algerba in prolog https://github.com/maths/PRESS prolog equation solving system
scryer prolog  a rust based implemnentation . https://github.com/mthom/scryerprolog Interesting links Precise garbage collection in Prolog “Can Logic Programming Execute as Fast as Imperative Programming?”  Peter van Roy indexing dif/2 https://arxiv.org/abs/1607.01590 calls for if_ predicate debray allocator
https://wiki.nikitavoloboev.xyz/programminglanguages/prolog notes
https://mercurylang.org/documentation/documentation.html mercury
Names: Kowalski schrijver Nuemerekl Markus triska Wielemaker Warren Miller Nadathur melivn fitting
https://www.metalevel.at/prolog/theoremproving presburger and resolution https://www.youtube.com/watch?v=b2Px7cu2a68&feature=youtu.be&ab_channel=ThePowerofProlog term rewriting in prolog
https://dl.acm.org/doi/book/10.1145/3191315 Declarative Logic Programming: Theory, Systems, and ApplicationsSeptember 2018 Has another WAM tutorial in it
So
prolog modes
https://www.metalevel.at/prolog/attributedvariables attributed variables
https://sicstus.sics.se/sicstus/docs/latest4/pdf/sicstus.pdf sicstus prolog manual
Exact reals. The semantics already has this three valued logic flavor
partition([X,Y]).
partition([X,Y]) : partition([[X, X+Y / 2]]).
partition([[X,Y]) : partition( [X+Y/2 , Y ]).
interval(X), stuff.
sqrt()
Using prolog multiple answer streams is kind of like relying on haskell laziness. It’s this intrinsic lANGUAGE construct being used as a streaming datatpe Unclear if wise. Fast but inflexible and unclear. Too clever for own good.
clpq clpr
delmittied dontinuation. The contiuation is a goal stack. But is the continuation also catching choice point stack?
homoiconic. Term syntax is identical to
Maier and Warren
T_p, the immediate conseqeunce operator. Applying one round of prolog/datalog/ etc rules
Proplog
SMTlog Datafun  a fiunctional datalog https://www.cl.cam.ac.uk/~nk480/datafun.pdf https://www.youtube.com/watch?v=gC295d3V9gE datalog  stephenel diehl https://www.stephendiehl.com/posts/exotic04.html uZ  datalog in Z3 souffle doup
What are appli8cations of datalog program analysis. That points to analysis tutorial
Datalog ~ polynomial time in some sense. So application wise, it can be fixed point computations Or we can encode
send more money num(0) num(1) num(2) adder( )
https://sites.google.com/site/pydatalog/Onlinedatalogtutorial nqueens  they unroll it significantly.
Some examples http://cse.unl.edu/~riedesel/pub/cse413/des/doc/manualDES.pdf
ok farmer goat. As a path search basicaly
state(goat, foxm, chienbk, ) :
Parsing a grammar. This is an odd one. Encode positions of string in database. t(1,a,2). t(2,b,3). t(3,a,4). t(4,b,5). t(5,a,6). a(F,L) : t(F,a,L). a(F,L) : a(F,M), t(M,b,L). a(F,L) : a(F,M), t(M,a,L). DES> a(1,6) { a(1,6) } Info: 1 tuple computed.
Games?
Domain modeling with datalog https://www.youtube.com/watch?v=oo7mN9WXTw&ab_channel=%23pivorakLvivRubyMeetUp
https://github.com/ptarau/TypesAndProofs More theorem provers
binprolog  analog of CPS. Add a new parameter to every predicate
LD resolution
monoid of clauses  unfolding bin(A : BBBB) = (A>C : BBBB>C)
2020/9 Propagators.
Kmett. The Art of the Propagator https://dspace.mit.edu/bitstream/handle/1721.1/44215/MITCSAILTR2009002.pdf?sequence=1&isAllowed=y
The gecode manual https://www.gecode.org/doclatest/MPG.pdf
Adding constraints or smt. I have a seperate store for them (in the state)? explicit probe annotations to check still satisfiable.
9/1/20
I was looking at prolog again. Jesus nothing changes.
What are the good programs. The art of prolog has an open access link
Difference lists are cool. They really are similar ot hughes lists. Or al ist that keeps a pointer to it’s end
Using it for theorem proving is cool. Where are those examples? The lambda prolog book has some exmaples. There is a propsitional satisfiabilioty prover in art of prolog. Propositional solver in powr of prolog https://www.metalevel.at/prolog/theoremproving http://vidalrosset.net/g4i_prover.html http://jensotten.de/tutorial_cade19/slides/prover_tutorial_CADE19_2.pdf
nomial logic programming https://arxiv.org/pdf/cs/0609062.pdf alphaprolog. Chris mentioned this nominal thing as nother way of dealing with binders
Datalog  souffle. Reading gorup paper https://arxiv.org/pdf/1207.5384.pdf. Sttratification. relations indexed on program point/ abstract state of program point. Interval analysis encoded in binary to datalog?
425/20 I was playing with prolog recently. Pretty cool
What is the deal with scheme and racket? i just don’t have the revelation.
I was looking at disjoint set data structures again https://en.wikipedia.org/wiki/Disjointset_data_structure#cite_noteConchon20079
Kmett’s latest propgator talk was mentioning using group actions somehow in unification? https://www.youtube.com/watch?v=s2dknG7KryQ
george wilson  https://www.youtube.com/watch?v=nY1BCv3xn24 intutition for propagators.
http://hackage.haskell.org/package/discrimination0.3 What the hell is this? Fritz Henglein.
http://conway.rutgers.edu/~ccshan/wiki/blog/posts/WordNumbers1/
https://www.reddit.com/r/haskell/comments/a9yze4/is_there_an_arraylike_data_structure_which_gives/
interesting comments
https://www.lri.fr/~filliatr/puf/ a coq formalization of a persistent union find data structure. They use persistent arrays, which do some kind of rebalancing operation.
Persistent data structures. Wassup with them?
2019
Combine LogicT with an OSQP monad for branch and bound
http://overtond.blogspot.com/2008/07/pre.html
https://github.com/dmoverton/finitedomain
https://blog.plover.com/prog/haskell/monadsearch.html
https://www.schoolofhaskell.com/user/chowells79/evenmoremoney
https://blog.jle.im/entry/uniquesampledrawingsearcheswithlistandstatet
Select Monad
Branch and Bound
Ed kmett is up to funny business
https://www.youtube.com/watch?v=ISNYPKiE0YU&t=916s
Propagators
https://www.sciencedirect.com/science/article/pii/S1571066105805444
Typed logical variables in haskell by Claesson and Ljundogjgklds
https://people.seas.harvard.edu/~pbuiras/publications/KeyMonadHaskell2016.pdf
Also by claesson, the key monad paper.
http://www.cse.chalmers.se/~koen/
Interesting guy. He is coqauthor with hughes on quickcheck.
Atze van der Ploeg is both Key monad paper and reflection without remorse. They have an FRP paper that sounds interesting
He metnioend a number of interesting things. He’s doing very reference heavy code? Kanren.
He mentoins intension vs extensional equality. Judgemental eqaulity is the one inside the type checker. Is it ~ ? And intwnsional equality is the one within the language itself, that is :~: . Extensional. nuPRL starts with an untyped lambda calculus and then you teahc the system typing derivations? What is nuPRL’s deal
Unionfind algortihm  as part of unification?
nerualkanren, synquid. Two program synthetsis projects. Synquid uses liquid typing
Oleg Shen paper using efficient charing for logic programming
https://wwwps.informatik.unikiel.de/~sebf/data/pub/icfp09.pdf
http://sebfisch.github.io/explicitsharing/
Maybe sebastein fischer is the name I should assicuate more storngly?
https://sebfisch.github.io/research/
The Curry language. Haskell + logic. Egison has weirdo patterns too. Multiple patterns can match? Nonlinear pattern require. Realted to view patterns? view patterns are a weirod syntax. realted to guard patterns. DOn’t need to introduce intermediate names
https://people.eecs.berkeley.edu/~necula/autded/lecture15tactics.pdf
View patterns might be a way of getting something like the Agda .x syntax, where something is forced to be something by unification?
https://gitlab.haskell.org/ghc/ghc/wikis/viewpatterns#Relatedwork
Kmett mentions a “octagonal” domain. What the hell is he talkiing about. He also moentions interval and polyhedral which makes more sense
https://wwwapr.lip6.fr/~mine/publi/articlemineHOSC06.pdf
Huh. Interesting. It is in between power of polyhedral and interval. allows sums/differences of two variables. I think I’ve heard this called difference logic. This paper also mentions galois connections. Galois connections are studied in the context of abstract interpetation?
https://arxiv.org/pdf/1807.08711.pdf
Using Agda and galois connections. Interestign example of sets of even and odd numbers.
This other paper does an interesting thing of defining division in terms of a glaois connection. Might we also get a good definition of fractions that way? a fraction t ~ m/n is a “number” such that forall z. x <= y > x * t * n <= y * m? There is an notion of negative numbers, fractions, etc as reified weirdo operations that can’t be solved yet. Hmm. Yeah, This jives with galois theory doesn’t it. That book I was reading was talking about field extensions. Or number systems being invented to make more equations solvable. The reals make ? solvable. fractions make division solvable. Complex makes roots solvable. finite field extensions make simple algerbaic equations solvable.
https://www.sciencedirect.com/science/article/pii/S1567832612000525
% —————————————————————– % leanseq.pl  A sequent calculus prover implemented in Prolog % —————————————————————–
% operator definitions (TPTP syntax)
: op( 500, fy, ~). % negation : op(1000, xfy, &). % conjunction : op(1100, xfy, ‘’). % disjunction : op(1110, xfy, =>). % implication : op( 500, fy, !). % universal quantifier: ![X]: : op( 500, fy, ?). % existential quantifier: ?[X]: : op( 500,xfy, :).
% —————————————————————– prove0(F) : prove([] > [F]). % —————————————————————–
Oliveira, that same guy as the Search monad and some other thingds
I suppose perhaps there is something similar happening in functional programming. to make recrsuively defined functions solvable, you need to extemnd the language with a Ycombinator or some of fixed point operator.
Interval airthemteic in a theorem prover. That is a way of getting sets. Min and Max. Interesting
This is also a pleasant by Backhouse
http://www.cs.nott.ac.uk/~psarb2/G53PAL/FPandGC.pdf
indirect equality
m=n === forall k. k <= m <=> k <= n
Galois connection between convex hulls of integer points? There is a sequence of abstractions for integer programming. You can turn dimension by dimension into integer so there are 2^D different domains to talk about. And there is this grid of connections that forms a lattice itself? Like the top is the completely R^D, and the bottom is Z^D. Using these connections is the branch and bound procedure.
Floor and Ceil are also galois connections. Maybe also round? I had been thinking in terms of ibjects being individual numbers, not convex sets of numbers. Convex sets does tie in much better to categorical thinking
http://www.cs.tau.ac.il/~msagiv/courses/asv/absint1.pdf
An interesting paper tutorial on galois connections. V cool.
monotone functions between are like natural tranfromations?
One place used dup as the adjunction to max.
There may be more to galois connections than adjunctions, since they are assuming a meet and join operation. Some interesting doncturctions like the porduct of galois connections.
 Edward Kmett  Logic Programming à la Carte
minikanren is strongly unification based. it is using search for the unification map. In simplest form [UniMap]
https://github.com/JeffreyBenjaminBrown/learnlogict
https://www.msully.net/blog/2015/02/26/microkanren%CE%BCkanreninhaskell/
https://gup.ub.gu.se/file/207634 logic typed variable claesson
http://dev.stephendiehl.com/fun/006_hindley_milner.html#unification unification.
Pure, Declarative, and Constructive Arithmetic Relations (Declarative Pearl)
https://roche.info/articles/20170617genericunification unificationfd .
https://winterkoninkje.dreamwidth.org/100478.html
unificationfd inserts itself in the same position Fix does.
Lattices. Subsumption lattice for unufication. More and less general partial order. meet and join. top and bottom
Notes from 2017 Resolution and unification
So I was learning about about minikanren. There are some videos online. Minikanren is a logic programming language (like Prolog) that embeds easily into other languages because it has a small core.
Logic programming is weird mainly (partially) because you define relations rather than functions. Relations do not have a input output relationship like functions do. In a sense they are like functions where you get to choose which thing is output and which things are input. Pretty crazy.
The most obvious way to do this to me is to make every function a bag of functions. Just write one function for every possible choice of output variable. These functions may need to be nondeterministic, outputting multiple possibilities, for example for y = x^2 gives x = +sqrt(y) or sqrt(y). However, this isn’t really how logic programs are written. Instead they deduce how to use a relation as a function.
I find most intro to prolog stuff off putting, talking about socrates(man), when that is not a problem I have ever given a crap about.
Resolution is the classical logic version of function composition.
a> b and b>c can be combined easily into a function a> c.
Implication in classical logic is weird. It translates to
a>b ====> (not a) or b
When a is true, b has to be true. When a is false, b can be true or false.
For the statement a implies b to be true then it needs to evaluate to false only when a is true and b is false
not (a and (not b))
using De Morgan’s law you can distribute nots turning ands into ors.
Then that becomes
(not a) or b.
If you have
((not a) or b) and ((not b) or c)
it does not matter what b is really because either b or not b will be false
so this is equivalent to
(not a) or c
since at least one has to be true to make the whole expression true
Unification
Predicate logic allows propositions to depend on variables. Think Prolog.
A simple question given two expressions is whether there are values of the variables that make the expressions equal.
I do this in my head sometimes when I’m looking a a parametric haskell type.
The type variables need to be matched up with two different expressions.
Sometimes this can be too hard to do in my head, especially when the type variables end up being functions. So there is need for an algorithmic procedure. I mean, also because you want a computer to do it.
First off, let’s suppose we have the two expressions in tree form.
Nodes can be Or, And, Predicates, Not.
We’ll want them in some canonical form too so that we don’t get tripped up by the commutativity or distributivity of Boolean operators
We need to collect up a bucket of deduced equivalences as we go down the trees of the two expressions. Whenever we hit a variable, we check if we have a substitution in our bucket. If so, replace it. If not, we put into our equivalences that variable is equal to whatever the other expression has in that place. When we hit something that trips us up, we announce failure and the expressions couldn’t be unified.
The prolog algorithm is roughly guess a pair of terms in the goal (the executing state) and knowledge base (the code base) that will unify. Try to unify them. If they do, then use resolution to get rid of those terms.
Like what if we reflected into Eisenberg’s Stitch? Or what was Weirich’s thing? People have been talking about intrinsically typed systemF lately.