Technicalities: maude
As part of "more public blogging" resolution, I'm thinking I'll return to occasional technical notes. This will be the first in a series of "things I've been looking at in the past few years", during the general haitus I've taken from writing technically.
Since these may be long-ish entries and quite boring to the less-technically-fascinated audience, I'll cut them and tag them as 'tech'.
Maude, TRSs and Equational Logic
I've become quite fond of Maude in the past year or so, for projects and experiments I'll get to in future posts. This post is just about Maude. Maude is a language, computational logic, and high performance implementation thereof. The logic is called "rewriting logic", a logical-deduction interpretation of Term Rewriting Systems (TRSs).
TRSs are a field of study I read up on a long time ago with great interest and then took a long vacation from. I was attracted to the topic as it seemed (to my younger eyes) a uniquely approachable level of thinking and talking about formal systems (logical deduction, search, simulation, program execution), in a way that feels to me similar to how I found group theory a uniquely approachable level of thinking and talking about math: it wasn't so much "more right or wrong" than other levels of detail and abstraction, but it was a field that talked about the subtopics I found interesting, or troubling, when thinking about the system, the topics that gave me pause, that made me wonder what would happen to the system if they weren't true.
Group theory was the first time I found myself (say) hearing someone seriously discuss both the presence and absence of commutativity or associativity in various operators, and the implications thereof; previously in math people had always just sort of taken for granted that some operations were and some weren't, and this just-so position always annoyed me and distracted me when trying to learn math. Similarly, TRSs were the first time I saw someone seriously discussing the presence and absence of normal forms or confluence, and what that means. Again, this is something that's normally just glossed over or stated as just-so in the presentations I've seen of other logics and logical frameworks, and it annoys and distracts me away from being able to focus on the material at hand. It's an aspect I want to look into and understand.
So Maude is a general-purpose TRS engine, of sorts. It has a number of interesting properties. Unfortunately it's quite hard for me to summarize because I'm not really an expert logician or TRS hacker; any time I talk about Maude I seem to stick both feet in my mouth. I will try to summarize some parts that seemed interesting to me, though. Theory nerds in the audience, please bear with me, this is just how my muddled brain works:
Anyway, that's my general Maude sales pitch. I have probably put my feet in my mouth a number of times either describing things that are not true about it, or nearly true but nonsensically phrased, or are completely obvious and present in all of its competitors. Nonetheless, I'm impressed. So impressed I've bought the book and am working through examples (very slowly). I feel like this is an object worthy of study.
Against it, there are some fairly clear criticisms, the simplest being that it's "too general" to use for anything without several layers of machinery built on top, the moral equivalent of "here's a turing machine, it's very powerful" (or "here's an assembler, it's very powerful"). It's also somewhat under-documented, and what documentation there is is quite dense, and the examples to study are often impractical or uninteresting. Finally its integration with other systems leaves much to be desired: the only real mechanism it has for interacting with the outside world is an object representing the evolution of infinite byte streams, hooked up to a TCP socket. It's clearly not designed for embedding.
This entry was originally posted at http://graydon2.dreamwidth.org/1100.html. Please comment there using OpenID.
Since these may be long-ish entries and quite boring to the less-technically-fascinated audience, I'll cut them and tag them as 'tech'.
Maude, TRSs and Equational Logic
I've become quite fond of Maude in the past year or so, for projects and experiments I'll get to in future posts. This post is just about Maude. Maude is a language, computational logic, and high performance implementation thereof. The logic is called "rewriting logic", a logical-deduction interpretation of Term Rewriting Systems (TRSs).
TRSs are a field of study I read up on a long time ago with great interest and then took a long vacation from. I was attracted to the topic as it seemed (to my younger eyes) a uniquely approachable level of thinking and talking about formal systems (logical deduction, search, simulation, program execution), in a way that feels to me similar to how I found group theory a uniquely approachable level of thinking and talking about math: it wasn't so much "more right or wrong" than other levels of detail and abstraction, but it was a field that talked about the subtopics I found interesting, or troubling, when thinking about the system, the topics that gave me pause, that made me wonder what would happen to the system if they weren't true.
Group theory was the first time I found myself (say) hearing someone seriously discuss both the presence and absence of commutativity or associativity in various operators, and the implications thereof; previously in math people had always just sort of taken for granted that some operations were and some weren't, and this just-so position always annoyed me and distracted me when trying to learn math. Similarly, TRSs were the first time I saw someone seriously discussing the presence and absence of normal forms or confluence, and what that means. Again, this is something that's normally just glossed over or stated as just-so in the presentations I've seen of other logics and logical frameworks, and it annoys and distracts me away from being able to focus on the material at hand. It's an aspect I want to look into and understand.
So Maude is a general-purpose TRS engine, of sorts. It has a number of interesting properties. Unfortunately it's quite hard for me to summarize because I'm not really an expert logician or TRS hacker; any time I talk about Maude I seem to stick both feet in my mouth. I will try to summarize some parts that seemed interesting to me, though. Theory nerds in the audience, please bear with me, this is just how my muddled brain works:
- It can be used as a very general dependently-typed total-functional programming language. In this mode, it supports specification of equational theories in relatively "normal" ML-ish functional style where a LHS pattern simplifies to an RHS expression. There's a Church-Rosser checker to ensure such theories are confluent.
- It also uses each of these equations, along with some declared metadata about associativity, commutativity, reflexivity and such to construct high performance matching automata for the patterns themselves, such that the patterns you write your equations in are matched modulo equality: anything equal to a pattern, within the equational theory of the sort specified by the pattern, matches the pattern. This makes for a really powerful, natural extension to normal FP, and feels "new" to me (maybe it happens in other systems I'm just less familiar with).
- Still viewed as a dependently-typed TFPL: its parametrization is very powerful. The types ("sorts") can be parametrized by signatures of whole equational theories. This also feels "new" to me, in expressiveness: like the ML module system with much stronger constraints. Though again, I may simply not be sufficiently practiced in expressing constraints in the types and theories of other systems.
- Beyond the equational part, it supports rules that are non-confluent/terminating, which it treats as general local state transitions in a concurrent system, and to which it applies arbitrary (meta) rewrite strategies; the default is an approximately "fair" one but you can provide your own. These let you model system-evolution state-spaces, and search for paths to prove or disprove the feasibility of terms, without necessarily constraining the order of that evolution. In this sense its behavior becomes more like a model checker, in which all possible evolutions of a concurrent system are explored.
- Again, when exploring the non-confluent rewrite rules, the engine matches terms modulo equality as implemented by each equational theory's matching automata. So if two terms A and B are equal in your theory, and you wrote a local state transition pattern based on A, it will fire on instances of B by applying the reduction to A first. This alternation between fast, deterministic, confluent equational theories used for term matching, and non-confluent rules used for state-space-expansion, seems like a very pleasant way or organizing reasoning and execution in a model. Again, I have no idea the extent to which this is what's happening under the hood in other systems, but the way Maude separates out, discusses and independently models the topics feels approachable to me in a way few other systems have.
- It's been tastefully built around a very general/minimal grammar and a very general mixfix parsing algorithm. The result is that, so long as you're able to live with a handful of minor constraints on your term language (balancing parens etc.), a large number of term-language grammars you might want to model can be written directly in their natural syntax, and the equational rules can be specified in that syntax too. I think I saw some quantity of this in ELF and HOL, but I never really got the hang of it. In Maude it feels sufficiently clear that I've been able to make it work.
- Finally: it's a very reflection-oriented system. Many important parts appear to be written in Maude itself, and can be extended or modified with user code. Moreover the reflection appears to be quite efficient: there's some sort of staged metaprogramming technique at work I can't quite figure out yet, in which programs written on reflections are lowered into high performance versions operating at the term level.
Anyway, that's my general Maude sales pitch. I have probably put my feet in my mouth a number of times either describing things that are not true about it, or nearly true but nonsensically phrased, or are completely obvious and present in all of its competitors. Nonetheless, I'm impressed. So impressed I've bought the book and am working through examples (very slowly). I feel like this is an object worthy of study.
Against it, there are some fairly clear criticisms, the simplest being that it's "too general" to use for anything without several layers of machinery built on top, the moral equivalent of "here's a turing machine, it's very powerful" (or "here's an assembler, it's very powerful"). It's also somewhat under-documented, and what documentation there is is quite dense, and the examples to study are often impractical or uninteresting. Finally its integration with other systems leaves much to be desired: the only real mechanism it has for interacting with the outside world is an object representing the evolution of infinite byte streams, hooked up to a TCP socket. It's clearly not designed for embedding.
This entry was originally posted at http://graydon2.dreamwidth.org/1100.html. Please comment there using OpenID.