Tracking issue for research-todo

[bvssvni]

• 2-bit mini language for reference grammar
  • {} for repeat block, x for product type, , for sum type
  • Uses between-the-lines self reference addressing
  • Generate optimal binary parsers
• Infibin: Figure out fast algorithm for ancestor/descendant detection
• Infibin: Figure out fast algorithm for optimal navigation between two numbers
• Infibin: Produce non-trivial example of self-symmetric path
• Naive Zen Logic: Generalize to a version with some room for uncertainty
• Naive Zen Logic: Produce a reproducible experiment where reasoning about a smarter version is possible, e.g. some well defined limitation
  • Could be a limitation of combinatorial explosion that could be fixed by finding a more efficient algorithm
• Experiment with common sense reasoning about physics
  • Investigate the possibility that Higher Order Operator Overloading makes it easier to interpret equations of physical systems
• Figure out algorithm for deriving normal paths of Boolean functions constructed by if
  • Might have already solved this, check out papers
• Develop graphical notation for continuity and discrete transformations
  • Arrows are discrete transformations with direction
  • Lines are continuous transformations with length
  • Product surface rules
• Figure out whether declaration of function bodies can be modeled with linear logic
  • Each term in the function declaration being a resource, mapped to a sub-type path
• Formalize some ideas about collections of symbols associated with symbols
  • A choice e.g. c(s : bool) where c constructs the collection and s is a value
• Write up list of symbols used in basic path semantics
• Formalize unthinkable symmetric paths f[g] <=> h where |∃h| > 2^n for some finite n
• Write up about binary relations vs boolean functions among arguments of binary relations
• Figure out how to write a complain-when-wrong type checker for path semantics, accurate up to output permutation group as described in the paper about "constrained functions"
• Figure out what happens in a type theory if f : A -> B means ∃f{A} = B
  • Usually f : A -> B means ∀ x : A { f(x) : B }
  • |A| = |B| means the function maps uniquely and is therefore an equivalence