Typy proste

(1)

Typy proste

15 kwietnia 2013

(2)

Simple types

Types:

I Type constant 0 is a type.

I If σ and τ are types then (σ → τ) is a type.

Alternatywne podej±cie: inne staªe lub zmienne typowe.

Konwencja:

I Zamiast (τ → (σ → ρ)) piszemy τ → σ → ρ.

Ka»dy typ ma posta¢ τ₁ → · · · → τ_n→atom.

(3)

Church style syntax (orthodox)

Assume innite setsVτ of variables of each type τ.

Dene setsTτ of terms of type τ:

I A variable of type τ is a term of type τ;

I If M ∈ Tσ→τ and N ∈ Tσ then (MN) ∈ Tτ;

I If M ∈ Tτ and x ∈ Vσ then (λx M) ∈ Tσ→τ. Write M^σ for M ∈ Tσ and dene beta-reduction by

(λx^σ.M^τ)N^σ ⇒M[x^σ :=N].

◦

(4)

Church and Curry

Church style:

I New syntax, built-in types.

I Every term has exactly one type.

I No untypable terms.

Curry style:

I Ordinary untyped lambda-terms.

I Types are derivable properties of terms.

I System of type assignment rules.

I A term may have many types or none.

I Typability not obvious.

(5)

Non-orthodox Church

Type-assignment with type annotations on bound variables.

Γ (x : σ) ` x : σ (Var)

Γ(x : σ) ` M : τ

(Abs) Γ `λx:σ M : σ → τ

Γ ` M : σ → τ Γ ` N : σ

(App) Γ `MN : τ

Fact:

If Γ ` M : τ and Γ ` M : σ then τ = σ.

◦

(6)

Relating systems

Orthodox Church terms are like

I Non-orthodox terms in a xed innite environment.

I Curry-style type derivations.

Konwencja: Typy jako górne indeksy, np.

(λx^σM^τ)N^σ : τ

◦

(7)

Properties

Subject reduction property:

Beta-eta reduction preserves types.

Strong normalization:

Every typed term is strongly normalizing.

◦

(8)

Denable functions

Liczebniki Churchan = λfx. fⁿ(x)maj¡ ka»dy typ postaci ω_σ = (σ → σ) → (σ → σ).

A function f : N^k → N is β-denablein type ωσ if there is a closed term F such that

I `F : ωσ → · · · → ω_σ → ω_σ;

I If f (n₁, . . . ,n_k) = m then F n₁. . .n_k =_β m.

◦

(9)

Examples

I Addition: λn^ω^σλm^ω^σλf^σ→σλx^σ.nf (mfx);

I Multiplication: λn^ω^σλm^ω^σλf^σ→σλx^σ.n(mf )x;

I Test for zero (if n = 0 then m else k): λn^ω^σλm^ω^σλk^ω^σλf^σ→σλx^σ.n(λy^σ.kfx)(mfx).

◦

(10)

Examples

I Test for zero (if n = 0 then m else k): λn^ω^σλm^ω^σλk^ω^σλf^σ→σλx^σ.n(λy^σ.kfx)(mfx).

◦

(11)

Examples

I Test for zero (if n = 0 then m else k):

λn^ω^σλm^ω^σλk^ω^σλf^σ→σλx^σ.n(λy^σ.kfx)(mfx).

◦

(12)

Extended polynomials (wielomiany warunkowe)

The least class of functions containing:

I Addition;

I Multiplication;

I Test for zero;

I Constants zero and one;

I Projections,

and closed under compositions.

Example: f (x, y) = if x = 0 then if y = 0 then p₁(x, y) else p2(x, y) else if y = 0 then p3(x, y) else p4(x, y).

(13)

Denable functions

Theorem (H. Schwichtenberg'76):

For every σ the functions beta-denable in type ωσ

are exactly the extended polynomials.

◦

(14)

More denable functions

A function f is non-uniformly denable if there is a closed term F such that

I `F : ωσ₁ → · · · → ω_σ_k → ω_σ;

I If f (n1, . . . ,nk) = m then F n1. . .nk =_β m.

Examples:

I The predecessor function p(n) =n −^· 1 and the exponentiation function exp(m, n) =mⁿ are non-uniformly denable. (Easy)

I The subtraction minus(m, n) =m −^· n and equality test Eq(m, n) =if m = n then 0 else 1 are not denable non-uniformly. (Hard)

◦

(15)

More denable functions

I `F : ωσ₁ → · · · → ω_σ_k → ω_σ;

Examples:

◦

(16)

More denable functions

I `F : ωσ₁ → · · · → ω_σ_k → ω_σ;

