headers
Philip Wadler | 27 Apr 2012 13:14
Picon
Picon
Favicon

[TYPES] Is naive freshness adequate to avoid capture?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Say that a lambda term is 'fresh' if each lambda abstraction binds a
distinct variable.  For instance, (\x.(\y.\z.y)x) is fresh, but
(\x.(\y.\x.y)x) is not.

Consider lambda terms without the alpha rule, where capture avoiding
substitution is a partial function.  For instance, [x/y](\z.y) is
defined, but [x/y](\x.y) is undefined, because the substitution would
result in capture.

Consider a sequence of beta reductions where no alpha reduction is
allowed.  In our first example, this terminates in a normal form:

  (\x.(\y.\z.y)x) -->  \x.\z.x

In our second example, we get stuck.

  (\x.(\y.\x.y)x) -/->

Attempting to beta reduce the redex would result in capture.

Starting with a fresh term and performing beta reductions but no alpha
reductions, are there reduction sequences which get stuck?  I suspect
the answer is yes, but I am having difficulty locating a
counter-example in the literature or creating one on my own.

Answers gratefully received.  Yours,  -- P

--

--
(Continue reading)

Permalink | Reply | 0 comments |
headers
Ben Karel | 27 Apr 2012 17:19
Picon
Gravatar

Re: [TYPES] Is naive freshness adequate to avoid capture?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

http://cstheory.stackexchange.com/questions/8947/closed-term-and-alpha-conversion

On Fri, Apr 27, 2012 at 7:14 AM, Philip Wadler <wadler@...> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
> Say that a lambda term is 'fresh' if each lambda abstraction binds a
> distinct variable.  For instance, (\x.(\y.\z.y)x) is fresh, but
> (\x.(\y.\x.y)x) is not.
>
> Consider lambda terms without the alpha rule, where capture avoiding
> substitution is a partial function.  For instance, [x/y](\z.y) is
> defined, but [x/y](\x.y) is undefined, because the substitution would
> result in capture.
>
> Consider a sequence of beta reductions where no alpha reduction is
> allowed.  In our first example, this terminates in a normal form:
>
>  (\x.(\y.\z.y)x) -->  \x.\z.x
>
> In our second example, we get stuck.
>
>  (\x.(\y.\x.y)x) -/->
>
> Attempting to beta reduce the redex would result in capture.
>
> Starting with a fresh term and performing beta reductions but no alpha
> reductions, are there reduction sequences which get stuck?  I suspect
(Continue reading)

Permalink | Reply | 0 comments |
headers
Philip Wadler | 27 Apr 2012 17:26
Picon
Picon
Favicon

Re: [TYPES] Is naive freshness adequate to avoid capture?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Bentiamino,  Many thanks for your counter-example.  Yours, -- P

On Fri, Apr 27, 2012 at 4:19 PM, Beniamino Accattoli
<beniamino.accattoli@...> wrote:
> Dear Philip,
> My first observation has been that it is easy to break "freshness",
> just consider the reduction of \delta \delta. But in this case is
> however possible to reduce without ever using alpha.
>
> If I understand the problem correctly, this is a counter-example for
> both freshness and alpha:
>
> (\l z.zz) (\ly.\lx.yx)
> ->
> (\ly.\lx.yx) (\ly.\lx.yx)
> ->
> \lx.((\ly.\lx.yx)x)
> -/->
>
> Best,
> Beniamino Accattoli
>
> On Fri, Apr 27, 2012 at 1:14 PM, Philip Wadler <wadler@...> wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> Say that a lambda term is 'fresh' if each lambda abstraction binds a
>> distinct variable.  For instance, (\x.(\y.\z.y)x) is fresh, but
>> (\x.(\y.\x.y)x) is not.
(Continue reading)

Permalink | Reply | 0 comments |
headers
George Cherevichenko | 27 Apr 2012 22:31
Picon

[TYPES] Explicit renaming of bound variables

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

 Hello.
I think I have  found "the right definition" of substitution and
alpha-conversion. Three main ideas are:
1) Contexts with multiplicity (i.e., repetitions of variables are
permitted);
2) A new form of explicit substitutions;
3) A new definition of free variables.
Renaming of bound variables when performing substitutions is done using
special reductions and may be delayed.
So far told two people: Lev Beklemishev and Mati Pentus (both like).
George.

http://arxiv.org/abs/1111.3171
Permalink | Reply | 0 comments |
headers
Rene Vestergaard | 28 Apr 2012 00:13
Picon

Re: [TYPES] Is naive freshness adequate to avoid capture?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

