Post Aq5QAsQdeajeLbDmd6 by aram@mastodon.sdf.org
 (DIR) More posts by aram@mastodon.sdf.org
 (DIR) Post #Aq5QAsQdeajeLbDmd6 by aram@mastodon.sdf.org
       2025-01-14T22:18:48Z
       
       0 likes, 0 repeats
       
       I believe β-reduction in interaction combinators is not monotonic with respect to partial evaluation. In other words only program reduction (no free variables) is β-optimal. Is this true?
       
 (DIR) Post #Aq5QFpbvYfBB3VrdLc by aram@mastodon.sdf.org
       2025-01-14T22:19:45Z
       
       0 likes, 0 repeats
       
       Proof 1: partial evaluation can reduce irrelevant redexes in subnets that would be erased in lazy evaluation for specific inputs.
       
 (DIR) Post #Aq5QGx7X7eSYdWBLgu by aram@mastodon.sdf.org
       2025-01-14T22:19:52Z
       
       0 likes, 0 repeats
       
       Partial reduction of lambda bodies is "pessimistic" in the sense that the partial reduction has to work for all inputs, whereas specific inputs can entail different dynamic behaviors in the reduction of a complete program.
       
 (DIR) Post #Aq5QHGG1yHXvzNIu4e by aram@mastodon.sdf.org
       2025-01-14T22:20:00Z
       
       0 likes, 0 repeats
       
       Partial evaluation seems to imply some degree of strictness and be at odds with lazy evaluation.
       
 (DIR) Post #Aq5QItWrRk1O4oxGpU by aram@mastodon.sdf.org
       2025-01-14T22:20:07Z
       
       0 likes, 0 repeats
       
       I have a specific counter example in mind but it's for a non-λ-calculus system. I don't know if inets guarantee β-optimality for all computational systems or just for λ-calculus.
       
 (DIR) Post #Aq5QKnk3vwh8hw2Tmy by aram@mastodon.sdf.org
       2025-01-14T22:20:39Z
       
       0 likes, 0 repeats
       
       Lazy evaluation means we compute only what we need, but with partial evaluation we don't know what we're going to need.