Skip to content

Latest commit

 

History

History
163 lines (128 loc) · 4.94 KB

rabbit-holes.md

File metadata and controls

163 lines (128 loc) · 4.94 KB

type theory

  • [martin-löf] Constructive Mathematics and Computer Programming
    • can we use <: and : for all judgements?
  • [martin-löf] Intuitionistic Type Theory
  • [henk-barendregt] Lambda Calculus With Types
    • recursive type
    • intersection type
  • [de-bruijn] automath

topos theory

  • we are interested in topos theory because we want to know is topos theory the algebraic semantics behind the use of partial function?

  • use partial function to specify algebraic structure

    • essentially algebraic theories
    • C-system
    • "Aspects of topoi", by Peter Freyd, 1972.
    • what is the main idea of topos theory? capture membership relation?
    • what is the relation between topos and partial function?
    • this might be very useful to
      • use algebraic structure in language without dependent type
      • capture composition of pi type in the dependent type theory

proof theory

  • [schroeder-heister]
    • standard formulation of elimination rule for implication v.s. another elimination rules to follow the same pattern, that is, the pattern exhibited by the rules of falsehood, disjunction, and existence elimination, has been considered by Schroeder-Heister.
  • [dag-prawitz] proof theory and natural deduction

actor model

  • armstrong_thesis_2003.pdf
  • 神經元 as actor
    • 神經網絡 閥值 no timeout the state of an actor encode informations the whole network encode informations

prover

  • martin lof
    • formalize girard-s-paradox
  • coq
  • discovering-modern-set-theory
  • find some theory to proof
    • number theory heyting arithmetic
    • plane geometry
    • must be able to use type class
  • predicate logic as prover
    • ACL2
    • the little prover -- little ACL
  • heyting algebra

physics

  • 经典力学
    • 爲了理解無窮小分析在物理學中的應用
    • 兩組視頻 walter lewin leonard susskind
    • 兩本書 micheal spivak -- physics-for-mathematicians--1--mechanics structure-and-interpretation-of-classical-mechanics

bishop

  • 如何明確地敘述 bishop 的計劃?
  • 對算法複雜度的形式化描述與機械化推導 就是向 bishop 的計劃 更買進了一步

fiber-space

  • 完成對 fiber-space 的理解 並寫好 at1 的綱領
  • 意譯 euler 以學教學法 與代數基礎
  • 讀古典 以批判分析的算數化

math reading list

  • classical
    • newton
    • euler
  • at
    • thurston/three-dimensional-geometry-and-topology--volume-1.djvu
    • dehn/papers-on-group-theory-and-topology--max-dehn.djvu
    • sze-tsen-hu/homotopy-theory.djvu
    • sze-tsen-hu/elements-of-general-topology.djvu
    • cell-complex/the-topology-of-cw-complexes--albert-lundell.djvu
    • hatcher/AT.pdf
    • norman-steenrod/how-to-write-mathematics--norman-steenrod.djvu
    • norman-steenrod/the-topology-of-fibre-bundles.djvu
    • algebraic-topology/simplicial-homotopy-theory.pdf
  • ag
    • algebraic-geometry-a-problem-solving-approach.pdf
  • dc
    • a-comprehensive-introduction-to-differential-geometry
  • cs
    • feynman/lectures-on-computation.pdf

AI

利用 sexp 向机器描述想要解决的问题， 机器给你解决问题的建议。

  • 问题可以是关于解决数学问题的，也可以是关于 OOP 的。

  • 类似专家系统。

  • 需要能够把某个领域的知识，表达给机器。

  • 如果我能帮助别人实现别人所感兴趣的所谓「专家系统」， 那么这个服务是否可以赚钱呢？

  • [project] 基于 how to slove it 的 bot。

  • [project] 基于 99 bottles of OOP 和 POODR 的 bot。

  • [project] 给出很多句子，学习出来语法。

Courses

highlights-of-calculus/ mit-18-065-matrix-methods-in-data-analysis--signal-processing--and-machine-learning--spring-2018/ mit-18-06sc-linear-algebra--fall-2011/ mit-18-085-computational-science-and-engineering-i--fall-2008/ mit-18-086-mathematical-methods-for-engineers-ii-spring-06/

Basic

Computer graphics

Database

  • cmu database course

AI