[meeting] [internal] 13.06.2024

[deemp]

Danila's notes

Rejected ITP Paper

• choose a conference (!)
• decide what to change and send
• learn what are the rules in extended PHI
• prove confluence for extended rules
• create TODOs for the paper

POPL paper

• Can't send a paper
• Nickolay can't work on formalization

Paper about the normalizer

• Current implementation of the engine is inefficient
• Can apply user-defined rules

Normalizer

• Want to make the engine efficient
• Speed comparable with Fast Yegor rules
• Describe the engine in the paper and send

Good example

• Still need to try normalizer on the multiplication table
• We can't do stdout because we can't normalize
• Apply to show that we can't normalize
• If we remove --minimize-stuck-terms, we get something bad
• Need to ask Yegor

Efficient engine

• Delayed substitutions or closures
• This is another internal implementation different to PHI
• Can translate substitutions to usual PHI terms
• Yegor suggested: rho terms are bound to PHI.new_objects - allocate new objects in the global object and reference them
• Nickolay wants to use an efficient representation
• Not necessary for closures
• Existing unification - first order (metavariables in rules)
• It's possible to generalize and implement efficiently
• There's efficient representation implemented with students
• Very big plan, but many steps
• Nickolay can't predict (~1 month)
• Nickolay didn't try yet
• Try to implement closures
• If implement closures, can implement putting objects into the global object
• The final term will be smaller

Open PRs

• Close Roukaya PRs

Try the multiplication table example

Check normalization rules: without —minimize-stuck-terms and with disabled atoms

• Will fail because of explicit rho. EO doesn't support them

Paper and patent

• Custom rules - Nickolay doesn't see development vectors
• Focus on efficient engine

Formalization

• Progress is slow because formalization is hard
• Nickolay won't have time next month

Anatoliy's notes

Previous paper:

• Find a new conference instead of ITP.
• Update our paper, apply suggested fixes from the reviewers.

Plans for another paper:

• Take current normalizer system, factor out core rule executor, improve its performance to be on par with hardcoded rules.
• Effective syntax representation and effective substitution.
  • Suspended substitutions with closures. These are separate from syntax and phi, should be more effective, and then can be converted to phi.
  • in particular, it might take on the role of suggested global variables for numerous rho's.
  • It is desired to try an effective representation made by Bachelors.
• First try closures, then effective representation.

Other

• Need an example to show Yegor that for some atoms nothing will be optimize if we do not know information in advance. -
• Close PRs by Yegor's student (https://github.com/objectionary/normalizer/pull/375, https://github.com/objectionary/normalizer/pull/369, https://github.com/objectionary/normalizer/pull/356).