objectionary / normalizer

Command Line Normalizer of 𝜑-calculus Expressions
https://www.objectionary.com/normalizer/
MIT License
7 stars 2 forks source link

Update the `COPY` rule as in phi-paper #445

Closed eyihluyc closed 1 month ago

eyihluyc commented 1 month ago

The current version of R_COPY does not account for the case when the inserted term is a formation that makes use of it's ρ attribute. As a result, when moving such formation inside the copied one, ξ.ρ changes, though it shouldn't.

Running recursive dataization on this term

{
  ⟦
    a ↦ ⟦ b ↦ ∅, x ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ (b ↦ ⟦ c ↦ ξ.ρ.x ⟧ ).b.c,
    x ↦ ⟦ Δ ⤍ 02- ⟧,
    λ ⤍ Package
  ⟧
}

results in

⟦ a ↦ ⟦ Δ ⤍ 01- ⟧,
  x ↦ ⟦ Δ ⤍ 02- ⟧,
  λ ⤍ Package
⟧

while the expected result is

⟦ a ↦ ⟦ Δ ⤍ 02- ⟧,
  x ↦ ⟦ Δ ⤍ 02- ⟧,
  λ ⤍ Package
⟧

PR-Codex overview

This PR focuses on updating object structures and patterns in the eo-phi-normalizer module.

Detailed summary

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

eyihluyc commented 1 month ago

I just realized there's a problem with the suggested rule, as it applies only to formation with application. If there's a "tail", for example .b.c in

a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ⟦ c ↦ ξ.ρ.x ⟧ ).b.c

it's not applicable.

eyihluyc commented 1 month ago

There was another issue. I added the example from the PR description to dataization.yaml and checked stack test on master, and all the tests passed. But when I use a separate command

stack run normalizer -- dataize --recursive --chain --rules eo-phi-normalizer/test/eo/phi/rules/yegor.yaml program.phi

, I get the different (wrong) result. I wonder if it is something that I do wrong maybe?

fizruk commented 1 month ago

checked stack test on master

I think some tests use built-in normalizer instead of yegor.yaml. We should specify a matrix of rulesets (builtin and from yaml) to test on. @deemp can you help with that?

0crat commented 1 month ago

@fizruk Thanks for the review! You've earned +35 points for this: +25 as a basis; +5 for 6 hits-of-code; +5 for 2 comments. Your running balance is +107.

0crat commented 1 month ago

@eyihluyc Thanks for the contribution! You've earned +20 points for this: +20 as a basis; +7 for 78 hits-of-code; -7 for 7 comments of reviewers. Please, keep them coming. Your running balance is +10.