Leibniz – A Digital Scientific Notation
github.com
github.com
I've been noodling with some similar ideas around collaborative editing of interconnected declarative models, and I don't think the above is necessarily true. A diagram of the Linux Kernel might be even more complex than a diagram of some wild systems biology[0], but surely there is ever more complexity to discover. The tools for massively distributed digital collaboration seem much more polished in software than scientific fields today. I hope the author's work is a step in the right direction!
For similar Scheme-y computer algebra stuff, see Sussman and Wisdom's work in "Structure and Interpretation of Classic Mechanics" and follow-ons.
[0]: https://s-media-cache-ak0.pinimg.com/originals/35/98/92/3598...
Software isn't like that. Software has to describe a process unambiguously and exhaustively. There is no option to say "and now you do X" while leaving X undefined.
Software can't be simpler than the process it describes, it can only provide a simpler interface.
Redundancy can be achieved through multiple independent systems, e.g. repeating the encoded text in multiple locations; such an approach is not holographic, though. Parity is a more holographic encoding scheme in that redundancy comes from the interaction of multiple pieces of encoded text.
The term is even more applicable when talking about convolutional neural networks in which every neural node significantly contributes to every encoding. Here the similarity to optical holograms becomes quite apparent.
Also, evolution selects for robust code.
Maybe not at runtime, but you seem to be describing lambda functions.
For example, these systems solve indefinite integrals without having to apply numerical methods with an infinite number of steps: http://www.integral-calculator.com/ http://maxima.sourceforge.net/ https://www.wolfram.com/mathematica/
The only reason it could be more complicated is if we only include a small portion of the systems biology diagram. Since we do not understand every reaction pathway in any biological system it will necessarily be a partial picture on the biological side. On the software side we can produce a full diagram.
It will be a long time before we are able to produce a full systems biology diagram.
(If the documentation is written by a separate person, not coördinating with the original coder / equat-or, then one must doubt its accuracy; and, if it is auto-generated—well, have you ever seen really good auto-generated documentation?)
Different priorities lead to different design decisions. In a computer algebra system, you never see a definition of a term algebra or a list of rewrite rules. They are hidden from the user, and in the case of commercial software even heavily encoded to make them inaccessible. A computer algebra system is the equivalent of a single giant unpublished Leibniz context. In contrast, Leibniz encourages small, readable, and remixable contexts that can be examined and understood by scientists with reasonable effort. However, Leibniz lacks the huge database of simplification rules that make up the bulk of a computer algebra system.
You can use the database of equations (and rules) to "reduce" a term, which is also what computer algebra systems do. The difference is that in Leibniz, the database of equations of rules is always known and can be inspected, whereas in a computer algebra system it is carefully hidden from the user. Since it's this database where scientific knowledge is stored, this difference is quite important.
The difference is in the focus rather than in the principles. Leibniz is a Turing-complete language, so you can use it for programming. But that's not what Leibniz is designed for. Term reduction is more a way of exploring the definitions in a context than a way to run code.
[1]: http://maude.cs.illinois.edu/w/images/0/0d/Maude-book.pdf
I remember dabbling with Pure, which used term rewriting, and lent itself to expressing mathematical equations in a familiar format, but it was not a prover.
I downloaded the PDF for Maude, and I will certainly take a look in the meantime. My interests are solely for learning, and I thought using something like Idris to work my way through Sussman's Structure and Interpretation of Classical Mechanics, might drive it home for me in ways that my physics classes didn't.
My only question is: why? Seriously, what problem are you trying to solve here?
Your 27 page long essay was useless in conveying that to me because it was written overly explicit and seems to have too much background but not really any content.
Looking at the examples I just don't see a point. I'm a scientist. I work with PDEs. You even mentioned one of the software I work with in your paper.
Nothing you have written explains to me why I should decide to write e.g.:
nabla v = 0
In whatever notation it is you are trying to sell me.
So please explain.
The point of Leibniz is to communicate information to other scientists, but in a notation that can be analyzed and verified by computer programs. An immediate advantage is coherence checking by the Leibniz system - you cannot use undefined quantities in an equation, for example.