diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ ```bash cabal update -cabal install --overwrite-policy=always phino-0.0.136 +cabal install --overwrite-policy=always phino-0.0.137 phino --version ``` @@ -1332,103 +1332,103 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1810402.021 μs - avg: 181040.202 μs - min: 169827.114 μs - max: 204681.114 μs - std dev: 13154.216 μs + total: 1768043.411 μs + avg: 176804.341 μs + min: 164618.314 μs + max: 199224.069 μs + std dev: 13380.573 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 7538811.226 μs - avg: 753881.123 μs - min: 694204.271 μs - max: 840942.094 μs - std dev: 41681.127 μs + total: 7486501.601 μs + avg: 748650.160 μs + min: 678843.922 μs + max: 882138.403 μs + std dev: 54979.122 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 597613.462 μs - avg: 59761.346 μs - min: 54912.144 μs - max: 65342.026 μs - std dev: 2994.555 μs + total: 580244.769 μs + avg: 58024.477 μs + min: 53745.242 μs + max: 67886.567 μs + std dev: 3972.462 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 4130310.545 μs - avg: 413031.054 μs - min: 404823.433 μs - max: 426597.938 μs - std dev: 7495.509 μs + total: 3581738.830 μs + avg: 358173.883 μs + min: 353632.119 μs + max: 364450.476 μs + std dev: 3758.053 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 4284120.069 μs - avg: 428412.007 μs - min: 413571.324 μs - max: 445658.981 μs - std dev: 11624.236 μs + total: 3586003.643 μs + avg: 358600.364 μs + min: 348511.573 μs + max: 363372.650 μs + std dev: 4666.744 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 13724020.907 μs - avg: 1372402.091 μs - min: 1344331.661 μs - max: 1409368.695 μs - std dev: 17786.287 μs + total: 13668454.509 μs + avg: 1366845.451 μs + min: 1331880.047 μs + max: 1392431.918 μs + std dev: 20241.996 μs === morph/symbolic/demo/e1 === warmup: 3 iterations batches: 10 x 1 - total: 866700.384 μs - avg: 86670.038 μs - min: 86184.411 μs - max: 87168.132 μs - std dev: 285.902 μs + total: 902246.384 μs + avg: 90224.638 μs + min: 88957.751 μs + max: 91781.678 μs + std dev: 808.904 μs === morph/symbolic/demo/e2 === warmup: 3 iterations batches: 10 x 1 - total: 1188660.494 μs - avg: 118866.049 μs - min: 116047.655 μs - max: 136278.751 μs - std dev: 5832.266 μs + total: 1221686.976 μs + avg: 122168.698 μs + min: 119410.311 μs + max: 123946.713 μs + std dev: 1478.809 μs === morph/symbolic/demo/e3 === warmup: 3 iterations batches: 10 x 1 - total: 1867565.431 μs - avg: 186756.543 μs - min: 185066.327 μs - max: 187725.046 μs - std dev: 1004.396 μs + total: 1867130.933 μs + avg: 186713.093 μs + min: 182254.442 μs + max: 199500.578 μs + std dev: 4421.828 μs === morph/symbolic/demo/e4 === warmup: 3 iterations batches: 10 x 1 - total: 623551.322 μs - avg: 62355.132 μs - min: 61620.682 μs - max: 63797.384 μs - std dev: 728.465 μs + total: 638270.776 μs + avg: 63827.078 μs + min: 62286.130 μs + max: 64675.326 μs + std dev: 647.450 μs === morph/symbolic/demo/e5 === warmup: 3 iterations batches: 10 x 1 - total: 186679.533 μs - avg: 18667.953 μs - min: 18384.769 μs - max: 18868.158 μs - std dev: 149.307 μs + total: 189257.666 μs + avg: 18925.767 μs + min: 18570.345 μs + max: 19165.345 μs + std dev: 197.617 μs === morph/symbolic/native/e5 === - warmup: 1 iterations + warmup: 2 iterations batches: 4 x 1 - total: 17947336.400 μs - avg: 4486834.100 μs - min: 4167627.934 μs - max: 4633560.228 μs - std dev: 189453.769 μs + total: 17870892.725 μs + avg: 4467723.181 μs + min: 4368895.499 μs + max: 4581076.732 μs + std dev: 95768.713 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-09-22 at 19:05, +on 2026-09-23 at 19:07, on Linux with 4 CPUs. @@ -1478,4 +1478,4 @@ [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin [issue-1291]: https://github.com/objectionary/phino/issues/1291 -[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/35770947279 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/35906648654 diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino -version: 0.0.137 +version: 0.0.138 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/normalize/dot.yaml b/resources/normalize/dot.yaml --- a/resources/normalize/dot.yaml +++ b/resources/normalize/dot.yaml @@ -15,14 +15,26 @@ # dispatch this one covered alone. Where no universe is known — the 'rewrite' # command, and 'isNF' asking about a term on its own — 𝑒1 binds nothing, the # guard cannot hold, and this rule answers every dispatch as it always did. +# Neither rule dispatches on a formation holding both λ and Δ: 'dl' says such a +# formation is ⊥, and carrying it out into ρ would leave a ρ ↦ ⊥ in a normal +# form that 'dl' firing first reduces to ⊥ outright, so the answer would hang +# on rule order (#1395). name: dot pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1 e-match: 𝑒1 when: - not: - eq: - - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧ - - 𝑒1 + and: + - not: + eq: + - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧ + - 𝑒1 + - or: + - disjoint: + - [λ] + - [𝐵1, 𝐵2] + - disjoint: + - [Δ] + - [𝐵1, 𝐵2] result: 𝑒2(ρ ↦ ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧) where: - meta: 𝑒2 diff --git a/resources/normalize/dotg.yaml b/resources/normalize/dotg.yaml --- a/resources/normalize/dotg.yaml +++ b/resources/normalize/dotg.yaml @@ -11,14 +11,23 @@ # a dispatch reaches this rule only once Φ has already been resolved that way. # Everything else is 'dot': the same pattern, the same contextualization # context, and a guard that is the exact complement of the one there, so the -# two never both answer a dispatch and never both refuse one. +# two never both answer a dispatch and never both refuse one, save a formation +# holding both λ and Δ, which both refuse and leave to 'dl' (#1395). name: dotg pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1 e-match: 𝑒1 when: - eq: - - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧ - - 𝑒1 + and: + - eq: + - ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧ + - 𝑒1 + - or: + - disjoint: + - [λ] + - [𝐵1, 𝐵2] + - disjoint: + - [Δ] + - [𝐵1, 𝐵2] result: 𝑒2(ρ ↦ Φ) where: - meta: 𝑒2 diff --git a/src/Morph.hs b/src/Morph.hs --- a/src/Morph.hs +++ b/src/Morph.hs @@ -440,19 +440,21 @@ -- allows. Every entry is charged to the '--max-steps' budget, which is what -- bounds the walk. deepened :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) -deepened expr univ state ctx = go (Just ctx._site) Nothing ExXi expr state ctx +deepened expr univ state ctx = go False (Just ctx._site) Nothing ExXi expr state ctx where -- A term as it was written, together with the locator naming it where one -- does and with what its free ξ stands for: the formation the walk entered -- it from, without the binding it came from, exactly the context the 'dot' -- rule hands a dispatched body. At the top there is no such formation, so ξ -- stands for itself and contextualization leaves the term alone, and the - -- locator is the one the whole run was aimed at. - go :: Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) - go standing dispatched context term state' caller = do + -- locator is the one the whole run was aimed at. Whether the formation a + -- term is bound in has its ρ bound is what decides whether a void ρ keeps + -- a formation from being entered (see 'parts'); at the top there is none. + go :: Bool -> Maybe Expression -> Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) + go attached standing dispatched context term state' caller = do let here = sited standing caller ctx' <- deeper here - (walked, walkedState) <- parts standing context term state' here + (walked, walkedState) <- parts attached standing context term state' here (answer, answered) <- ctx'._fire dispatched (contextualize walked context) univ walkedState ctx' pure (fromMaybe walked answer, answered) -- The context a term is walked in, aimed at the term itself where a locator @@ -466,19 +468,36 @@ -- where they were, so the term keeps the shape it was written in. Only a -- binding of a formation carries the locator further: the head of a -- dispatch and both sides of an application stand under no attribute, so - -- what they hold is entered with no locator of its own. - parts :: Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) - parts standing _ (ExFormation bds) state' caller = do + -- what they hold is entered with no locator of its own. An abstract + -- formation, one holding a void, is a method nobody applied: its body is + -- parametric, walking it can only end in ⊥ or a stuck term, and a λ there + -- dataizing a parameter would end the whole run, so it is handed back as it + -- was written (#1393). A void ρ counts as well where the formation it is + -- bound in has its own ρ bound: ρ is the parameter a dispatch binds, and + -- 'dot' binds it in every copy a reduction reaches, so a formation still + -- holding ρ ↦ ∅ inside such a copy is a method nobody dispatched, and its + -- ξ.ρ can only collapse to ⊥ (#1397). The program as it was written holds + -- ρ ↦ ∅ all the way down, since nothing dispatched it either, and its + -- objects are walked the way they always were. + parts :: Bool -> Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) + parts attached _ _ term@(ExFormation bds) state' _ + | any abstract bds = pure (term, state') + where + abstract :: Binding -> Bool + abstract (BiVoid AtRho) = attached + abstract (BiVoid _) = True + abstract _ = False + parts _ standing _ (ExFormation bds) state' caller = do (entered, state'') <- bindings standing bds bds state' caller pure (ExFormation entered, state'') - parts _ context (ExDispatch target attr) state' caller = do - (entered, state'') <- go Nothing (Just attr) context target state' caller + parts _ _ context (ExDispatch target attr) state' caller = do + (entered, state'') <- go False Nothing (Just attr) context target state' caller pure (ExDispatch entered attr, state'') - parts _ context (ExApplication target arg) state' caller = do - (entered, state'') <- go Nothing Nothing context target state' caller + parts _ _ context (ExApplication target arg) state' caller = do + (entered, state'') <- go False Nothing Nothing context target state' caller (applied, state''') <- argument context arg state'' caller pure (ExApplication entered applied, state''') - parts _ _ term state' _ = pure (term, state') + parts _ _ _ term state' _ = pure (term, state') -- Walk the bindings of a formation left to right, threading the state -- through them. Only what the formation itself holds is entered: ρ names -- the object around it rather than one inside it, and a void, Δ or λ @@ -489,9 +508,13 @@ bindings _ _ [] state' _ = pure ([], state') bindings standing whole (BiTau attr body : rest) state' caller | attr /= AtRho = do - (entered, state'') <- go (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller + (entered, state'') <- go (any bound whole) (fmap (`ExDispatch` attr) standing) Nothing (scope attr whole) body state' caller (others, state''') <- bindings standing whole rest state'' caller pure (BiTau attr entered : others, state''') + where + bound :: Binding -> Bool + bound (BiTau AtRho _) = True + bound _ = False bindings standing whole (bd : rest) state' caller = do (others, state'') <- bindings standing whole rest state' caller pure (bd : others, state'') @@ -508,10 +531,10 @@ -- applies is walked by the caller and the argument it binds is walked here. argument :: Expression -> Argument -> State -> ReduceContext -> IO (Argument, State) argument context (ArTau attr arg) state' caller = do - (entered, state'') <- go Nothing Nothing context arg state' caller + (entered, state'') <- go False Nothing Nothing context arg state' caller pure (ArTau attr entered, state'') argument context (ArAlpha alpha arg) state' caller = do - (entered, state'') <- go Nothing Nothing context arg state' caller + (entered, state'') <- go False Nothing Nothing context arg state' caller pure (ArAlpha alpha entered, state'') -- The premise binding the given expression meta, if any. The conclusion of a diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -2197,12 +2197,12 @@ , "\\phinoNormalizationRule{dot}" , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" , " { e_2 ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }" - , " { [[ B_1, \\tau -> n, B_2 ]] \\not= e_1 }" + , " { [[ B_1, \\tau -> n, B_2 ]] \\not= e_1 \\;\\text{and}\\; \\lparen [ L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\;\\text{or}\\; [ D ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\rparen }" , " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_2 } }" , "\\phinoNormalizationRule{dotg}" , " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }" , " { e_2 ( \\phiTerminal{\\rho} -> Q ) }" - , " { [[ B_1, \\tau -> n, B_2 ]] = e_1 }" + , " { [[ B_1, \\tau -> n, B_2 ]] = e_1 \\;\\text{and}\\; \\lparen [ L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\;\\text{or}\\; [ D ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\rparen }" , " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_2 } }" , "\\phinoNormalizationRule{miss}" , " { [[ B ]] ( \\tau -> e ) }"