English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 DetailsSummary
  Parametric Order‐sorted Types in Logic Programming

Hanus, M. (1991). Parametric Order‐sorted Types in Logic Programming. In S. Abramsky, & T. Maibaum (Eds.), TAPSOFT‐91 (pp. 181‒200). Berlin: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0023-C352-C Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0023-C353-A
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Hanus, Michael1, Author           
Affiliations:
1External Organizations, ou_persistent22              

Content

show
hide
Free keywords: -
 Abstract: This paper proposes a type system for logic programming where types are \u000Astructured in two ways. Firstly, functions and predicates may be declared with \u000Atypes containing type parameters which are universally quantified over all \u000Atypes. In this case each instance of the type declaration can be used in the \u000Alogic program. Secondly, types are related by subset inclusions. In this case a \u000Afunction or predicate can be applied to all subtypes of its declared type. \u000AWhile previous proposals for such type systems have strong restrictions on the \u000Asubtype relation, we assume that the subtype order is specified by Horn clauses \u000Afor the subtype relation ≤. This allows the declaration of a lot of \u000Ainteresting type structures, e.g., type constructors which are monotonic as \u000Awell as anti‐monotonic in their arguments. For instance, parametric \u000Aorder‐sorted type structures for logic programs with higher‐order predicates \u000Acan be specified in our framework. This paper presents the declarative and \u000Aoperational semantics of the typed logic language. The operational semantics \u000Arequires a unification procedure on well‐typed terms. This unification \u000Aprocedure is described by a set of transformation rules which generate a set of \u000Atype constraints from a given unification problem. The solvability of these \u000Atype constraints is decidable for particular type structures.

Details

show
hide
Language(s): eng - English
 Dates: 1991
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: Hanus91b
DOI: 10.1007/3540539816_67
 Degree: -

Event

show
hide
Title: International Joint Conference on Theory and Practice of Software Development
Place of Event: Brighton, UK
Start-/End Date: 1991-04-08 - 1991-04-12

Legal Case

show

Project information

show

Source 1

show
hide
Title: TAPSOFT‐91
  Subtitle : Proceedings of the International Joint Conference on Theory and Practice of Software Development Brighton, UK, April 8–12, 1991
  Abbreviation : TAPSOFT 1991
Source Genre: Proceedings
 Creator(s):
Abramsky, S., Editor
Maibaum, T.S.E., Editor
Affiliations:
-
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 181‒200 Identifier: -

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 494 Sequence Number: - Start / End Page: - Identifier: -