Components

Components of ProvingGround

The code is divided into projects and packages. The division into projects is partly based on what can run in the browser (via scala-js) and what needs to run locally (on a jvm). In terms of functions, our code consists of the following components.

• Foundations : this is essentially an implementation of Homotopy Type Theory.
• Learning : based on an abstract framework for generative models and associated costs, flows etc., evolution of finite distributions and generation of equations from generative models, and special rules encapsulating various heuristics (such as backward reasoning).
• Translation : a general recursive translation framework is implemented, with some special rules for using the output of parsers, as well as a target language. This is meant to be a major component but is only slightly developed so far.

Projects

The following are the active projects:

• core : most of the code is in this project; it consists of all the stuff that is important and can run both locally and in a browser (essentially no java dependency or filesystem access).
• leanlib : this is code that is generated from the lean library into our format.
• mantle : this mainly consists of the interfaces, including a web server that allows access to some features. There is also some stuff that uses java dependencies.
• nlp : the natural language processing components. Note that some core parts of this (such as the target language) are in the core.
• client : this is the scala-js interface to run in the browser.

Packages

The more meaningful division is into packages, which span across projects. We describe these below.

• provingground : this has
  • the implementation of our foundations - Homotopy Type Theory - except inductive types and induction/recursion (which are complex enough to get their own package) and representations using scala objects (which are formally not part of HoTT).
  • probability distributions including finite ones.
  • a few utilities.
• provingground.induction : inductive types, induction and recursion.
• provingground.scalahott : representations of objects in Homotopy Type Theory by scala objects.
• provingground.learning : the other large component besides foundations, with learning using generative models.
• provingground.translation : an abstract translation framework, natural language processing and other translation tasks such as formatted printing and translation to and from storage formats.
• provingground.library : mathematics in our format, including created by code generation from Lean Theorem Prover.
• provingground.interface : interfaces.
• other packages - these are not active.