a language for talking about math precisely

[gusl]

I just spent >1 hour brainstorming/designing a heavily-typed language to help me formalize the math behind basic statistics and linear algebra. The fun of seeing mathematical objects with types like A -> B -> C is to consider mathematical concepts that arise out of currying it, reversing arrows, etc., and visualizing possible analogies between different concepts.

To paraphrase someone, the programs would be written to be read by humans, and only occasionally by computers. In particular, I'm designing it to be tolerant of incomplete formalizations/implementations (since formalizing "common-sense math" is so much work). This means it won't always be able catch contradictions... but I'm hoping it could learn to, by interacting with the user (turning "programming by demonstration" into "math acquisition by demonstration").

Currently I'm not distinguishing definitions from theorems. They're both "Constraint".

Comments

[en-ki.livejournal.com]

Have you seen vdash?

[gustavolacerda.livejournal.com]

That's a pretty cool idea. Thanks for the link. He and I have a lot of the same ideas (most of which were expressed in the QED Manifesto).

But since it's aiming for full formalizations, I wonder if it'll ever get off the ground. The Isabelle example shows syntax highlighting on the wiki article, which is pretty sweet. If wonder if they'd offer syntax highlighting in the 'edit' view.

In any case, I'm certainly aiming for less. I'll definitely talk to him at some point.

[stepleton.livejournal.com]

Good luck! If you can bridge the gap between formality and flexible idiom in this setting, you will have accomplished a formidable and worthy goal.

Since you're aiming for human readability, I imagine (or hope) you are giving careful consideration to the appearance of your language. Mathematical notation is so compact, and part of learning to be better at math (for me, anyway) is training my brain to construct a picture of what a formula does after I give it a quick visual scan. I guess your goal is not to replace traditional notation, but if you hold human processing as a goal, I proffer that you'll have to inject enough visual distinctiveness in your syntax to facilitate this kind of off-the-cuff analysis.* If your code is a bunch of monospaced lines (a la Matlab) then scanning will be more difficult. Moreover, while I disdain many mathematical formulas as programs with lousy variable names (x, γ, etc. vs. "distance", "time"), if you employ long keywords or type identifiers like 'PositiveDefiniteMatrix'**, you may complicate matters for scanners still further---just try to interpret any overly-CamelCased C++ out there at a glance.

(* If you're skeptical as to why you would need good first-glance analysis, I'd suggest that first impressions are important to putting the human viewer on the right track to thinking about the math quickly.)
(** Is this a type you would want? I don't know; not a PL guy here; maybe your type system could encode properties like these...)

I've often wondered what mathematical notation I could come up with if I decided to hole myself into a cave for a few years and start over from scratch. I don't like the current system very much... it has lots of arbitrary nooks and crannies (e.g. sin^y x versus sin^-1 x) and is, in my mind, excessively terse. I would love a place for comments, just like in code! Really! That said, I can't even begin to think of something new that would be any better. What we have now takes us a long way.

[en-ki.livejournal.com]

As far as notation goes, I'd just as soon have TeX <-> Lisp (I don't care which one is canonical, as long as the converter comes free with the package).

[gustavolacerda.livejournal.com]

Is my goal to replace traditional notation?

Well, I am a proponent of "dynamic syntax": one should be able to choose between traditional view (for scanners) and a more explicit view (for beginners)... or an integrated view, such as a tooltip telling you the type of the object whose identifier your mouse is on.

Of course, this is generally more work for content authors, at least until the system is intelligent enough to translate between the two automatically.

Ambiguity and terseness are also my main complaints with traditional notation.

PositiveDefiniteMatrix is definitely the kind of thing I have in mind.

I suspect that many difficulties will have to do with context-dependency.

Scanning is a concern I hadn't considered.

[demarko (from livejournal.com)]

woah, new picture!