[HN Gopher] Exotic Programming Ideas: Part 2 (Term Rewriting)
___________________________________________________________________
Exotic Programming Ideas: Part 2 (Term Rewriting)
Author : azhenley
Score : 96 points
Date : 2020-11-16 15:32 UTC (5 hours ago)
(HTM) web link (www.stephendiehl.com)
(TXT) w3m dump (www.stephendiehl.com)
| georgewsinger wrote:
| > It is true that this system can be used to program arbitrary
| logic, it can however become a bit clunky when trying to code
| imperative logic that works with inplace references and mutable
| data structures. Nevertheless it is a very powerful domain tool
| for working in scientific computing and the number of functions
| related to technical domains that are surfaced in the language
| represents decades of meticulous expert domain expertise.
|
| Can you explain this more? Why is (i.e.) the Wolfram Programming
| Language best thought of as a "domain" tool, and not a general
| purpose programming language? Why couldn't someone build an
| extraordinarily complex piece of software (say with millions of
| lines of code) under term-rewriting paradigm (like Wolfram) in a
| domain that has nothing to do with traditional
| mathematics/scientific computing?
|
| BTW, my favorite Wolfram fact is that it is the most concise
| programming language on the Rosetta:
| https://blog.revolutionanalytics.com/2012/11/which-programmi...
| 6gvONxR4sf7o wrote:
| You could. But as one of the Mathematica devout, it works be a
| massive pain in the as compared to other languages better
| suited for it. Assuming languages are equivalently expressive
| (in the Turing complete sense), the difference is in what they
| make easy.
|
| It's easier to make a small web API in python than assembly,
| even though they can do the same things. Mathematica is
| designed to make (symbolic) mathematics easiest. It excelled
| there at the expense of weirdness elsewhere.
|
| The answer unfortunately reduces to "I dunno, try it and see."
| chubot wrote:
| Yeah I'm finding myself explaining the difference between
| shell and Python a lot:
|
| https://news.ycombinator.com/item?id=24873284
|
| _Shell is good for creating Unix systems because of the
| tools it provides. ... It 's hard to explain, but if you work
| in that area, you'll very quickly see it._
|
| I think many people have learned one language, or 3 languages
| that are similar, and they think all languages do roughly the
| same thing.
|
| That's incorrect on all counts: in terms of the core data
| model, the operators, and the libraries.
|
| If you do a lot of work in a specific domain, you'll start to
| see all the differences. Shell is the best tool for bringing
| up machines, which happens a lot in both the cloud/web and
| embedded spaces.
|
| ----
|
| Ditto for R. R makes a lot of tasks really easy, and a lot of
| other ones really hard (like being 10x slower than Python, or
| 1000x slower than C, for many tasks). That sounds horrifying,
| but it really helps you get a lot of work done.
|
| Another thing people have trouble appreciating is the
| difference between R and Matlab, and Matlab and Mathematica.
| Those 3 languages are drastically different because of both
| their core data model and who uses them.
| kmill wrote:
| It's "fine" for imperative programming if you never make a
| mistake: the problem is that it is extremely permissive and
| won't stop execution on errors. I usually add my own error
| checking and default cases to cause programs to halt, and
| these help a lot, but there are still a number of footguns.
|
| One example is what happens if you map a function f over a
| list lst: f /@ list. Oh, the variable was called lst and not
| list? Mathematica will happily evaluate this and result in
| list, assuming list has not been defined. This is because
| what /@ does is apply f to each part of the expression, and a
| Symbol has no parts. If Mathematica had a way to declare
| which global symbols can be used in local expressions, it
| might help prevent this class of bugs.
| tgb wrote:
| What's the magic going on in substitutions like:
| Sin[a+b] /. Sin[x_] -> Cos[x]
|
| which yields 'Cos[a+b]'. Is the underscore after the x what
| indicates that "x_" can take any value? And Mathematica then
| strips the undescore and replaces 'x' with that value? Why not
| just use x_ on both sides? And earlier the author was using '_x'
| instead of 'x_'. It seems rather mysterious to me.
| 6gvONxR4sf7o wrote:
| It matches the expression with x_ as a named wildcard (it has
| lots of stuff you can do to constrain the matching, like "only
| match if x is prime"). Then it replaces the whole expression
| having x bound to whatever x_ matched.
| colehasson wrote:
| the underscore makes it a symbolic variable, not one with value
|
| unbound in the lambda sense
| tgb wrote:
| So _any_ underscore at all makes it a symbolic variable? (Or
| trailing /leading underscores only?) And the name of the
| variable on the right-hand side of the substitution is that
| name with the (or all?) underscore removed? It seems very
| clunky, so I think I'm missing something.
| Someone wrote:
| Mathematica doesn't allow underscores in names. I also
| think the use of __x_ is an error in this article
| (disclaimer: I haven't used mathematics in decades)
|
| = underscores must come at the end.
| tgb wrote:
| So is the right interpretation to think of "_" not as
| part of the variable name at all but rather as a unary
| operator (that acts on its left) which denotes a variable
| as unbound?
| kmill wrote:
| A pattern like _List matches lists, but the match isn't
| associated to a variable.
| 6gvONxR4sf7o wrote:
| At this point you seem too understand the mechanism well
| enough that the docs will help you with the details best.
| kmill wrote:
| The left-hand side of the arrow is a pattern expression [1]
| (though usually you'd use the :> arrow to delay evaluation of
| the right-hand side). The "full" notation is x_H for a pattern
| variable x that needs to have head H. Dropping the H, it
| matches anything. Dropping the x, it just doesn't set a
| variable when matching. Dropping both, it matches anything and
| doesn't set a variable.
|
| [1] https://reference.wolfram.com/language/guide/Patterns.html
| tgb wrote:
| Okay thanks, that all makes more sense now.
| hyperpallium2 wrote:
| I want to write a term rewriter for algebraic equations (just
| commute, assoc, distr, etc), but I wonder about the UI: the best
| way for a user to _specify_ which parts to transform?
|
| Here's the obvious ways I've thought of - have I missed some?
|
| - Derivations are usually written as before and after, and
| sometimes the name of the transform, and the reader must work out
| the arguments. Could have the program check the transform... but
| I'd like to save the user all that rewriting...
|
| - You could specify the arguments with a function at that point
| (using location to address them). Seems just as bad.
|
| - An awkward _path_ through the parse tree to specify each
| argument is also possible.
|
| - In a GUI, arguments could be selected by clicking.
|
| - The user could name the transform, and the program
| automatically find where it is applicable, and apply it - or give
| a list of applications, and the user selects which one. But this
| is a step towards an automatic theorem prover, and is more
| automation than I want the user to have.
|
| Are there other ways?
| jswrenn wrote:
| The `traces` procedure from Redex displays a navigable graph of
| _all_ applicable transformations and their result.
|
| https://docs.racket-lang.org/redex/The_Redex_Reference.html#...
| siraben wrote:
| In a similar vein, see[0] which talks about rewrite systems from
| a more formal viewpoint. On the practice side, GHC performs
| rewrite rules[1], an example of which is
| "map/map" forall f g xs. map f (map g xs) = map (f.g) xs
|
| Combining two calls to map into one. While this seems silly,
| terms like this can arise as a result of other compiler
| optimizations. GHC can even remove intermediate data
| structures[2] entirely, so writing factorial as
| factorial n = product [1..n]
|
| would result in an efficient first-order program without the list
| at all. Another example of where rewrite rules come in handy is
| linting[3]. It does seem that a lot of these rewrites are
| possible only in a pure language, otherwise the compiler would
| have to resort to analyzing side-effects.
|
| [0] www.cs.tau.ac.il/~nachum/papers/taste-fixed.pdf
|
| [1]
| https://downloads.haskell.org/~ghc/7.0.3/docs/html/users_gui...
|
| [2]
| https://users.cs.northwestern.edu/~robby/courses/395-495-201...
|
| [3] https://github.com/ndmitchell/hlint
| codekilla wrote:
| Maude is a really cool Language based on rewriting logic.
|
| http://maude.lcc.uma.es/maude31-manual-html/maude-manual.htm...
| sritchie wrote:
| If anyone wants to play with these ideas in Clojure(script), take
| a look at the SICMUtils project:
| https://github.com/littleredcomputer/sicmutils
|
| I picked up co-maintenance on this project a few months ago; it's
| a Clojure port of the computer algebra system behind Sussmans'
| "Structure and Interpretation of Classical Mechanics" [0] and
| "Functional Differential Geometry" [1], and can run all the code
| from those books. (I'm currently working on integrating it into
| https://Maria.cloud so all of this will be usable from the
| browser.)
|
| `sicmutils.generic.simplify` plugs in to a rule-based term
| rewriting system like Mathematica's, along with polynomial and
| rational function simplification.
|
| The core idea of the library is that if you build everything on
| top of extensible generic arithmetic operators (multimethods in
| Clojure), then a lot of good stuff shows up for free:
|
| - If I implement all the operations for symbols, I get a symbolic
| arithmetic system for free. - Extend the generics to Dual
| numbers[2]? Boom, forward-mode AD pops out!
|
| I'm getting carried away. Check it out, get your term-rewriting
| fix.
|
| [0] https://mitpress.mit.edu/books/structure-and-
| interpretation-... [1] https://mitpress.mit.edu/books/functional-
| differential-geome... [2]
| https://en.wikipedia.org/wiki/Dual_number
| agambrahma wrote:
| This is really cool.
|
| Remember coming across SICM a long time ago, feel it gets
| under-appreciated because it's perhaps too niche (not enough of
| the "SICP crowd" cares about the physics, people who care about
| the physics don't come across it).
|
| A Clojure version will ensure it lives on longer (the one
| downside of these old books is how closely they're tied to MIT-
| Scheme)
| muizelaar wrote:
| If you want to follow along you can use without using Mathematica
| you can use the Mathematica clone
| https://github.com/mathics/Mathics
| kmill wrote:
| Sometimes the way I explain Mathematica to people is that, where
| Perl is the Perl of string rewriting, Mathematica is the Perl of
| tree rewriting.
|
| Some comments about the article:
|
| Mathematica has two types of rules, Rule and RuleDelayed, given
| by a -> b and a :> b. You usually use RuleDelayed unless you want
| Mathematica to pre-evaluate b. For example, if you create a rule
| like x_ -> (Print[x]; 1 + x) it will immediately print the symbol
| x and then result in the rule x_ -> 1 + x, but x_ :> (Print[x]; x
| + 1) instead evaluates to itself without that side effect.
|
| It might be worth knowing that $Assumptions has a dynamic scope
| construct (like fluid-let in scheme), where Assuming[a > 0, ...]
| will temporarily append a > 0 to $Assumptions.
|
| The code for Diff is not correct, since it has patterns on the
| right-hand side of the rules (and also it's Power, not Pow). For
| idiomatic Mathematica, you would attach these rules to the Diff
| symbol itself as "DownValues" so that Mathematica will
| automatically apply them: Diff[f_ g_, x_] := f
| Diff[g, x] + g Diff[f, x]; Diff[f_ + g_, x_] := Diff[f, x]
| + Diff[g, x]; Diff[Power[x_, n_Integer], x_] := n*Power[x,
| n - 1]; Diff[n_?NumericQ, x_] := 0;
|
| These := operators append a rule to DownValues[Diff], where the
| rule is exactly from replacing := with :>.
| In[14]:= DownValues[Diff] Out[14]=
| {HoldPattern[Diff[f_ g_, x_]] :> f Diff[g, x] + g Diff[f, x],
| HoldPattern[Diff[f_ + g_, x_]] :> Diff[f, x] + Diff[g, x],
| HoldPattern[Diff[x_^n_Integer, x_]] :> n x^(n - 1),
| HoldPattern[Diff[n_?NumericQ, x_]] :> 0}
|
| The HoldPatterns in here are to prevent Mathematica from
| evaluating the patterns, since Diff has all these rules that
| really want to activate for those left-hand sides. (Yes,
| patterns, too, are subject to evaluation. It can be helpful in
| very limited circumstances, like metaprogramming the rules.)
|
| It looks like it's still missing some rules, though:
| In[42]:= Diff[x^2 + 2 x + 1, x] Out[42]= 2 x + 2
| Diff[x, x]
|
| One fix is to change the power rule to
| Diff[Power[x_, n_Integer: 1], x_] := n*Power[x, n - 1]
|
| which gives n the default value of 1, plugging into a system
| where Mathematica knows x^1 and x are the same.
|
| ---
|
| Something I use Mathematica for is calculations in things like
| the Temperley-Lieb algebra (for calculating the Jones polynomial
| of knots). The Temperley-Lieb algebra is pretty much a calculus
| of path composition, but you also take formal linear combinations
| of these, and closed loops evaluate to some polynomial. In the
| following, P[1, 2] would denote a path between points 1 and 2.
| SetAttributes[P, Orderless]; P /: P[a_, b_] P[b_, c_] :=
| P[a, c]; P /: P[a_, b_]^2 := P[a, a]; P /: P[a_, a_]
| := -A^2 - A^-2;
|
| For example, P[1, 2] P[2, 3] P[3, 1] evaluates to -A^2 - A^-2. (I
| have a library for these things where the "boxes" it renders to
| in the Mathematica notebook is a graphical representation of the
| paths. The graphical paths _are_ the expressions, which has been
| very helpful to me.)
| 7thaccount wrote:
| Sometimes I think people don't fully understand how cool the
| term rewriting is in Mathematica where it continuously expands
| on anything from text to functions to images and audio...it's
| pretty neat.
| jswrenn wrote:
| If you're interested in playing around with term rewriting, I
| highly recommend the Redex framework! https://docs.racket-
| lang.org/redex/index.html
|
| It's a really neat way to model programming languages and
| transition systems. Unfortunately, I think the documentation is
| perhaps more intimidating than the tool (its target audience is
| programming language theorists; not people who just like noodling
| around with programming language design).
|
| My favorite Redex hack is that you surface your Redex model as a
| hashlang (Racket's way of providing replacing/extending the
| language), and get a fully-featured algebraic stepper in
| DrRacket! See this repo and PR for details:
| https://github.com/justinpombrio/RacketSchool/pull/5
| boygobbo wrote:
| That's a really useful comment - thanks!
| sriram_malhar wrote:
| I like Maude a lot. I recommend Peter Olveczky's book
|
| Designing Reliable Distributed Systems: A Formal Methods Approach
| Based on Executable Modeling in Maude
| Syzygies wrote:
| Two term rewriting algorithms of central importance in their
| domains: Grobner bases for systems of polynomials in many
| variables, and the Schreier-Sims algorithm for computing with
| permutations.
___________________________________________________________________
(page generated 2020-11-16 21:02 UTC)