Proof theory of higher-order equations: conservativity, normal forms and term rewriting
2003 (English)In: Journal of computer and system sciences (Print), ISSN 0022-0000, E-ISSN 1090-2724, Vol. 67, no 1, 127-173 p.Article in journal (Refereed) Published
We introduce a necessary and sufficient condition for the omega-extensionality rule of higher-order equational logic to be conservative over first-order many-sorted equational logic for ground first-order equations. This gives a precise condition under which computation in the higher-order initial model by term rewriting is possible. The condition is then generalised to characterise a normal form for higher-order equational proofs in which extensionality inferences occur only as the final proof inferences. The main result is based on a notion of observational equivalence between higher-order elements induced by a topology of finite information on such elements. Applied to extensional higher-order algebras with countable first-order carrier sets, the finite information topology is metric and second countable in every type.
Place, publisher, year, edition, pages
2003. Vol. 67, no 1, 127-173 p.
IdentifiersURN: urn:nbn:se:kth:diva-22682DOI: 10.1016/s0022-0000(03)00048-5ISI: 000184240900006OAI: oai:DiVA.org:kth-22682DiVA: diva2:341380
QC 201005252010-08-102010-08-10Bibliographically approved