Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Proof theory of higher-order equations: conservativity, normal forms and term rewriting
KTH, Superseded Departments, Numerical Analysis and Computer Science, NADA.ORCID iD: 0000-0002-9706-5008
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
Abstract [en]

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.
Keyword [en]
algebra
Identifiers
URN: urn:nbn:se:kth:diva-22682DOI: 10.1016/s0022-0000(03)00048-5ISI: 000184240900006OAI: oai:DiVA.org:kth-22682DiVA: diva2:341380
Note
QC 20100525Available from: 2010-08-10 Created: 2010-08-10 Last updated: 2017-12-12Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Meinke, Karl

Search in DiVA

By author/editor
Meinke, Karl
By organisation
Numerical Analysis and Computer Science, NADA
In the same journal
Journal of computer and system sciences (Print)

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 19 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf