Running To Do List

automated-thm-todo.md

Theorem Prover Coding/Writing

• Fix typos in my notes on DPLL
  • Fixing the getLiterals code snippet to match the code
• Rewrite notes on DP algorithm after examining Knuth's drafts more thoroughly
  • Clearly explain the DP & DPLL algorithms in pseudocode
  • Clearly explain the backjumping optimization
    • Is it possible to do a more thorough algorithmic analysis of it? (I.e., do a better job!)
• Explore possibility that monads can be used for backjumping?
• Resolution space for random 3-SAT proves "with high probability" that "the total resolution space is quadratic".

First-Order Logic Related Stuff

• Write the prolegomena on first-order logic
  • Skolemization related notes
    • Torsten Hahmann, Skolemization, Most General Unifiers, First-Order Resolution
    • Christoph Weidenbach, 3.5 Normal Forms and Skolemization (Traditional)
  • Claus-Peter Wirth, Herbrand's Fundamental Theorem - an encyclopedia article
• Examine this Teach Yourself Logic guide

History of Theorem Provers

• Perhaps examining the history of Automated theorem provers would be interesting?
• See, e.g., The Early History of Automated Deduction

1950s

• The Logic Machine
  • Newell and Simon's "Logic Theory Machine" 1956
  • Programming the Logic Machine 1957
  • Empirical Explorations with the Logic Theorist Machine
  • Stefferud's "The Logic Theory Machine"

The 1960s

• Automath (1967)

The 1970s

• Prolog (1970)
• LCF (1972)
• Mizar (1973)

lambda-cube.md

Overview

My running list on stuff relating to the Lambda Cube.

Untyped Lambda Calculus

• Motivation
  • The Stanford Encyclopedia of Philosophy has a surprisingly good entry
  • Focus on lambda calculus as a "theory of equations", which explains why substitution is the only semantic mechanism
• Reduction Relations
  • Normalization, i.e., will the reduction process terminate after finitely many steps?

Simply Typed Lambda Calculus

Motivate Types

• Avoids ambiguities caused by self-application of Omega combinator, for example

ST Lambda Calculus + Type Constructors

ST Lambda Calculus + Polymorphism

ST Lambda Calculus + Dependent Types

References

• Barendregt's Lambda Calculus book is the bible for Untyped Lambda calculus
• Barendregt, "Introduction to generalized type systems" first introduced the Lambda Cube
• Pierce, Types and Programming Languages are a gentle introduction to a subset of the lambda cube.

todo.md

Overview

This is my running to do list...

• If we consider a Lorentzian manifold M which is the base for a spinor bundle, then it is clearly orientable. But is it globally hyperbolic?

Writing

Typesetting Notes

• Type up my notes on quantum gravity

Formal Proofs

• Investigate how tenable using Leslie Lamport's macros for structured proofs would be...
  • Could we implement something like Wiedijk's Mathematical Vernacular using Lamport's macros?
  • Lamport's macros are too peculiar to be used, need to write my own (or hack his) to have each \step be like an \item in that I just write \step <blah> as opposed to \step{number}{blah}.
• Can we formalize definitions too?
  • Examine J Urban's "Translating Mizar for first-order theorem provers" for a relevant discussion of this topic.

Physics

• Conjecture: Adler's paper violates the Froissart bound.
• Is there anything to Non-relativistic Twistor Theory and Newton-Cartan theory?
  • Newton-Cartan theory is enjoying a "renaissance" due to its use in Condensed matter physics

Thermodynamics & Statistical Mechanics

• Examine the thermodynamic limit further.

Side Projects

Toy programs I should write some time...

Computer Algebra System

It'd be nice to write a toy lisp that's also a CAS (or more precisely: a CAS whose syntax uses S-expressions, and may qualify as a lisp). Something like MAL may help bootstrap the initial stuff...

Ideally it should use the same tricks Euler used, i.e., follow the "generality of algebra" (for better or worse). Some stuff on this...

• Is there an algebra for divergent series summation operators?
  • Yuri I. Lyubich, "Axiomatic theory of divergent series and cohomological equations". arXiv:0705.1578
• C.f., MPL in Scheme --- dharmatech has a few other interesting and relevant repositories

Toy Lisp

I've been following the make a lisp guide to try to understand how Clojure works "under the hood" (there will probably be a blog post chronicling my adventures). This will be done in C++ to understand how the JVM does stuff, too (so, e.g., I'd implement some counterpart to AtomicInteger to get gensym working properly).

Bibliography Helper

• Write a program that will:
  • Take in some text files consisting of links to arXiv articles
  • Produce a markdown file consisting of formatted bibliography entries to the links
• Make the program able to update a markdown file, i.e., check if a given link is already entered in the bibliography...to avoid needlessly hitting arXiv too much.
• Have the input file also include header sections separated by #, ##, ###, etc., for various sections, subsections, subsubsections, respectively.