Lectures onType Theory
ch:fomega-self-representation: ch:fomega-self-representation
appendix sectiontutorials

ch:fomega-self-representation: ch:fomega-self-representation

Exercise 17.10.

Represent variables and the four deep cases by ordinary Kappa data. First write structural quote and unquote; test their round trip on a tree containing all four cases. Next write independent direct and fold size functions and compare them. Finally implement the term- and type-redex head tests and the quotation-image predicate. Run

kappa check artifacts/ch17-fomega-selfrepr/corpus.kp
kappa test  artifacts/ch17-fomega-selfrepr/corpus.kp
kappa run   artifacts/ch17-fomega-selfrepr/corpus.kp
kappa audit artifacts/ch17-fomega-selfrepr/corpus.kp

Require the six frozen PASS lines, the final count, and []. Replay each README mutation from a fresh accepted copy; a mutation succeeds as a negative control only when check passes and test fails. The finite data model checks fold equations, not full Fω kinding.

Search the book

Type to search the local edition.