English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The algebraic intersection type unification problem is an important componentin proof search related to several natural decision problems in intersectiontype systems. It is unknown and remains open whether the algebraic intersectiontype unification problem is decidable. We give the first nontrivial lower boundfor the problem by showing (our main result) that it is exponential time hard.Furthermore, we show that this holds even under rank 1 solutions (substitutionswhose codomains are restricted to contain rank 1 types). In addition, weprovide a fixed-parameter intractability result for intersection type matching(one-sided unification), which is known to be NP-complete.  We place the algebraic intersection type unification problem in the contextof unification theory. The equational theory of intersection types can bepresented as an algebraic theory with an ACI (associative, commutative, andidempotent) operator (intersection type) combined with distributivityproperties with respect to a second operator (function type). Although theproblem is algebraically natural and interesting, it appears to occupy ahitherto unstudied place in the theory of unification, and our investigation ofthe problem suggests that new methods are required to understand the problem.Thus, for the lower bound proof, we were not able to reduce from known resultsin ACI-unification theory and use game-theoretic methods for two-player tilinggames.

The Algebraic Intersection Type Unification Problem