All residual (non-renaming) beta-steps are enabled for fresh terms, 
i.e., all beta-reductions of redexes that are not newly created with 
respect to the fresh term we start from have enabled renaming-free 
substitutions. This follows from (what Vincent van Oostrom once told me 
is called) Hyland's Disjointness Property: within beta-residual theory, 
two descendants of a given redex are disjoint, i.e., neither contains 
the other.

Theorem 2.17 in my PhD thesis (The primitive proof of the 
lambda-calculus) shows that any sequence of residual beta-steps from a 
fresh term can be residually-completed. The setting of the result is the 
marked lambda-calculus, with a marked and an unmarked application 
constructor and only (renaming-free) beta-reduction for the former kind. 
Residual completion is the (partial) function that attempts to contract 
all marked redexes inside-out.

Hope this help with the slightly bigger picture,
Rene

On 4/27/12 8:14 PM, Philip Wadler wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Say that a lambda term is 'fresh' if each lambda abstraction binds a
> distinct variable.  For instance, (\x.(\y.\z.y)x) is fresh, but
> (\x.(\y.\x.y)x) is not.
>
> Consider lambda terms without the alpha rule, where capture avoiding
> substitution is a partial function.  For instance, [x/y](\z.y) is
(Continue reading)

Permalink | Reply | 0 comments |
headers
LD | 28 Apr 2012 00:41
Picon

Re: [TYPES] Is naive freshness adequate to avoid capture?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

[Resending from former email address as current one is rejected by  
list.]

Dear Philip,

Such freshness resembles usual axiomatisations in proof-theoretic
logical treatments of (typed) lambda calculus.

Keeping track of lambda subterm free variables invariantly for beta and
eta (open) reduction (working like a static type) avoids variable  
capture,
dispensing alpha conversion and simplifying substitution (N/y of term N
for variable y) to replacement (otherwise in general possibly  
capturing).

Write

X for an useq; ie sequence without repetitions of free variables (eg  
x,y,z)

X # Y for disjoint X and Y ie when X and Y have no common elements

[X]M for an (X free variables) annotated lambda term M; derived by rules
	[X,y,Z]y if (X # Z and X # y and y # Z); ie all pairwise disjoint

	[X](M N) if ([X]M and [X]N)

	[X](\y.M) if (X # y and [X,y]M)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Vincent van Oostrom | 28 Apr 2012 14:56
Picon

Re: [TYPES] Is naive freshness adequate to avoid capture?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Maybe it's interesting to note that each of the three reduction steps
of the canonical counterexample as given by Beniamonino corresponds
to a phenomenon that, when forbidden, yields a calculus that
is safe (cf. the work of Blum and Ong in the typed case),
in the sense that the initial term can be renamed
such that alpha-free-substitution is correct during reduction:
(1) Duplicating step. Forbidding gives linear lambda-calculus;
(2) Created step. Forbidding gives developments (Rene points out);
(3) Step below lambda. Forbidding gives weak reduction.
For more on this see pp. 24-38 of our presentation:
http://www.phil.uu.nl/~oostrom/publication/talk/terese181110.pdf
In the corresponding paper (also available from my homepage):
http://dx.doi.org/10.1016/j.tcs.2011.04.011
it is shown that mu-reduction as captured by the rule
   mu x.Z(x) -> Z(mu x.Z(x))
is safe in the above sense (without more). A general setting
encompassing both the mu-rule and developments as in (2) above, is
provided by a certain class of higher-order recursive program schemes
for which "self-capture-freeness" is preserved under reduction
(freshness is not preserved as Beniamonino points out).

kind regards,
Vincent van Oostrom

On 28-04-12 00:13, Rene Vestergaard wrote:
> [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
(Continue reading)

Permalink | Reply | 0 comments |
headers
Vladimir Voevodsky | 29 Apr 2012 16:10
Favicon

[TYPES] strict unit type

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

let Pt be the unit type ("one point"). In Coq-like systems it is introduced through an eliminator and the
associated iota-reduction rule. This is in practice sufficient for proving all its expected properties
modulo propositional equality (or identity types) but does not create a terminal object in the category
of contexts. 

I wonder if any one has considered type theories where Pt is introduced as having a distinguished object tt
together with reduction rules of the following form (in the absence of dependent sums, otherwise one
needs more):

1. any object of Pt other than tt reduces to tt,

2. Prod x : T , Pt reduces to Pt,

3. Prod x : Pt , T reduces to T.

Thanks,
Vladimir.
Permalink | Reply | 0 comments |

Gmane