Examples:

(17)

Equality

Theorem (R. Statman'79):

The equality problem Are two well-typed terms beta-equal?

is non-elementary. That is, for no xed k it is solvable in time

2²

···2n9

=

; k

Exercise:

How long is the normal form of 2 · · · 2xy?

◦

(18)

Equality

Theorem (R. Statman'79):

The equality problem Are two well-typed terms beta-equal?

is non-elementary. That is, for no xed k it is solvable in time

2²

···2n9

=

; k

Exercise:

How long is the normal form of 2 · · · 2xy?

◦

(19)

The inhabitation problem

Inhabitation problem:

Given Γ, τ, is there M such that Γ ` M : τ?

Fact (R. Statman):

Inhabitation in simple types is decidable and Pspace-complete.

◦

(20)

The inhabitation problem

Inhabitation problem:

Given Γ, τ, is there M such that Γ ` M : τ?

Fact (R. Statman):

Inhabitation in simple types is decidable and Pspace-complete.

◦

(21)

Representing data types

I Natural numbers are generated by

I Constant 0 : int;

I Successor s : int → int.

They correspond to long normal forms of type ω = (0 → 0) → 0 → 0

I Words over {a, b} are generated by

I Constant ε : word;

I Two successors λλw (a · w) and λλw (b · w) of type word → word.

They correspond to long normal forms of type word = (0 → 0) → (0 → 0) → 0 → 0

◦

(22)

Representing data types

I Constant 0 : int;

◦

(23)

Representing data types

I Constant 0 : int;

◦

(24)

Representing data types

I Constant 0 : int;

(25)

Representing data types

I Binary trees are generated by

I Constant nil : tree;

I Constructor cons : tree → tree → tree.

They correspond to long normal forms of type tree = (0 → 0 → 0) → 0 → 0 Generalization:

Free algebras correspond to types of order two, i.e, of the form (0ⁿ¹ →0) → · · · → (0ⁿ^k →0) → 0

◦

(26)

Representing data types

They correspond to long normal forms of type tree = (0 → 0 → 0) → 0 → 0

Generalization:

◦

(27)

Representing data types

They correspond to long normal forms of type tree = (0 → 0 → 0) → 0 → 0 Generalization:

◦

(28)

Type reducibility

Denition: Type τ is reducible to type σ i there exists a closed term Φ : τ → σ such that the operator λλM:τ. ΦM is injective on closed terms, i.e.,

ΦM₁ =_βη ΦM₂ implies M₁ =_βη M₂ for closed M₁,M₂ : τ.

Theorem (R. Statman):

Every type over a single type constant 0 is reducible to tree.

◦

(29)

Type reducibility

Denition: Type τ is reducible to type σ i there exists a closed term Φ : τ → σ such that the operator λλM:τ. ΦM is injective on closed terms, i.e.,

ΦM₁ =_βη ΦM₂ implies M₁ =_βη M₂ for closed M₁,M₂ : τ.

Theorem (R. Statman):

Every type over a single type constant 0 is reducible to tree.

◦

(30)

Semantics for nite types

Assumptions:

I Orthodox Church style;

I Only one atomic type 0;

I Extensional equality =βη.

◦

(31)

Standard model M(A)

I Basic domain D0 =A;

I Function domains: Dσ→τ =Dσ →Dτ;

I Obvious semantics:

I [[x]]v =v(x);

I [[MN]]v = [[M]]v([[N]]v);

I [[λx^τ.M]]_v = λλd∈Dτ. [[M]]_v[x7→d].

◦

(32)

Completeness

Theorem (Harvey Friedman):

Terms are βη-equal i they are equal in M(N).

Proof:

Dene partial surjections ϕ_σ :Dσ −◦ T^σ/₌_βη by induction: For σ = 0 take ϕ₀ : N → T0/₌_βη to be any (total) surjection. (Terms of base type are represented by their numbers.) For function types, we represent (the behaviour of) lambda-terms using integer functions, so that:

ϕσ(ab) = ϕτ →σ(a)ϕτ(b).

◦

(33)

Completeness

Theorem (Harvey Friedman):

Terms are βη-equal i they are equal in M(N).

Proof:

Dene partial surjectionsϕ_σ :Dσ −◦ T^σ/₌_βη by induction:

For σ = 0 take ϕ₀ : N → T0/₌_βη to be any (total) surjection.

(Terms of base type are represented by their numbers.) For function types, we represent (the behaviour of) lambda-terms using integer functions, so that:

ϕσ(ab) = ϕτ →σ(a)ϕτ(b).

◦

(34)

Completeness proof

Given ϕσ :Dσ −◦ T^σ/₌_βη and ϕτ :Dτ −◦ T^τ/₌_βη,

we say that a function f : Dτ →Dσ represents a term M^{τ →σ} when (informally) the following diagram commutes:

Dτ f //

ϕτ

Dσ

ϕσ

Tτ/=_βη

λλt. Mt

//Tσ/=_βη

For any M, there exists such an f (not unique).

For a given f , such an M (if exists) is unique up to βη.

(35)

Completeness proof

Dene partial surjectionsϕ_σ :Dσ −◦ T^σ/₌_βη by induction:

I ϕ₀ : N → T0/₌_βη is any (total) surjection.

I ϕ_{τ →σ}(f ) = [M]=βη when f represents M.

Abbreviation: If d ∈ Dσ, write d for ϕσ(d).

Main property:

If f and e are dened then f (e) is dened andf e =βη f (e)

◦

(36)

Partial epimorphism: f e =

^βη

f (e)

e

Dτ f //

ϕτ

Dσ

ϕσ

f (e)

e Tτ/₌_βη

λλt. Mt

f //Tσ/₌_βη f (e)

◦

(37)

Completeness proof

Lemma:

Take v so that v(x) = x, for all x. Then M =βη [[M]]v, all M.

Main Proof:

Let M(N) |= M = N. Then [[M]]v = [[N]]v, for all v, in particular for v as above. Therefore

M =βη [[M]]v =βη [[N]]v =βη N.

◦

(38)

Completeness proof

Lemma:

Take v so that v(x) = x, for all x. Then M =βη [[M]]v, all M.

Main Proof:

Let M(N) |= M = N. Then [[M]]v = [[N]]v, for all v, in particular for v as above. Therefore

M =βη [[M]]v =βη [[N]]v =βη N.

◦

(39)

Finite completeness

Theorem (R. Statman):

For every M there is k such that, for all N:

M =βη N i M(k) |= M = N.

Corollary:

Terms are βη-equal i they are equal in all nite models.

◦

(40)

Finite completeness proof

It suces to prove that

for every closed M : treethere is k such that, for all N : tree:

M =βη N i M(k) |= M = N.

Indeed, for closed M : τ, consider Φ(M),

where Φ is a reduction of τ to tree.

For non-closed terms, consider appropriate lambda-closures.

◦

(41)

Letp(m)(n) = 2^m(2n + 1). Then p ∈ D_0→0→0 in M(N).

Observe that p(m)(n) > m, n, for all m, n.

Term zamkni¦ty typu tree, to w istocie drzewo.

Warto±¢[[M]](p)(0) mo»na uwa»a¢ za numer tego drzewa.

wiczenie: Jaka liczba jest numerem drzewa λpx. px(p(pxx)x)?

◦

(42)

Warto±¢[[M]](p)(0) mo»na uwa»a¢ za numer tego drzewa.

◦

(43)

Warto±¢[[M]](p)(0)mo»na uwa»a¢ za numer tego drzewa.

◦

(44)

For M : tree, dene k = 2 + [[M]](p)(0), i.e. 2 + numer(M).

Letp⁰ :k → k → k be p truncated to values less than k. Then p⁰ ∈D_0→0→0 in M(k).

SupposeM(k) |= M = N. Then in the model M(k):

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at most k − 2. (Otherwise the rhs equals k − 1.)

Therefore [[M]](p)(0) = [[N]](p)(0) holds also in M(N). It follows that M =βη N.

◦

(45)

Letp⁰ :k → k → k be p truncated to values less than k.

Then p⁰ ∈D_0→0→0 in M(k).

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at most k − 2. (Otherwise the rhs equals k − 1.)

◦

(46)

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*)

But all numbers needed to verify (*) are at most k − 2. (Otherwise the rhs equals k − 1.)

◦

(47)

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at most k − 2.

(Otherwise the rhs equals k − 1.)

◦

(48)

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at most k − 2.

(Otherwise the rhs equals k − 1.)

Therefore [[M]](p)(0) = [[N]](p)(0) holds also in M(N).

It follows that M =βη N.

(49)

Equality is not denable in simple types

There is no E : ωτ → ω_σ → ω_ρ, such that for all p, q ∈ N:

E p^ω^τq^ω^σ =_βη 0^ω^ρ i p = q.

Proof:

By Statman's thm., take k such that for all N : ωρ: M(k) |= 0^ω^ρ =N i 0^ω^ρ =_βη N.

There are p 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k). So in M(k): [[Ep^ω^τq^ω^σ]] = [[E]][[p^ω^τ]][[q^ω^σ]] = [[E]][[q^ω^τ]][[q^ω^σ]] =

