Can you please explain Dyna? I'm trying to understand it using what I know about Prolog. For example, what does this rule (?) do?
phrase(X,I,I+1) max= rule(X, word(I)).
What is the 'max=' operator(?). Is phrase/3 an interface to Definite Clause Grammars as in Prolog?
How about this one?
phrase(X,I,K) max= phrase(Y,I,K) * rule(X,Y).
Is the * operator (?) to be interpreted as a multiplication? As a disjunction or other logical operation? If a multiplication, what is it multiplying?
Thanks!
Edit: I'm struggling with the Fibonacci example. The text says that Dyna 2.0 uses unification "like Prolog" but I can't make head or tails of how the first-order terms in the following rule would unify:
fib(N) := fib(N-1) + fib(N-2).
It seems that 'N-1' and 'N-2' are meant to be replaced by their values. In that case, when does unification happen? Are the terms evaluated, then their values unified? Obviously those values would (eventually) be constants, so where is the unification happening? Is this something to do with lazy evaluation? Or is unification here only used as a value-passing mechanism, to propagate the value of N through the expression?
It's very, interesting work. People keep wondering about production use. What they don't realize (or maybe do) is that going from high-level descriptions to efficient execution on imperative GPU's is solving a series of NP-hard problems, like ASIC synthesis. A few tools, like Cray's Chapel, do a pretty good job when given more specific information, though.
My background was high-assurance systems that are provably correct. The field found that designing something for easy analysis and verification was the opposite of for efficiency. So, the solution became to verify the high-level description (formal specifications) first. Then, verify equivalence to a lower-level, efficient form which was probably designed side by side with the other one to make that easier.
Having only read the abstract and example code, I see your work being most valuable as what we called an "executable, spefication language." Those were specs or models close to original, mathematical description that could actually run for exploration and testing. They were also, in theory, easy to modify by the researcher who could focus on intended behavior rather than low-level code.
You are already using transformations to produce low-level implementation. My brainstorm would be to do a bottom-up approach of making common operations on GPU's, in libraries like Jax, and rules about how to integrate them. Then, synethesize combinations of them with constraints on combinations with the system further specializing the components as it went on. (It will be interesting to see what you did.)
I think HLS on ASIC's, Cray's Chapel, and high-level libraries in machine learning show such an approach could make implementations fast enough to test theories on small models. I think someone should build on these concepts trying to connect them to primitives in Chapel or Jax or something already designed to itself synthesize or abstract away many low-level details. Then, implement pieces of common, useful models in it with pre-synthesized implementations.
Shorter version: I think it's neat work.worth further exploration which might accelerate development and validation of ML algorithms even with sub-optimal, runtime performance.
(And I still haven't read the papers. This is just independent brainstorming I do first to see if our ideas are converging any which has its own value.)
This language seems quite similar to Scallop [1], which was recently posted to HN [2]. Both are extensions of Datalog to arbitrary semirings, meaning that they generalise assigning merely true or false to relational statements, allowing probabilistic reasoning and more (almost arbitrary tagging of statements). Scallop is further focused on being differentiable and being able to integrate Scallop code into a PyTorch function. Both seem to have quite a bit of work put into them and have JIT compilers (Scallop also has a GPU implementation). I like the sound of "I have further modernized Dyna to support functional programming with lambda closures and embedded domain-specific languages." [3]
Same lineage (weighted/semiring logic programming for ML), but different system. Francis Landau’s work (Dyna) is a term rewriting implementation is of a weighted logic language with bag relational semantics, dynamic programming, and a tracing JIT. Scallop is a Datalog style neurosymbolic language built on provenance semirings with differentiable/relaxed semantics intended for e2e training with NNs. Consider Scallop a variation branch in the lineage optimized for differentiable neurosymbolic learning vs Dyna is a more general weighted logic programming framework with a different execution mode
I'd be fascinated to hear about the author's experience using Clojure for something as complex as a compiler. Was the lack of types an issue? Or was the simplicity and flexibility of the language worth the tradeoff?
I just finished a bit of spelunking in the Clojure Repo of Dyna3, and I got the distinct feeling that I had just stumbled upon an alien artifact from the future.
The focus of this work was a research project. IMO, a mature system would require a several more person years of work. However, there is nothing stopping you from using it in a production system if you find it useful (there is a python, clojure, and java api).
[+] [-] matthewfl|7 months ago|reply
https://matthewfl.com/phd
https://matthewfl.com/papers/mfl-dissertation.pdf
https://github.com/argolab/dyna3
https://www.youtube.com/watch?v=sXRvba2yjY0
[+] [-] YeGoblynQueenne|7 months ago|reply
How about this one?
Is the * operator (?) to be interpreted as a multiplication? As a disjunction or other logical operation? If a multiplication, what is it multiplying?Thanks!
Edit: I'm struggling with the Fibonacci example. The text says that Dyna 2.0 uses unification "like Prolog" but I can't make head or tails of how the first-order terms in the following rule would unify:
It seems that 'N-1' and 'N-2' are meant to be replaced by their values. In that case, when does unification happen? Are the terms evaluated, then their values unified? Obviously those values would (eventually) be constants, so where is the unification happening? Is this something to do with lazy evaluation? Or is unification here only used as a value-passing mechanism, to propagate the value of N through the expression?[+] [-] nickpsecurity|7 months ago|reply
My background was high-assurance systems that are provably correct. The field found that designing something for easy analysis and verification was the opposite of for efficiency. So, the solution became to verify the high-level description (formal specifications) first. Then, verify equivalence to a lower-level, efficient form which was probably designed side by side with the other one to make that easier.
Having only read the abstract and example code, I see your work being most valuable as what we called an "executable, spefication language." Those were specs or models close to original, mathematical description that could actually run for exploration and testing. They were also, in theory, easy to modify by the researcher who could focus on intended behavior rather than low-level code.
You are already using transformations to produce low-level implementation. My brainstorm would be to do a bottom-up approach of making common operations on GPU's, in libraries like Jax, and rules about how to integrate them. Then, synethesize combinations of them with constraints on combinations with the system further specializing the components as it went on. (It will be interesting to see what you did.)
I think HLS on ASIC's, Cray's Chapel, and high-level libraries in machine learning show such an approach could make implementations fast enough to test theories on small models. I think someone should build on these concepts trying to connect them to primitives in Chapel or Jax or something already designed to itself synthesize or abstract away many low-level details. Then, implement pieces of common, useful models in it with pre-synthesized implementations.
Shorter version: I think it's neat work.worth further exploration which might accelerate development and validation of ML algorithms even with sub-optimal, runtime performance.
(And I still haven't read the papers. This is just independent brainstorming I do first to see if our ideas are converging any which has its own value.)
[+] [-] versteegen|7 months ago|reply
Going to try it out.
[1] https://www.scallop-lang.org/
[2] https://news.ycombinator.com/item?id=43443640
[3] https://matthewfl.com/research#phd
[+] [-] ProofHouse|7 months ago|reply
[+] [-] refset|7 months ago|reply
There are some epic looking Clojure namespaces here, e.g. this JIT compiler https://github.com/argolab/dyna3/blob/master/src/clojure/dyn...
[+] [-] brokencode|7 months ago|reply
[+] [-] aeonik|7 months ago|reply
https://github.com/argolab/dyna3
[+] [-] jdnier|7 months ago|reply
[+] [-] tomrod|7 months ago|reply
[+] [-] matthewfl|7 months ago|reply
[+] [-] sieabahlpark|7 months ago|reply
[deleted]