From the title I expected this to be about differentiating DCG grammars themselves. That is actually a technique for matching regular expression [1]; now I wonder can it also be applied to DCGs (or a restricted form like PEGs).
DCGs are lovely things that allow you to implement a toy example quickly but then the dragon appears and gobbles you up..
The scent of dragon's breath can already be seen in this example in a couple of places.
In the first place, using DCGs generatively is very interesting. It implies that you can write programs that generate strings as easily as parse them.
But the question of which grammars are reversible this way is very thorny. Even worse, this question is highly context specific. A grammar might be reversible in one context and not in another. Reversibility is also very delicate. Adding trivial changes to a parser can suddenly make it no longer reversible.
The second scent is the way that apparently small limitations in the Prolog language start to have very large implications in terms of program complexity. Since these limitations are inherited by the DCG framework itself, it quickly becomes necessary to either lose the attractive identification of Prolog expressions with syntax trees or to wind up with an explosion in program size.
An example appears in this article. The differentiation for each of the functions exp, sin, cos and tan involves a separate definition of the chain rule. For instance, we have
and then simply define derivatives of each function without the chain rule.
We can't do that, however, because Prolog doesn't support unification of functors. We could patch that if we started referring to function application with more elaborate syntax by parsing "sin(exp(x))" as application(sin, application(exp, x)) so that we could unify on sin, but this quickly obscures the syntax tree and removes the delightfully direct nature of DCGs.
We see problems popping up in the simplification as well. The problem of simplification is that you can wind up simplifying in circles which makes a depth first approach as used in Prolog very dangerous. The authors insert a cut to avoid this, but this also suddenly makes the entire system non-reversible.
The fundamental problem is that logic programming in the form of Prolog is practical precisely because of these limits. If you want more expressive power, you need to start talking about much more than unification and depth first search. At that point, you suddenly wind up with mechanisms like coordinate types which have the full expressivity of formal logic, but lose the simple execution of Prolog; simple type checking becomes undecidable.
> We can't do that, however, because Prolog doesn't support unification of functors. We could patch that if we started referring to function application with more elaborate syntax by parsing "sin(exp(x))" as application(sin, application(exp, x)) so that we could unify on sin, but this quickly obscures the syntax tree and removes the delightfully direct nature of DCGs.
Would the =../2 predicate help? It allows for you to unify functors without wrapping them in something like your application(exp, x) example. Not sure how it would interact with DCGs, though - never took more than a superficial glance at them.
It follows from Turing completeness. See https://en.wikipedia.org/wiki/Turing_completeness. It takes very little for a system to become Turing complete. And once it is, you can include arbitrary computations. Proving that they stop is impossible in general due to the well-known Halting problem.
The flip side is that such systems can still be practically useful. You just have to manage your type complexity, much like you already manage your runtime complexity.
DCGs are now up for formal adoption in the Prolog ISO specification[1].
If at all possible, please encourage your national ISO representatives to vote for its adoption.
For the US it's ANSI SC 22 WG 17.
[1]: https://www.iso.org/standard/83635.html
From the title I expected this to be about differentiating DCG grammars themselves. That is actually a technique for matching regular expression [1]; now I wonder can it also be applied to DCGs (or a restricted form like PEGs).
[1] https://en.wikipedia.org/wiki/Brzozowski_derivative
Ah, yes. I remember this well.
DCGs are lovely things that allow you to implement a toy example quickly but then the dragon appears and gobbles you up..
The scent of dragon's breath can already be seen in this example in a couple of places.
In the first place, using DCGs generatively is very interesting. It implies that you can write programs that generate strings as easily as parse them.
But the question of which grammars are reversible this way is very thorny. Even worse, this question is highly context specific. A grammar might be reversible in one context and not in another. Reversibility is also very delicate. Adding trivial changes to a parser can suddenly make it no longer reversible.
The second scent is the way that apparently small limitations in the Prolog language start to have very large implications in terms of program complexity. Since these limitations are inherited by the DCG framework itself, it quickly becomes necessary to either lose the attractive identification of Prolog expressions with syntax trees or to wind up with an explosion in program size.
An example appears in this article. The differentiation for each of the functions exp, sin, cos and tan involves a separate definition of the chain rule. For instance, we have
The problem here is that we want to write something like this: and then simply define derivatives of each function without the chain rule.We can't do that, however, because Prolog doesn't support unification of functors. We could patch that if we started referring to function application with more elaborate syntax by parsing "sin(exp(x))" as application(sin, application(exp, x)) so that we could unify on sin, but this quickly obscures the syntax tree and removes the delightfully direct nature of DCGs.
We see problems popping up in the simplification as well. The problem of simplification is that you can wind up simplifying in circles which makes a depth first approach as used in Prolog very dangerous. The authors insert a cut to avoid this, but this also suddenly makes the entire system non-reversible.
The fundamental problem is that logic programming in the form of Prolog is practical precisely because of these limits. If you want more expressive power, you need to start talking about much more than unification and depth first search. At that point, you suddenly wind up with mechanisms like coordinate types which have the full expressivity of formal logic, but lose the simple execution of Prolog; simple type checking becomes undecidable.
> We can't do that, however, because Prolog doesn't support unification of functors. We could patch that if we started referring to function application with more elaborate syntax by parsing "sin(exp(x))" as application(sin, application(exp, x)) so that we could unify on sin, but this quickly obscures the syntax tree and removes the delightfully direct nature of DCGs.
Would the =../2 predicate help? It allows for you to unify functors without wrapping them in something like your application(exp, x) example. Not sure how it would interact with DCGs, though - never took more than a superficial glance at them.
> simple type checking becomes undecidable
Where can I read more about this?
It follows from Turing completeness. See https://en.wikipedia.org/wiki/Turing_completeness. It takes very little for a system to become Turing complete. And once it is, you can include arbitrary computations. Proving that they stop is impossible in general due to the well-known Halting problem.
https://beza1e1.tuxen.de/articles/accidentally_turing_comple... offers examples showing how easy it is to accidentally get Turing completeness, including multiple widely used type systems.
This book does it well. It can be a heavy slog:
https://mitpress.mit.edu/9780262536431/the-little-typer/
Here is a free book on how type checking can be used to do mathematical proofs:
https://lean-lang.org/functional_programming_in_lean/
Typescript's type system is technically undecidable because you can interpret Turing machines with it:
https://github.com/microsoft/TypeScript/issues/14833
The flip side is that such systems can still be practically useful. You just have to manage your type complexity, much like you already manage your runtime complexity.
This looks very fancy, but some linebreaks in the statements would have really helped readability.