| dbo:abstract
|
- Nominal terms are a metalanguage for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence (equivalence up to a permutative renaming of bound names). Nominal terms came out of a programme of research into nominal sets, and have a concrete semantics in those sets. Where the regular unification found in Prolog is linear in the size of terms compared, the extension to faithfully capture equivalence of nominal terms, called nominal unification in the literature, is quadratic (Calvès 2013). Based on an earlier PTIME algorithm for nominal unification, is a Prolog-like logic programming language with facilities for binding names in terms, which was intended to be useful for programs acting on program syntax (Cheney 2004). Nominal term embeddings may be seen as alternatives to de Bruijn encodings and higher-order abstract syntax, where the latter uses the simply typed lambda calculus as a metalanguage. (en)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 6628 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdfs:comment
|
- Nominal terms are a metalanguage for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence (equivalence up to a permutative renaming of bound names). Nominal terms came out of a programme of research into nominal sets, and have a concrete semantics in those sets. (en)
|
| rdfs:label
|
- Nominal terms (computer science) (en)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
