NDLI: The complexity of subtype entailment for simple types

Content Provider	IEEE Xplore Digital Library
Author	Henglein, F. Rehof, J.
Copyright Year	1997
Description	Author affiliation: Dept. of Comput. Sci., Copenhagen Univ., Denmark (Henglein, F.)
Abstract	A subtyping /spl tau//spl les//spl tau/' is entailed by a set of subtyping constraints C, written C \|=/spl tau//spl les//spl tau/', if every valuation (mapping of type variables to ground types) that satisfies C also satisfies /spl tau//spl les//spl tau/'. We study the complexity of subtype entailment for simple types over lattices of base types. We show that: deciding C \|=/spl tau//spl les//spl tau/' is coNP-complete; deciding C \|=/spl alpha//spl les//spl beta/ for consistent, atomic C and /spl alpha/, /spl beta/ atomic can be done in linear time. The structural lower (coNP-hardness) and upper (membership in coNP) bounds as well as the optimal algorithm for atomic entailment are new. The coNP-hardness result indicates that entailment is strictly harder than satisfiability, which is known to be in PTIME for lattices of base types. The proof of coNP-completeness gives an improved algorithm for deciding entailment and puts a precise complexity-theoretic marker on the intuitive "exponential explosion" in the algorithm. Central to our results is a novel characterization of C \|=/spl alpha//spl les//spl beta/ for atomic, consistent C. This is the basis for correctness of the linear-time algorithm as well as a complete axiomatization of C \|=/spl alpha//spl les//spl beta/ for atomic C by extending the usual proof rules for subtype inference. It also incorporates the fundamental insight for understanding the structural complexity bounds in the general case.
Starting Page	352
Ending Page	361
File Size	949222
Page Count	10
File Format	PDF
ISBN	0818679255
ISSN	10436871
DOI	10.1109/LICS.1997.614961
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1997-06-29
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Inference algorithms Calculus Lattices Power generation Computer science Cost accounting Explosions Computer languages Logic Power system modeling
Content Type	Text
Resource Type	Article
Subject	Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A lattice-valued modal propositional logic system LMP(X)

Type theory via exact categories

Complexity and expressive power of logic programming

Trichotomy in the Complexity of Minimal Inference

Axiomatization of Credulous Reasoning in Default Logics using Sequent Calculus

3-Valued Abstraction: More Precision at Less Cost

Types and programming languages: the next generation

On locality and uniform reduction

A Proof of Strong Normalisation using Domain Theory

The complexity of subtype entailment for simple types

Similar Documents

A lattice-valued modal propositional logic system LMP(X)

Type theory via exact categories

Complexity and expressive power of logic programming

Trichotomy in the Complexity of Minimal Inference

Axiomatization of Credulous Reasoning in Default Logics using Sequent Calculus

3-Valued Abstraction: More Precision at Less Cost

Types and programming languages: the next generation

On locality and uniform reduction

A Proof of Strong Normalisation using Domain Theory

The complexity of subtype entailment for simple types