Wang, Yuting ;
Chaudhuri, Kaustuv
A Prooftheoretic Characterization of Independence in Type Theory
Abstract
For lambdaterms constructed freely from a type signature in a type theory such as LF, there is a simple inductive subordination relation that is used to control typeformation. There is a related—but not precisely complementary—notion of independence that asserts that the inhabitants of the function space tau_1 > tau_2 depend vacuously on their arguments. Independence has many practical reasoning applications in logical frameworks, such as pruning variable dependencies or transporting theorems and proofs between type signatures. However, independence is usually not given a formal interpretation. Instead, it is generally implemented in an ad hoc and uncertified fashion. We propose a formal definition of independence and give a prooftheoretic characterization of it by: (1) representing the inference rules of a given type theory and a closed type signature as a theory of intuitionistic predicate logic, (2) showing that typing derivations in this signature are adequately represented by a focused sequent calculus for this logic, and (3) defining independence in terms of strengthening for intuitionistic sequents. This scheme is then formalized in a metalogic, called G, that can represent the sequent calculus as an inductive definition, so the relevant strengthening lemmas can be given explicit inductive proofs. We present an algorithm for automatically deriving the strengthening lemmas and their proofs in G.
BibTeX  Entry
@InProceedings{wang_et_al:LIPIcs:2015:5173,
author = {Yuting Wang and Kaustuv Chaudhuri},
title = {{A Prooftheoretic Characterization of Independence in Type Theory}},
booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
pages = {332346},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897873},
ISSN = {18688969},
year = {2015},
volume = {38},
editor = {Thorsten Altenkirch},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5173},
URN = {urn:nbn:de:0030drops51736},
doi = {10.4230/LIPIcs.TLCA.2015.332},
annote = {Keywords: subordination; independence; sequent calculus; focusing; strengthening}
}
2015
Keywords: 

subordination; independence; sequent calculus; focusing; strengthening 
Seminar: 

13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Issue date: 

2015 
Date of publication: 

2015 