[[Eq^ω^τq^ω^σ]] = [[0^ω^ρ]] Thus M(k) |= Ep^ω^τq^ω^σ =0^ω^ρ, whence p = q.

◦

(50)

Equality is not denable in simple types

Proof:

There are p 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k). So in M(k): [[Ep^ω^τq^ω^σ]] = [[E]][[p^ω^τ]][[q^ω^σ]] = [[E]][[q^ω^τ]][[q^ω^σ]] =

◦

(51)

Equality is not denable in simple types

Proof:

There are p 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k).

So in M(k): [[Ep^ω^τq^ω^σ]] = [[E]][[p^ω^τ]][[q^ω^σ]] = [[E]][[q^ω^τ]][[q^ω^σ]] =

◦

(52)

Equality is not denable in simple types

Proof:

There are p 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k). So in M(k):

[[Ep^ω^τq^ω^σ]] = [[E]][[p^ω^τ]][[q^ω^σ]] = [[E]][[q^ω^τ]][[q^ω^σ]] =

[[Eq^ω^τq^ω^σ]] = [[0^ω^ρ]]

Thus M(k) |= Ep^ω^τq^ω^σ =0^ω^ρ, whence p = q.

(53)

Plotkin's problem

Given d ∈ Dτ in a nite model M(X ).

