Lectures onType Theory
ch:cdle-cedille: finite zero-cost observations
appendix sectiontutorials

ch:cdle-cedille: finite zero-cost observations

Exercise 96.6.

Problem and invariant.

Observe Church counts, identity roll/unroll, and list-map reuse. Admit a function pair only when its finite erasure tags agree.

Two representations. An annotated untyped lambda evaluator could compare normalized programs. The selected identity/copying tags make the cost boundary explicit and keep execution total.

First complete version. Define function tags and intersections, then Church observations and identity roll/unroll. Add structural list map and equality before the identity and copying fixtures.

Observable result. The run ends All 5 Chapter 96 corpus cases passed.

A failing version. Admit every intersection. The copying pair is then accepted, its oracle changes to FAIL, and the test exits 1.

Acceptance and boundary. Run all four commands, restore the source, and require exact stdout and []. The model records five finite runtime facts; it does not check CDLE typing or prove zero-cost reuse in general.

Search the book

Type to search the local edition.