[meeting] [joint] 01.02.24

[deemp]

Long-term goals

• In two months, EO team wishes the normalizer to be stabilized and included into their optimization pipeline.
• Nikolay is going to write a paper and submit it by mid-March.
• Get a patent

Notes

• Need to finalize extended rule set so that it can be further formalized.

• Normalizer rules are still being implemented, some features are lacking, but awaiting them soon.

• Normalizer team needs more test programs to run the test in a pipeline.

  • Yegor shared a link to a repo with lots of unit tests (Collect EO programs #69 (comment)).
    • One simple change is required to make them print resulting code.

• Collect performance metrics #78

• Collect optimization metrics #79

• README was updated to include instruction on running the normalizer, and on writing yaml files with custom rules (refactor: readme #73).

  • Normalizer team plans to set up a site (mkdocs) with the instructions (Set up a site #74).

• Normalizer will be pushed to hackage today (related to deployment to hackage.haskell.org is not configured #2).

• Formalization is almost complete

  • Need to finish proof of a single lemma (Fix and complete the substitution lemma proof#12).
  • Additionally, need to prove to lean that some functions terminate (Fix termination proofs proof#15).

• Yegor asked to make a presentation of what is going on in the proof repo once KS22 is complete (Prepare a presentation proof#18).

• Nikolay has been constructing EO programs to check how ϕ-calculus rules and EO compiler/optimizer(?) correspond to each other.

  • Currently, there are several issues/misunderstandings.
  • Nikolay is rewriting the rules into mathematical notation.
  • Nikolay will make a few examples on how the notation works.

• Update normalization rules and their description (https://github.com/yegor256/phi-paper/issues/13).