WOLFRAM NOTEBOOK

In[]:=
Clear[g]
FixedPoint[Replace[XXXX]]
NestList[ReplaceList[XXXX]]
In[]:=
SubsetReplace[{f[a],g[b],f[c],g[d],g[c]},{g[x_],g[y_]}->Splice[{f[x],g[x+y]}]]
Out[]=
{f[a],f[b],g[b+d],f[c],g[c]}

How to represent an evaluation path?

What to with its “tentacles”?
FindEquationalProof
In[]:=
x=x+1
$RecursionLimit
:Recursion depth of 1024 exceeded during evaluation of 1+x.
Out[]=
Hold[1+x]
In[]:=
x=.

cf. Monte Carlo sampling / probabilistic programming

Basic logic programming operation:

FindReplacePath[{a->b,c->d},x,y]
FindReplacePath[{a->b,c->d},x,pattern]

? SPARQL query

Find an intermediate on a path
RDF triple : tagged edge
Relation vs. event
x->relation->y
Triplestore is a hypergraph with ternary hyperedges {x, relation, y}
Can be a schema for the triples
A query finds a path (or several); or a subgraph
​

Proof representation

In[]:=
ProofObject
Logic: EquationalLogic
Steps: 11
Theorem:
∀
x
g[e,x]x
["Properties"]
Out[]=
{Axioms,Logic,ProofDataset,ProofFunction,ProofGraph,ProofGraphWeighted,ProofLength,ProofNotebook,Theorem}
In[]:=
ProofObject
Logic: EquationalLogic
Steps: 11
Theorem:
∀
x
g[e,x]x
["ProofGraph"]
Out[]=
In[]:=
ProofObject
Logic: EquationalLogic
Steps: 11
Theorem:
∀
x
g[e,x]x
["ProofDataset"]
Out[]=
›
›
Proof
Construct
{Axiom,2}
Orientation
-1
Rule
g[g[x1_,x2_],x3_]g[x1,g[x2,x3]]
Side
1
Subpattern
g[x1_,x2_]
MatchingConstruct
{Axiom,1}
MatchingOrientation
-1
MatchingRule
g[x1_,e]x1
MatchingSide
1
The proof shows how we instantiate laws of inference
Unify[lhs->f(X,Y,Z),rhs->f(g(Z),j(W),h(Y,a))]->[Z->h(Y,a),Y->j(W),X->g(Z)]

Other examples of potential proofs

Simplify

Chemical reactions

States: chemical graphs
Tokens: bonds ??

Game graphs

Tiling

Recursion

Evaluating Fibonacci : you want to collect all the leaves
Search analog: you want to pick a single leaf
In[]:=
NestGraph[x|->If[x<2,{1},{x-1,x-2}],6,10,VertexLabelsAutomatic]
Out[]=

Puzzle solving

State graphs

[ Modelica standard ]
[ similar to Petri nets ]
Hanging differential equations off the discrete graph
[Acausal modeling]
(Represents system of equations as a graph)

DFAs etc.

Products of machines / wreath products etc.

Category theory

Monoidal category : [n-ary functions]

Elements

Tokens
States
Events
Reference frames / goals

Strings: linked lists [could have a reconnection event]
Expressions: require backfilling events to reknit the results into a superexpression

Tokens could contain patterns: then one has do pattern unification to apply an event

NestGraph deterministic or not

(Same as token deduplication?)

Deduplication is the equivalent of pre-caching everything, whether or the thing occurred to memoize

Are tokens always knitted into states through atoms

Possible Outputs

Add up every leaf ( e.g. recursive function evaluation)

Find a winning path (search; logic programming; etc.)

Find a probability distribution over paths (~ Monte Carlo ; probabilistic programming )

Proof assistant [ human assisted path finding ]

Language Design

We have expressions, but we do not have a way of representing the process of transformation

Where does a pattern apply? [ AKA how does a state decompose into tokens? ]
Wolfram Cloud

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.


I understand and wish to continue anyway »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.