Desugaring Galois connection

[rolyp]

Show how the fwd and bwd desugaring slicing rules form a Galois connection (for a given program). Tasks:

Done/dropped:

• sanity-check “ambient computation” in desugarBwd – needs further thought, but basically ok
• helper macros for things like totaliseGeq
• consolidate list-comp-gen proofs using new list-gen lemma
• roll out macros to proofs
• purge superfluous x-refs
• simplify list comprehension proofs to remove done and list-comp-last
• macroise desugaring overloads
• check list-comp-gen bwd – can this be made more symmetric with fwd rule?
• define functions desugarFwd_s, desugarBwd_s in terms of the corresponding relations, similar to eval
• theorem stating that the two functions form a Galois connection
• drop done sentinel in list comprehension syntax and allow [s | ε] instead
• ensure eq rather than geq used for (meta-) “pattern-matching”
• trace analogues as subscripts in backward desugaring relations
• new symbol for desugaring relations that have expression or continuation on the left
• define Galois connection notation f ⊣ g in terms of composites (f after g) and (g after f) – see def:core-language:gc
• define \Below{v} notation using ⊑
• prove “part 1” (fwd after bwd is increasing)
• prove “part 2” (bwd after fwd is increasing)
• identify any other theorems we need as go along, e.g. monotonicity
• state GC theorems for:
  • desugar for list rest
  • totalise
  • desugar for clauses
  • desugar for single clause (judgements p, κ \desugar σ and \vec{p}, e \desugar σ)

Other useful points of reference:

• “set of paths in a term” exposition in 3.2 of FPTETW
• methodology summarised in 2.3 of IFPTETW

[rolyp]

@min-nguyen Notes from Friday. Will add some tasks above. Suggest referring to our ICFP 2017 paper to look at how we set up the Galois connections there.

Lattices; in the finite case, can always understand in terms of a powerset:

Partial order (actually lattice) of slices of a fixed expression:

Functions eval_fwd and eval_bwd defined as forward and backwards slicing relations, domain-restricted to slices of a fixed expression:

[rolyp]

@min-nguyen I’ve defined some of the notation we discussed yesterday (see bullet list above). That should be enough to get you started.