Is there a term M : τ with [[M]] = d?

More generally:

Let v(x₁) = e₁ ∈Dσ₁, . . . ,v(x_n) =e_n ∈Dσ_n. Is there M such that [[M]]v =d?

(Is d denable from e₁, . . . ,e_n?)

Fact: These decision problems are reducible to each other.

◦

(54)

Undecidablility of lambda-denability

Theorem (Ralph Loader, 1993):

Plotkin's problem is undecidable.

Proof:

Reduction from the undecidable word problem for Semi-Thue systems.

Semi-Thue system: a nite set of rules C ⇒ D, where C, D ⊆ {a, b}^∗. Induces rewritingxCy → xDy, for any x, y. Word problem: Can a word w be rewritten to v in a nite number of steps?

◦

(55)

Undecidablility of lambda-denability

Theorem (Ralph Loader, 1993):

Proof:

Semi-Thue system: a nite set of rules C ⇒ D, where C, D ⊆ {a, b}^∗. Induces rewritingxCy → xDy, for any x, y. Word problem: Can a word w be rewritten to v in a nite number of steps?

◦

(56)

Undecidablility of lambda-denability

Theorem (Ralph Loader, 1993):

Proof:

Semi-Thue system: a nite set of rules C ⇒ D, where C, D ⊆ {a, b}^∗. Induces rewritingxCy → xDy, for any x, y.

Word problem: Can a word w be rewritten to v in a nite number of steps?

(57)

Undecidablility of lambda-denability

Theorem (Ralph Loader, 1993):

Proof:

Kodujemy sªowa w i v i reguªy systemu jako elementy modelu Pytamy, czy v jest deniowalne z w i reguª.

◦

(58)

Proof

TakeX = {a, b, L, R, ∗, 1, 0}. Encode any word w = o1. . .on

as a functionw : D₀ⁿ→D0, such that

I w(∗ · · · ∗ oi ∗ · · · ∗) =1, if the i-th symbol in w is oi;

I w(∗ · · · ∗ LR ∗ · · · ∗) = 1;

I w(. . .) = 0, otherwise.

◦

(59)

How does it work?

Forw = w1Cw2 we have w = λλ~xλλ~yλλ~z. w(~x)(~y)(~z).

Fix ~x,~z and consider the function g = λλ~y. w(~x)(~y)(~z). It accepts the following strings (depending on ~x,~z):

~x ~y ~z

∗ · · · ∗oi ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ same as C ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗oi∗ · · · ∗

∗ · · · ∗LR ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗L R ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗L R ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗LR ∗ · · · ∗

◦

(60)

How does it work?

Forw = w1Cw2 we have w = λλ~xλλ~yλλ~z. w(~x)(~y)(~z).

Fix ~x,~z and consider the function g = λλ~y. w(~x)(~y)(~z).

It accepts the following strings (depending on ~x,~z):

~x ~y ~z

∗ · · · ∗o_i ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ same as C ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗oi ∗ · · · ∗

∗ · · · ∗LR ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗L R ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗L R ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗LR ∗ · · · ∗

(61)

How does it work?

Depending on ~x,~z, the function g is as follows:

~x g ~z

∗ · · · ∗oi ∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗

∗ · · · ∗ C ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗oi ∗ · · · ∗

∗ · · · ∗LR ∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗

∗ · · · ∗L χ{R∗···∗} ∗ · · · ∗

∗ · · · ∗ χ{∗···∗L} R ∗ · · · ∗

∗ · · · ∗ χ{∗···∗} ∗ · · · ∗LR ∗ · · · ∗ Otherwiseg = χ∅.

◦

(62)

How to encode a rule F = (C ⇒ D)?

What will change in this table if we replace w₁Cw₂ by w₁Dw₂?

~x g ~z

∗ · · · ∗oi ∗ · · · ∗ χ{∗···∗} ∗ · · · ∗

∗ · · · ∗ C ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗oi ∗ · · · ∗

∗ · · · ∗LR ∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗

∗ · · · ∗L χ_{_{R∗···∗}} ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}_L} R ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗LR ∗ · · · ∗

otherwise χ_∅ otherwise

◦

(63)

How to encode a rule F = (C ⇒ D)?

What will change in this table if we replace w₁Cw₂ by w₁Dw₂?

~x g ~z

∗ · · · ∗oi ∗ · · · ∗ χ{∗···∗} ∗ · · · ∗

∗ · · · ∗ C ∗ · · · ∗

∗ · · · ∗ χ{∗···∗} ∗ · · · ∗oi ∗ · · · ∗

∗ · · · ∗LR ∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗

∗ · · · ∗L χ_{_{R∗···∗}} ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}_L} R ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗LR ∗ · · · ∗

otherwise χ_∅ otherwise

◦

(64)

How to encode a rule F = (C ⇒ D)

Every ruleF = (C ⇒ D) is encoded as a function F : (D₀^m →D₀) → (D₀ⁿ →D₀),

where m = |C| and n = |D|. We take:

I F (χ^{{∗···∗}}) = χ{∗···∗};

I F (χ{R∗···∗}) = χ{R∗···∗};

I F (χ{∗···∗L}) = χ{∗···∗L};

I F (C) = D;

I F (g) = χ∅, for any other g.

(65)

Claim

A word w can be rewritten to v i the element v of M(X ) is denable fromw and the functions F encoding the rules.

The easy part: Letw = w1Cw2 rewrites tov = w1Dw2

usingF = (C ⇒ D). Assume that term W denes w. Then v is denable by

V = λ~x~u~z, F (λ~y. W~x~y~z)~u, (*) It follows that codes of reachable words are denable.

The hard part: And conversely.

◦

(66)

Claim

usingF = (C ⇒ D). Assume that term W denes w.

Then v is denable by

◦

(67)

Claim

usingF = (C ⇒ D). Assume that term W denes w.

Then v is denable by

◦

Typy proste

Typy proste

Simple types

Church style syntax (orthodox)

Church and Curry

Church style:

Curry style:

Non-orthodox Church

Fact:

Relating systems

Properties

Denable functions

Examples

Examples

Examples

Extended polynomials (wielomiany warunkowe)

Denable functions

Theorem (H. Schwichtenberg'76):

More denable functions

Examples:

More denable functions

Examples:

More denable functions

Examples:

Equality

Theorem (R. Statman'79):

Exercise:

Equality

Theorem (R. Statman'79):

Exercise:

The inhabitation problem

Inhabitation problem:

Fact (R. Statman):

The inhabitation problem

Inhabitation problem:

Fact (R. Statman):

Representing data types

Representing data types

Representing data types

Representing data types

Representing data types

Representing data types

Representing data types

Type reducibility

Theorem (R. Statman):

Type reducibility

Theorem (R. Statman):

Semantics for nite types

Standard model M(A)

Completeness

Theorem (Harvey Friedman):

Proof:

Completeness

Theorem (Harvey Friedman):

Proof:

Completeness proof

Completeness proof

Partial epimorphism: f e =

f (e)

Completeness proof

Main Proof:

Completeness proof

Main Proof:

Finite completeness

Theorem (R. Statman):

Corollary:

Finite completeness proof

Equality is not denable in simple types

Proof:

Equality is not denable in simple types

Proof:

Equality is not denable in simple types

Proof:

Equality is not denable in simple types

Proof:

Plotkin's problem

Undecidablility of lambda-denability

Theorem (Ralph Loader, 1993):

Proof:

Undecidablility of lambda-denability

Denable functions

Denable functions

More denable functions

More denable functions

More denable functions

Semantics for nite types

Partial epimorphism: f e =

Equality is not denable in simple types

Equality is not denable in simple types

Equality is not denable in simple types

Equality is not denable in simple types

Undecidablility of lambda-denability

Undecidablility of lambda-denability

Undecidablility of lambda-denability

Undecidablility of lambda-denability