Timeline for Explanation of the definition of Saturated Sets in Lambda Calculus

6 events

when toggle format	what		by	license	comment
May 14, 2015 at 13:23	vote	accept	meditans
May 14, 2015 at 13:21	comment	added	meditans		Ok, I got it now, I was missing the fact that, in order to show that $\lambda x.b[\vec{x}:=\vec{g}] \in [\![\alpha \rightarrow \beta]\!]$, I had also to show that $\lambda x.b [\vec{x} := \vec{g}]$ is strongly normalizing, so it's important for a saturated set to contain all the variables in order to do the sostitution you hinted to, hence the first condition. Thank you again, wish I could upvote your answer more than once!
May 14, 2015 at 1:08	history	edited	cody	CC BY-SA 3.0	Clarify condition 1)
May 14, 2015 at 1:06	comment	added	cody		I'll amend my answer.
May 14, 2015 at 0:56	comment	added	meditans		Hi cody, this is exactly the type of answer I was looking for, thank you very much! Before I mark this as accepted, could you clarify a bit the justification for the first property? Why should I apply the substitution $t\, [\vec{x} := \vec{x}]$, in the context of this proof for STLC?
May 13, 2015 at 23:58	history	answered	cody	CC BY-SA 3.0