The 1-Aug-2008 release of mmj2 was the eleventh mmj2 release. A lot has happened since the first release, 29- Aug-2005! In fact, a lot of work took place leading up to the initial release.
Whew! So where to now?
mmj2 provides many features which make proving Metamath theorems easier, but even after all of the work, proving new theorems is still quite difficult, and the Metamath learning curve remains rigorous.
One hardship facing human provers is the requirement that the external "concrete" syntax match the internal "abstract" syntax of Metamath statements. This requirement is implicitly imposed by mmj2 but Metamath itself makes no provision for differences between external and internal syntax. For example, extra parentheses are not tolerated, and the customary abbreviations used in predicate and propositional logic are not supported.
Unfortunately, mmj2 is fully dependent upon using a single syntax throughout processing of an input Metamath database. The mmj2 unification algorithms perform unforgiving tree matches that would be mystified by extra, superfluous child nodes.
Overcoming this restriction cannot feasibly be accomplished within mmj2 – the code changes would be quite difficult. Fortunately, another way is possible using the new "mmj2 Service" feature which allows mmj2 to be called as a subroutine (or to call a user program).
With the mmj2 Service interfacing to mmj2's facilities a completely new code layer can be built from scratch which translates statements to the syntax required by mmj2 and the input Metamath database!
In addition, the new Theorem Loader facility is accessible to the mmj2 Service feature. Thus, an external program (code layer) can store theorems into the Metamath database in memory and write out Metamath ".mm" format theorems for easy loading later into Metamath.
The new Book Manager provides additional help for external code by providing a new set of slices through a Metamath database. Metamath "sections" and "sub-sections" are broken out into Book Manager "Chapters" and "Sections", with an additional slice of Book Manager Sections into Symbols, Variable Hypotheses, Syntax Axioms and Logical Assertions. Thus, external code can easily extract groups of related Metamath declarations.
Another benefit of layering new code onto mmj2 using the mmj2 Service feature is that multiple instances of mmj2 can be run simultaneously, either on a single processor or multiple processors. Each instance of mmj2 can run in a separate process and can be utilized by external code via the mmj2 Service to perform functions such as trial unifications and unification searches.
Thus, even though mmj2 itself is not written for multi- threaded use, users of mmj2 can "scale up". We can safely assume that memory and CPU capacity will continue to increase while costs decrease, so there is really no reason why a "power user" could not utilize dozens or hundreds of mmj2 instances! This means that new code layered on top of mmj2 can tackle computationally expensive tasks such as automated proving and high-powered "blackboard metaphor" proof assistanting.
Another major challenge facing human provers doing Metamath is the clerical and technical task of translating a set of equivalencies and associated "factoids" into a finished Metamath proof. We are all familiar with "blackboarding" a derivation by rewriting formulas with substitutions and simplification of terms. This task is non-trivial in Metamath because of its use of the "Hilbert style" instead of "natural deduction" (and the omission of many obvious theorems in set.mm to conserve space), but is far more amenable to automation than full-fledged automatic proving.
What we would like to have is a persistent user "workspace" with a graphical (aka "blackboard") interface on which derivations could be sketched out at a user-friendly level of detail. The code should then fill in the (Metamath) gaps and convert the statements back to the (internal) syntax required by mmj2 and Metamath.
Moreover, the workspace ought to provide the user extra features besides the basics. English descriptions and diagrams might be helpful, to say nothing of hyperlinks and interfaces to other programs (perhaps for import/export of formulas).
In theory the workspace could reside in a virtual world environment such as Second Life. And why not provide a voice interface?
There requirements cannot conceivably be added to mmj2. The only way to accomplish these feats would be to layer code on top of mmj2 via the mmj2 Service. mmj2 would thus provide an interface to Metamath and would perform essential proof checking functions for verification of the derivations created in the workspace environment.
I also believe that the amount of work implied by the ideas in this document could only be performed by a team of programmers. Using the mmj2 Service feature provides the solution to mmj2 coding bottleneck (me). Code can be layered onto the mmj2 base and minimal changes to mmj2 itself will be required.
thought you might want to see this:
http://www-03.ibm.com/press/us/en/pressrelease/23565.wss
ARMONK, NY - 21 Feb 2008: IBM (NYSE: IBM) today announced new technologies that recreate data centers in a secure virtual world – bringing real-time data from different facilities into a 3-D environment to visualize hot spots, data flow, server utilization and more to better monitor and manage the entire IT platform.
As companies of all sizes become more global in nature and tap into skills across the world, this mounting virtual workforce needs new tools to be effective. The 3-D Data Center allows experts to manage data center resources regardless of where they are or when these resources need attention, giving both employees and corporations enhanced productivity and freedom. The globally-integrated enterprise can deliver enormous economic benefits to both developed and developing nations, and new technology like this one can help companies seamlessly operate in such a distributed model.
Implenia, a Swiss construction, building services and real estate company, used the IBM virtual data center solutions to extend its existing virtual operations center which was previously used mainly for the facilities management processes. Adding the data from datacenter equipment allowed Implenia a finer control of the HVAC and security system. The virtual data center is a tailored 3-D replica of servers, racks, networking, power and cooling equipment that allows data center managers to experience real-time enhanced awareness of their dispersed resources.
3-D data centers are better able to consolidate the footprint of large numbers of machines only being used at, for instance, 10% capacity, to get rid of extraneous machines, and to monitor power and cooling, distribute workload between data centers, and even move processing to cooler sites when weather conditions are unfavorable.
"Viewing information about your data center in 2-D text – even in real time – only tells a data center manager part of the story, because our brains are wired for sight and sound," said IBM Researcher Michael Osias, who architected the 3-D data center service. "By actually seeing the operations of your data center in 3-D, even down to flames showing hotspots and visualizations of the utilization of servers allows for a clearer understanding of the enterprise resources, better informed decision-making and a higher level of interaction and collaboration."
A consolidated view gives operators insight into real physical issues such as how heat and energy flow through the data center. It also provides an intuitive method for understanding the company's entire computing architecture.
Currently, Implenia manages eight pilot sites including a data center that is managed by different tools and technologies. This challenged Implenia's management capability and affected its ability to control its customer properties and overall efficiency.
"Until working with IBM we only knew the state of our data center from the information we got through the building automation system and our virtual worlds communications interface. We didn't know the state of the server and information that was readily available to us until it was made more accessible via the 3-D visualizations that IBM built for us. We think that by combining this information with the information we had from the building automation side we can, from a building management standpoint, control the data much better and take action to be more efficient," said Oliver Goh, Implenia IT Specialist.
The key element in the work for Implenia is linking IBM's virtual world integration middleware, Holographic Enterprise Interface (HEI), that links real-world data center operations in cyberspace to their Building automation interface (VWCI). HEI has a modular and flexible design that allows clients to customize the desired interactions between real and virtual worlds. Each physical data center linked through this technology has an HEI instance that will transmit messages over the private network using Internet standard protocols to the 3-D virtual world server.
The virtual world platforms that render the 3-D environment is based on the OpenSim? Application Platform for 3D Virtual Worlds (http://opensimulator.org/wiki/Main_Page).
Most enterprises have data centers in different buildings, cities and possibly even countries. This is because data center designs have often been dictated by a company's need to scale quickly to meet demand from company growth and the transfer of more business processes to IT. But the job of efficiently managing data centers in Beijing and Buenos Aires from an office in Madrid is not always an easy one.
Companies are increasingly dealing with this problem by relying on software that allows them to manage their far-flung data centers as if they were a single, centralized computing pool.
Since the IBM 3-D data center is a multi-user virtual world, complete with in-world instant messaging, multiple users can have a shared 3-D experience about aspects of the data center, either in simulation or live mode, and carry on active discussions in-world. This shared experience allows technical, business, and even partner personnel, to collaborate on elements of the enterprise data center.
This type of collaboration provides much faster cycle times for analysis and decision making, by viewing operations in near real time, instead of exchanging messages and two-dimensional drawings via email.
With the IBM 3-D data center, customers can not only monitor and manage live systems, but they can perform simulations and 'what if' scenarios about their enterprise.
Since the 3-D assets are data driven, and there is no knowledge of the source of the data (only the structure of the message and its semantic meaning), the data center can be driven with mock up or pre-recorded data.
The modeling and simulation capability can also be used for exercises in space, power, and cooling planning, training, and disaster recovery scenarios. Users can move assets, interact with them, and drive them with real or simulated data.
The 3-D data center is customizable according to the client's servers, applications and monitoring systems. Models of non-IBM equipment are also available.
This is a true illustration of the future of work and how business will be conducted in the 21st century workplace. IBM is in the best position to help clients understand the challenges and opportunities that affect a globally-integrated enterprise. Global integration has become embedded in IBM's workforce, strategy, leadership and operations – affecting how the company collaborates across time zones and cultures and locates its operations, functions and leadership anywhere in the world based on the right skills and business environment.
About IBM For more information about IBM, please visit www.ibm.com.
About Implenia For more information about Implenia, please visit www.implenia.com
Here are some related links:
http://opensimulator.org/wiki/Main_Page
http://en.wikipedia.org/wiki/OpenSimulator
http://en.wikipedia.org/wiki/Libsecondlife
http://openmv.org/wiki/Main_Page
Well, no one has provided any input or gotten enthused about helping port Metamath/mmj2 into opensimulator (open source server for Second Life). So I will provide my first idea about this project:
Objects stored in the virtual world need more than 3 dimensions. Preferably n would be variable. The reason is that "real" mathematicians would find a mere three dimensions intolerable because what the virtual reality environment must be able to do is easily create objects from mathematical descriptions (sets of formulas), and mathematicians will need more than 3 dimensions in many situations. The virtual world would then, I suppose, render just the three dimensions which are rotated into the xyz plane.
Also…
I also think that the world itself should have more than 3 dimensions. For example, each user will likely wish to have the ability to create his/her own world within the world. (This idea needs fleshing out.)
I haven't looked into opensimulator.org to see if they support more than 3 dimensions. If they do not then it would be a heckuva job to clone the code and make the fixes. But it would be necessary, IMO, for a serious tool that would satisfy "real" mathematicians.
(Personally speaking, I haven't decided to formally begin this project. But I finally ordered high speed internet – upgrade from a modem … the last American to do so, haha – and I am pondering the acquisition of a new computer… I think it might be a server with at least 4GB of RAM running Linux.)
Henry Segerman's Second Life Images
Well…I had a dream last night and when I awoke I was worried about having enough money to live on. I think I may not be able to afford to continue doing new development in "open source" mode. I'll be able to afford to maintain mmj2 and support the users (if any bugs are ever reported :-), but the idea of spending another 1000 hours working and not earning any money feels unwise to me. I know that my abilities have value, the question is about how to find something which uses my abilities and pays me a few bucks for my rice, beans, rent and insurance.
Any suggestions, please speak up…
--ocat 7-Aug-2008