Skip to content

Latest commit

 

History

History
310 lines (232 loc) · 14.8 KB

notes.org

File metadata and controls

310 lines (232 loc) · 14.8 KB
Raw

Goals

Long Term Goal

  • Write finite element code where the energy/action can be written down like on paper and the final cede can be differentiated with respect to almost anything like domain, stiffness parameters, initial conditions etc.
  • Support compilation to GPU and CPU.

Mid term Goal

  • Semi-automatic differentiation and optimization tools.
  • Inline C++ compiler to write efficient low level code.
  • Formalize and wrap OpenVDB, NanoVDB, Houdini, Eigen primitives.
  • Node based editor in Houdini.

Short Term Goal

My first goal is to write couple of simple ODE solvers maybe some simple finite difference solvers. The main things to focus on:

  • compare performance to hand written C++ code
  • attempt at semi-automatic differentiation of energy/lagrangian

Lean Framework

Implement these to in the order to get these examples working:

  1. Harmonic Oscillator
  2. Pendulum
  3. NBody
  4. NPendulum in 2D
  5. NPendulum in 3D
  6. 1D wave equation
  7. 2D wave equation

Reorganization

Mathlib

Everything that will hopefully be in mathlib one day

Categories

This contains all categories and basic proof automation in those categories.

  • proofs for algebraic operations
  • proofs for combinators
  • Hom and morphisms
Cat - common interface for all categories
Lin
Smooth
Diff
Cont
Set
Inv
Others - no immediate plan to do these
  • LInv - is it a category?
  • RInv - is it a category?
    • Difeo - This needs diffeology to have internalized Hom
Operators

This contains basic operators proofs about them and simplification identities

adjoint
sum
differential operators

differential, gradient, tangent_map, back_prop

limit
invert – basic properties and possible approximations
integral – basic properties and possible approximations
ode_solve – basic properties and possible approximations

Categories [/]

  • [ ] Implement `IsSmooth` - just duplicate IsDiff and add axiom that differential of smooth is smooth
  • [ ] Implement `IsLInv` `IsRInv`
  • [ ] experiment with `extends` keyword to chain categories properly and test if `IsInv` can be written just as an extension of `IsLInv` and `IsRInv`
  • [ ] Define Hom for categories and pick arrows
    • Lin: ⊸ –o -o
    • Smooth: ⟿ ~~> \r~3
    • Dif: ⇝ -~> \r~2
    • Cont: ↦ –> \r6
    • Diffeo: ↭ <~> \lr5
    • RInv: ↠ ->> \r23
    • LInv: ↪ >-> \r8
    • Inv: ↔ <-> \lr
  • [ ] internalized combinators
  • [ ] extract smooth/linear/… symbol - this will create appropriate morphism
  • [ ] modify remove lambda let to work with morphisms
  • [ ] Specialized notation λₛ for morphisms, maybe also ascii version as fun (x : X) ~~> (f x) or fun (v : V) --o (A v)
  • [ ] Implement IsCont
  • [ ] Add IsDiffeo a category of diffeomorphisms

Computations [2/11]

  • [ ] add simple algebraic simplification, probably based on this zulip chat
    • Attempt 1: What the link suggest does not work naively in my case :(
  • [X] add autodiff, autograd tactics
  • [X] make rmlamlet work in conv mode
  • [ ] rewrite autodiff and autograd to use conv mode
  • [ ] add autodual tactic
  • [ ] fix `remove lambda let` to work properly with `let` such that for loops are correctly abstracted
  • [ ] Add basic real functions like sin, cos, exp and their derivatives and inverses
  • [ ] Vector T n fixed sized array of type T
  • [ ] Tensor #[n1, n2, n3] fast float array to hold data - probably column major
  • [ ] Vec2, Vec3, Vec4 simple fixed size vectors
  • [ ] Mat2, Mat3, Mat4 simple fixed size matrices

Solver class [3/9]

  • [X] add tactics solver_check and solver_assumtion
  • [X] add tactic lift_limit
  • [X] rewrite Impl based on Mario’s answer
  • [ ] add tactic assume_this
  • [ ] add tactic check_this
  • [ ] refine lift_limit It should automatically call assume_this for assuming lifting of the limit

Based on how lift_limit currently works it should call one iteration of beta-reduction.

  • [ ] add tactic finish_impl probably just `apply Solver.pure`
  • [ ] check computability in finish_impl The approach is probably to replace every free variables in the target expression by their instance of `Inhabited`. For this use Expr.replaceFVar

    If the target is a function, synthesize all arguments with `Inhabited` and apply them.

Finally I need to figure out how to test if an expression can be evaluated.

  • [ ] implement assemble

Variational calculus [/]

  • [ ] Figure out how to deal with adjoint and dual in case of integrals
  • [ ] Automatize duality on integrals

External Linear algebra [/]

On using external C code: zulip thread

Example on how to use lean_external_object

Sims [/]

Harmonic Oscillator [2/6]

  • [X] Lean implementation
  • [ ] C++ implementation
  • [ ] measure performance and create nice comparison
  • [X] Hamiltonian formulation
  • [ ] Lagrangian formulation
  • [ ] Action formulation

Pendulum [0/6]

  • [ ] Lean implementation
  • [ ] C++ implementation
  • [ ] measure performance and create nice comparison
  • [ ] Hamiltonian formulation
  • [ ] Lagrangian formulation
  • [ ] Action formulation

N-Body Simulation [0/6]

  • [ ] Lean implementation
  • [ ] C++ implementation
  • [ ] measure performance and create nice comparison
  • [ ] Hamiltonian formulation
  • [ ] Lagrangian formulation
  • [ ] Action formulation

N-Pendulum [/]

  • [ ] Lean implementation
  • [ ] C++ implementation
  • [ ] measure performance and create nice comparison
  • [ ] Hamiltonian formulation
  • [ ] Lagrangian formulation
  • [ ] Action formulation

1D Wave Equation on Circle [0/6]

  • [ ] Lean implementation
  • [ ] C++ implementation
  • [ ] measure performance and create nice comparison
  • [ ] Hamiltonian formulation
  • [ ] Lagrangian formulation
  • [ ] Action formulation

2D Wave Equation on Torus [/]

  • [ ] Lean implementation
  • [ ] C++ implementation
  • [ ] measure performance and create nice comparison
  • [ ] Hamiltonian formulation
  • [ ] Lagrangian formulation
  • [ ] Action formulation

Notes on Lean

  • When cursor is places at the end of `repeat rw[thrm]` the goal shows only one rewrite as repeat didn’t work. This is confusing.

Links

Articles

Main

Other

Math Foundation

Lean

Video

Categorical Formalism

Blog posts

Presentations

others

  • David Sankel A guy writing Reflection TS proposal, but why is he interesting is that he developed some visual functional programming language similar to Houdini as he mentioned in CppCast.

Software

Vaguely related software

  • Enso - hybrid visual & textual programming language

Some relevant Zulip discussions: