Skip to content

Latest commit

 

History

History
169 lines (136 loc) · 5.84 KB

Notes.md

File metadata and controls

169 lines (136 loc) · 5.84 KB
Raw

Notes

We want to alert you that you've been granted the following access: Manage Users and Edit to the Google Analytics account plfa (UA-125055580) by [email protected].

Google analytics

Where to put Lists?

Three possible orders:

  • (a) As current
  • (b) Put Lists immediately after Induction.
    • requires moving composition & extensionality earlier
    • requires moving parameterised modules earlier for monoids
    • add material to relations: lexical ordering, subtype ordering, All, Any, All-++ iff
    • add material to isomorphism: All-++ isomorphism
    • retain material on decidability of All, Any in Decidable
  • (c) Put Lists after Decidable
    • requires moving Any-decidable from Decidable to Lists
  • (d) As (b) but put parameterised modules in a separate chapter

Tradeoffs:

  • (b) Distribution of exercises near where material is taught
  • (b) Additional reinforcement for simple proofs by induction
  • (a,c) Can drop material if there is lack of time
  • (a,c) Earlier emphasis on induction over evidence
  • (c) More consistent structuring principle

Set up lists of exercises to do

  • Use md rather than HTML
  • Tell students to do all exercises, and just mark some as stretch?
  • Make a list of exercises to do, with some marked as stretch?
  • Compare with previous set of exercises to discover some holes?
  • Add ==N as an exercise to Relations?

Other questions

  • Resolve any issues with modules to define properties of orderings?
  • Resolve any issues with equivalence and Setoids?

Old questions

Possible structures for the book

  • One possible development

    • raw terms
    • scoped terms (is conversion from raw to scoped a function?)
    • typed terms (via bidirectional typing)

  • The above could be developed either for

    • pure lambda terms with full normalisation
    • PCF with top-level reduction to value

  • If I follow raw-scoped-typed then:

    • might want to have reductions for completely raw terms later in the book rather than earlier
    • full normalisation requires substitution of open terms

  • Today's task (Tue 8 May)

    • consider lambda terms to values (not PCF)

    • raw, scoped, typed

    • Note that substitution for open terms is not hard, it is proving it correct that is difficult!

    • can put each development in a separate module to support reuse of names

  • Today's thoughts (Thu 10 May)

    • simplify TypedFresh
      • Does it become easier once I have suitable lemmas about free in place?
    • still need a chain of development
      • raw -> scoped -> typed
      • raw -> typed and typed -> raw needed for examples
      • look again at raw to scoped
      • look at scoped to typed
      • typed to raw requires fresh names
      • fresh name strategy: primed or numbers?
      • ops on strings: show, read, strip from end
    • trickier ideas
      • factor TypedFresh into Barendregt followed by substitution? This might actually lead to a much longer development
      • would be cool if Barendregt never required renaming in case of substitution by closed terms, but I think this is hard

  • Today's achievements and next steps (Thu 10 May)

    • defined break, make to extract a prefix and count primes at end of an id. But hard to do corresponding proofs. Need to figure out how to exploit abstraction to make terms readable.
    • Conversion of raw to scoped and scoped to raw is easy if I use impossible
    • Added conversion of TypedDB to PHOAS in extra/DeBruijn-agda-list-4.lagda
    • Next: try adding bidirectional typing to convert Raw or Scoped to TypedDB
    • Next: Can proofs in Typed be simplified by applying suitable lemmas about free?
    • updated Agda from: Agda version 2.6.0-4654bfb-dirty to: Agda version 2.6.0-2f2f4f5 Now TypedFresh.lagda computes 2+2 in milliseconds (as opposed to failing to compute it in one day).

PHOAS

The following comments were collected on the Agda mailing list.

Untyped lambda calculus

Agda resources

Syntax for lambda calculus

  • ƛ \Gl-
  • ∙ .