Hacker News Reader

Hacker News

Comment by matthewfl | Hacker News Reader

Full thread

matthewfl

It's nice to discover my PhD research trending on Hacker news.

https://matthewfl.com/phd

https://matthewfl.com/papers/mfl-dissertation.pdf

https://github.com/argolab/dyna3

https://www.youtube.com/watch?v=sXRvba2yjY0

View on HN

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?

The dissertation covers extensive details, but on your last point at least it describes:

> 2.2.1 Evaluation by Default. One of the major syntactic differences between Dyna and other logic programming languages is that Dyna evaluates an expression in place by default. The reason for this change is that most terms have a meaningful value, much like how a function returns a value in a functional programming language. Conversely, in logic programming languages such as Prolog or Datalog, terms only “return” the value of true.

Prolog (and Datalog) plays fast and loose with the original FOL terminology from which its own is derived, so e.g. a "term" in Prolog is both an "atomic formula" or "atom" in FOL, and a "first order term" (or just term) in FOL. In FOL the sets of function and predicate symbols are distinct and disjoint, but in Prolog they are not, and my guess has always been that this is the reason that everything gets called a "term" (and "atom" ends up replacing "constant").

And nothing gets evaluated, either in FOL or Prolog/Datalog, so I'd like to nitpick and say that terms don't '"return" the value of true', they are only transformed, by unification and -in the case of Prolog- by SLD-Resolution. The interpretation of a Prolog program eventually "returns" the result of a proof, which is usually 'true' or 'false', but sometimes 'yes' or 'no'; but nothing in a Prolog program can really be seen as "returning" anything. It's a peculiarity of logic programming languages that I think takes a while for most programmers to get their heads around.

So a logic programming language that returns values and replaces expressions by their values is a substantial departure from Prolog syntax and semantics. But, you know that judging from the excerpt above.

Pedantry!

It's not pedantic at all. Interpreting terms as "themselves" and term ordering is core to Herbrand interpretation and unification, as you know very well.

Yes but not everyone is up for a logic programming lecture on a Sunday :)

Author here.

Chapter 2 of my dissertation covers a lot about the syntax of Dyna https://matthewfl.com/papers/mfl-dissertation.pdf

As refset said in the other comment, In Dyna, terms return values like a function in a functional programming language. Hence, when you write

  word(I)

this returns the value defined by the `word` function. E.g.

  word(0) = "Hello".

This is different from typical logic programming languages like Prolog in that if you write

  foo(X, bar(Y))

then you are "calling" the term `foo`, but then `bar` ends up being a structured-term that gets unified with the second argument of `foo`. Prolog provides this shortcut as "calling" `bar` doesn't make sense in this case, as `bar` only would return the value `true`, which isn't particularly useful.

In Dyna, we provide square brackets to create structured-terms as both calling the term "bar" and creating the structured-term bar can be useful. E.g. the Prolog expression `foo(X, bar(Y))` would be equivalent to the dyna `foo(X, bar[Y])`.

For the aggregator `max=`, this is looping over the different possible values on the right-hand-side and selecting the value that is the max. Hence in

  phrase(X,I,K) max= phrase(Y,I,K) \* rule(X,Y).

this is looping over the variable `Y` and selecting the one that is maximal. Using `max=` on

  phrase(X,I,I+1) max= rule(X, word(I)).

is done because we want all of the right-hand-sides to use the same aggregator so that we can aggregate between different rules that contribute to `phrase/3`.

Thanks! Honesty: I don't know if I have the time to read a dissertation (or two, or three, judging from the references on the article above). I will try to make some time because Dyna looks interesting.

Regarding 'max=' I guess then phrase/3 is calculating... the string of words I with maximum probability? Which IIUC is bound to Y? If so, that's cool. I've done that with DCGs in the past, but the functional syntax makes it ... look more like a function :)

>> E.g. the Prolog expression `foo(X, bar(Y))` would be equivalent to the dyna `foo(X, bar[Y])`.

I'm guessing that's for convenience? I think it's not rare for functional languages to have a "quoting" (?) mechanism like that?

Edit: Might be a good idea to add an example that also shows a program's output, alongside its source code.

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.)

Reply on news.ycombinator.com