Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Confluence tests for new rules fail #569

Open
2 tasks
deemp opened this issue Nov 27, 2024 · 0 comments
Open
2 tasks

Confluence tests for new rules fail #569

deemp opened this issue Nov 27, 2024 · 0 comments
Assignees
Labels
(normalization rules) Related to normalization rules

Comments

@deemp
Copy link
Member

deemp commented Nov 27, 2024

Details

@eyihluyc, @Anatolay, I ran the tests locally and discovered this critical pair.

  test/Language/EO/Rules/PhiPaperSpec.hs:341:9: 
  1) Language.EO.Rules.PhiPaper, New Yegor's rules, Are confluent (via QuickCheck)
       Falsified (after 692 tests and 6 shrinks):
         Source term:
           ⟦
           φ ↦ ⟦
             ρ ↦ ⟦
               v5 ↦ ∅
             ⟧
             (
               v5 ↦ ⟦ ⟧
             )
           ⟧
           .ρ
         ⟧
         
         Critical pair:
           Using rule 'DOT': ⟦
           φ ↦ ⟦
             v5 ↦ ∅
           ⟧
           (
             v5 ↦ ⟦ ⟧
           )
           (
             ρ ↦ ⟦
               ρ ↦ ⟦
                 v5 ↦ ∅
               ⟧
               (
                 v5 ↦ ⟦ ⟧
               )
             ⟧
           )
         ⟧
         
           Using rule 'COPY': ⟦
           φ ↦ ⟦
             ρ ↦ ⟦
               v5 ↦ ⟦ ⟧
             ⟧
         ()
           ⟧
           .ρ
         ⟧
         

  To rerun use: --match "/Language.EO.Rules.PhiPaper/New Yegor's rules/Are confluent (via QuickCheck)/" --seed 1547631552

Randomized with seed 1547631552

Subtasks

  • Try to reproduce with the eo-phi-normalizer on master
  • Try running 2000 tests to discover other critical pairs
@deemp deemp added the (normalization rules) Related to normalization rules label Nov 27, 2024
@deemp deemp changed the title New rules aren't confluent Confluence tests for new rules fail Nov 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
(normalization rules) Related to normalization rules
Projects
None yet
Development

No branches or pull requests

3 participants