Sean Nichols (mrputter) wrote,
Sean Nichols
mrputter

  • Location:
  • Mood:
  • Music:

Ha!

The Catamorphism has: Each Clause i has: Each Constructor j has:
∃{Q}i
∀{X}i
∃{B:=A1→…→An→Q[X/Ak]k}i
type params: ∃Z1…Zm
params: ∃{A1…An}i
context for the clauses: {f:B}i
a collection tree on the cut
context for the cut: {f:A1→…→An→Q}i
given type B
given params A1…An
given return type Q
given type params Z1…Zm
      eqn Ak:=T<Z1…Zm>
given return type Qi
      params ∃C1…Cr [X/Ck]k
      for each C, type eqns cloned from symbol table w/ params Z1…Zm
      a collection tree on Qi
      context for the tree: {p1:A1…pn:An} ∪ {x1:C1…xr:Cr}[X/Ck]k


Take that, you sonofabitch!


Mom, is it true that I was adopted?
"Mom, is it true that I was adopted?"
Tags: compilers, grad school, other cat, thesis, type theory
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment