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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

A sound and complete algorithm for nominal unification of higher-orderexpressions with a recursive let is described, and shown to run innondeterministic polynomial time. We also explore specializations like nominalletrec-matching for expressions, for DAGs, and for garbage-free expressions anddetermine their complexity. We also provide a nominal unification algorithm forhigher-order expressions with recursive let and atom-variables, where we showthat it also runs in nondeterministic polynomial time. In addition we provethat there is a guessing strategy for nominal unification with letrec andatom-variable that is a trade-off between exponential growth andnon-determinism. Nominal matching with variables representing partialletrec-environments is also shown to be in NP.

Nominal Unification and Matching of Higher Order Expressions with Recursive Let