Preservation under Substitution with Telescopes

Clash Royale CLAN TAG#URR8PPP

up vote
2
down vote

favorite

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":

• If $Gamma vdash v : tau_1$ and $(x : tau_1) vdash t : tau_2$,
  then $Gamma vdash [v/x]t : tau_2 $.

However, the proof of this relies on the property of permutation, that we can rearrange contexts and it will preserve typing of terms.

I'm wondering, can we prove a similar property for dependently typed languages? The problem is that, here, permutation may not hold, since telescopes are used in place of environments, and the types themselves may refer to variables. Moreover, since the types and terms overlap, we have to substitute in $Gamma$ and $tau_2$ as well.

Does anyone have a good reference to proving such a preservation property for a dependently typed language? Are there tricks that are used to avoid the permutations?

reference-request pl.programming-languages type-theory lambda-calculus dependent-type

share|cite|improve this question

asked 2 hours ago

jmite

705423

add a comment | 

up vote
2
down vote

favorite

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":

• If $Gamma vdash v : tau_1$ and $(x : tau_1) vdash t : tau_2$,
  then $Gamma vdash [v/x]t : tau_2 $.

However, the proof of this relies on the property of permutation, that we can rearrange contexts and it will preserve typing of terms.

I'm wondering, can we prove a similar property for dependently typed languages? The problem is that, here, permutation may not hold, since telescopes are used in place of environments, and the types themselves may refer to variables. Moreover, since the types and terms overlap, we have to substitute in $Gamma$ and $tau_2$ as well.

Does anyone have a good reference to proving such a preservation property for a dependently typed language? Are there tricks that are used to avoid the permutations?

reference-request pl.programming-languages type-theory lambda-calculus dependent-type

share|cite|improve this question

asked 2 hours ago

jmite

705423

add a comment | 

up vote
2
down vote

favorite

up vote
2
down vote

favorite

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":

• If $Gamma vdash v : tau_1$ and $(x : tau_1) vdash t : tau_2$,
  then $Gamma vdash [v/x]t : tau_2 $.

However, the proof of this relies on the property of permutation, that we can rearrange contexts and it will preserve typing of terms.

I'm wondering, can we prove a similar property for dependently typed languages? The problem is that, here, permutation may not hold, since telescopes are used in place of environments, and the types themselves may refer to variables. Moreover, since the types and terms overlap, we have to substitute in $Gamma$ and $tau_2$ as well.

Does anyone have a good reference to proving such a preservation property for a dependently typed language? Are there tricks that are used to avoid the permutations?

reference-request pl.programming-languages type-theory lambda-calculus dependent-type

share|cite|improve this question

asked 2 hours ago

jmite

705423

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution":

• If $Gamma vdash v : tau_1$ and $(x : tau_1) vdash t : tau_2$,
  then $Gamma vdash [v/x]t : tau_2 $.

However, the proof of this relies on the property of permutation, that we can rearrange contexts and it will preserve typing of terms.

I'm wondering, can we prove a similar property for dependently typed languages? The problem is that, here, permutation may not hold, since telescopes are used in place of environments, and the types themselves may refer to variables. Moreover, since the types and terms overlap, we have to substitute in $Gamma$ and $tau_2$ as well.

Does anyone have a good reference to proving such a preservation property for a dependently typed language? Are there tricks that are used to avoid the permutations?

reference-request pl.programming-languages type-theory lambda-calculus dependent-type

reference-request pl.programming-languages type-theory lambda-calculus dependent-type

share|cite|improve this question

asked 2 hours ago

jmite

705423

share|cite|improve this question

asked 2 hours ago

jmite

705423

share|cite|improve this question

share|cite|improve this question

asked 2 hours ago

jmite

705423

asked 2 hours ago

jmite

705423

asked 2 hours ago

jmite

705423

705423

add a comment | 

add a comment | 

1 Answer
1

active

oldest

votes

up vote
3
down vote

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation)

The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove

• If $Gamma vdash t_1 : tau_1$ and $Gamma, x : tau_1, Delta vdash t_2 : tau_2$ then $Gamma,Delta[t_1/x] vdash t_2[t_1/x] : tau_2[t_1/x]$
  

share|cite|improve this answer

answered 1 hour ago

Max New

630416

add a comment | 

Your Answer

StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "114"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
convertImagesToLinks: false,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: null,
bindNavPrevention: true,
postfix: "",
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcstheory.stackexchange.com%2fquestions%2f41816%2fpreservation-under-substitution-with-telescopes%23new-answer', 'question_page');

);

Post as a guest

Name Email

1 Answer
1

active

oldest

votes

1 Answer
1

active

oldest

votes

active

oldest

votes

active

oldest

votes

up vote
3
down vote

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation)

The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove

• If $Gamma vdash t_1 : tau_1$ and $Gamma, x : tau_1, Delta vdash t_2 : tau_2$ then $Gamma,Delta[t_1/x] vdash t_2[t_1/x] : tau_2[t_1/x]$
  

share|cite|improve this answer

answered 1 hour ago

Max New

630416

add a comment | 

up vote
3
down vote

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation)

The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove

• If $Gamma vdash t_1 : tau_1$ and $Gamma, x : tau_1, Delta vdash t_2 : tau_2$ then $Gamma,Delta[t_1/x] vdash t_2[t_1/x] : tau_2[t_1/x]$
  

share|cite|improve this answer

answered 1 hour ago

Max New

630416

add a comment | 

up vote
3
down vote

up vote
3
down vote

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation)

The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove

• If $Gamma vdash t_1 : tau_1$ and $Gamma, x : tau_1, Delta vdash t_2 : tau_2$ then $Gamma,Delta[t_1/x] vdash t_2[t_1/x] : tau_2[t_1/x]$
  

share|cite|improve this answer

answered 1 hour ago

Max New

630416

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation)

The key is that you need to generalize the inductive hypothesis to when the variable in t appears in a context. So for a dependent type theory you prove

• If $Gamma vdash t_1 : tau_1$ and $Gamma, x : tau_1, Delta vdash t_2 : tau_2$ then $Gamma,Delta[t_1/x] vdash t_2[t_1/x] : tau_2[t_1/x]$
  

share|cite|improve this answer

answered 1 hour ago

Max New

630416

share|cite|improve this answer

share|cite|improve this answer

answered 1 hour ago

Max New

630416

answered 1 hour ago

Max New

630416

answered 1 hour ago

Max New

630416

630416

add a comment | 

add a comment | 

 

draft saved

draft discarded

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcstheory.stackexchange.com%2fquestions%2f41816%2fpreservation-under-substitution-with-telescopes%23new-answer', 'question_page');

);

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Name Email

Name

Email

Name Email

Name

Email