Loading...
Please wait, while we are loading the content...
Similar Documents
Permissive nominal terms and their unication
| Content Provider | Semantic Scholar |
|---|---|
| Author | Dowek, Gilles Gabbay, Murdoch James Mulligan, Dominic P. |
| Copyright Year | 2009 |
| Abstract | We introduce permissive nominal terms, and their unication. Nominal terms are one way to extend rst-order terms with binding. However, they lack some useful properties of rst- and higher-order terms: Terms must be reasoned about in a context of ‘freshness assumptions’; it is not always possible to ‘choose a fresh variable symbol’ for a nominal term; and it is not always possible to ‘ -convert a bound variable symbol’. Permissive nominal terms closely resemble nominal terms, but they recover these useful ‘always fresh’ and ‘always alpha-rename’ properties, familiar from rst- and higherorder syntax. In the permissive world, freshness contexts are elided, and the notion of unier is based on substitution alone, rather than on nominal terms’ notion of substitution plus freshness conditions. We prove that expressivity is not lost moving to the permissive case. We provide a translation from nominal terms into permissive nominal terms and we prove that a nominal unication problem is solvable if and only if its translation into permissive nominal terms is. Finally, we investigate the precise relation between nominal unication and Miller’s higher-order pattern unication. We translate nominal terms into the -calculus and show that the translation may also be applied to unication problems; the result is pattern unication. This cements an existing intuition that higher-order patterns are what is needed to unify encodings of nominal terms. This builds on a translation by Levy and Villaret, and renes it; both translations are parameterised by sets of atoms, but we identify a smaller parameter set and prove that it is as small as possible. We also translate solutions of nominal unication problems to solutions of higher-order pattern unication problems. We exhibit a general class of higher-order pattern solutions and show that every pattern solution in that class is the translation of a nominal unication solution up to a permutative renaming. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://dominic-mulligan.co.uk/files/papers/dowek-permissive-2009.pdf |
| Alternate Webpage(s) | http://www.gabbay.org.uk/papers/perntu.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
