| 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 |
https://hal.inria.fr/hal-00926833/document https://homepages.inf.ed.ac.uk/jcheney/publications/thesis-informal.ps |
| dbo:wikiPageID |
27345568 (xsd:integer) |
| dbo:wikiPageLength |
6628 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID |
1053266524 (xsd:integer) |
| dbo:wikiPageWikiLink |
dbr:Programming_languages dbr:Prolog dbr:Unification_(computer_science) dbr:De_Bruijn_index dbr:Compiler dbr:Nominal_techniques dbr:Simply_typed_lambda_calculus dbr:Logic_programming dbr:First-order_logic dbc:Theoretical_computer_science dbr:Lambda_calculus dbr:Higher-order_abstract_syntax dbr:Logics dbr:Metalanguage dbr:Undecidable_problem dbr:Lambda-calculus dbr:LambdaProlog dbr:Pi-calculus dbr:Abstract_syntax_trees dbr:Computer_scientists dbr:Unification_(computing) dbr:AlphaProlog |
| dbp:wikiPageUsesTemplate |
dbt:Cite_conference dbt:Cite_journal dbt:Cite_thesis dbt:Clarify dbt:Empty_section |
| dct:subject |
dbc:Theoretical_computer_science |
| gold:hypernym |
dbr:Metalanguage |
| 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 |
freebase:Nominal terms (computer science) wikidata:Nominal terms (computer science) https://global.dbpedia.org/id/4sW7e |
| prov:wasDerivedFrom |
wikipedia-en:Nominal_terms_(computer_science)?oldid=1053266524&ns=0 |
| foaf:isPrimaryTopicOf |
wikipedia-en:Nominal_terms_(computer_science) |
| is dbo:wikiPageDisambiguates of |
dbr:Nominal_terms |
| is dbo:wikiPageWikiLink of |
dbr:Nominal_techniques dbr:Nominal_terms |
| is foaf:primaryTopic of |
wikipedia-en:Nominal_terms_(computer_science) |