Home » forums » LtU Forum

Other free theorems

Given,

f : ∀a:*. a → a → a

we can take a = {x,y} to show that for a particular x,y, either:

f x y = x, or 
f x y = y

My question is how to formally reason that f is uniformly defined by one of those equations. What property of f is needed? Informally, it's easy to reason that there is nothing f could branch on, but I don't see how to generalize.

Thanks

By Matt M at 2011-10-22 19:51 | LtU Forum | previous forum topic | next forum topic | other blogs | 5798 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Partial application

For me it's easier to look at what happens if you look at the type as a -> (a -> a) instead.

Then f x has to equal either id or const x. (or diverge)

By Douglas McClean at Sat, 2011-10-22 20:10 | login or register to post comments

Parametricity or normalization

The popular article on how to get results out of parametricity is Wadler's Theorems for free!.

Such reasoning are generally formalized as properties of the whole system, rather than properties of a function f. The idea is to define a logical relation indexed by types : for a type T, you have a relation between elements of type T that, intuitively, represents semantic equality at that type. Then you can prove, if your system has good properties, that all well-typed elements are related to themselves; this gives you a general reasoning principle on all well-typed terms.

I suppose that you can turn this reasoning as depending on properties the function f : instead of saying "in a system where well-typed terms are semantically equal to themselves, ...", you say "if f is semantically equal to itself, ...".

What you would get by the usual definition of equivalence in a type system with arrows and universal quantification is : for all relations R between two types A and A', if x R x' and y R y', then (f [A] x y) R (f [A'] x' y'). I suppose if you take A and A' equal and R to be of the form { (x,x), (y,y) }, you get the property you're looking for.

The other way to prove those things is to use normalization on the language, either assuming a termination/consistency result on the whole system, or assuming that f is (and all its partial applications) are normalizing. The reasoning is then dependent on the structure of the normal forms of your language. It would go as the following. For A a type and x,y in A, what is the normal form of f [A] x y ? Well, you are in a context A type, x:A, y:A, and get a result of type A; if your language is consistent and well-behaved, you usually get that the normal form is either x or y.

This is not necessarily true; for example, if your language has a fail construct of type ∀α.α, then you won't be able to show consistency, and fail[A] could also be the result of f. I expect you also have an equivalent of this with the parametricity argument: functions that use fail won't be semantically equal to themselves.

By gasche at Sun, 2011-10-23 12:26 | login or register to post comments

Parametricity

Rephrasing what you've said, parametricity gives that ∀φ. φ(f x y) = f (φx) (φy), viewing a relation φ as a multi-valued function. Choosing the φ you suggest (φ x = {x}, φ y = {y}, and φ _ = {}), seems to just show that (f x y ∈ {x,y}) for each x and y, not that f is defined at all inputs by one of two equations. And as I noted, that can be obtained by just instantiating a with {x,y}.

I don't think a noramlization based argument will work for me, but that aside, I think the argument you've sketched will have a similar problem. Compare to:

g : ∀a. Bool → a → a → a

Any such function g will ultimately have to choose between its two a-typed parameters, just like f, but there are four possibilities for g.

By Matt M at Sun, 2011-10-23 16:25 | login or register to post comments

Choose R first

You're right about parametricity.
It seems there is some amount of purity involved. If you have a random x y construct in your language, then the admissible behaviors for ∀α.α→α→α change, yet this doesn't endanger parametricity of the type system. So parametricity isn't going to help here.

Note that normalization gives the uniformity you're looking for : a normal form for f is is of the form Λα.λx₀.λy₀.t with t normal form in the context α,x₀:α,y₀:α, so is either x₀ or y₀ : ∀α.α→α→α admits only two elements upto βη-equivalence.

By gasche at Sun, 2011-10-23 16:57 | login or register to post comments

Normalization

You're right. I misunderstood the argument you had in mind, but I agree that a normalization argument would work. Still, it's not clear to me how to formally reason about situations like this in general. I was hoping someone would provide a link to a formal system that does this kind of reasoning out of the box :). Not that your suggestion of normalization wasn't helpful. It was, thank you!

By Matt M at Sun, 2011-10-23 17:36 | login or register to post comments

Parametricity after all?

I was thinking about this again yesterday and I think this does actually follow from parametricity. We just need to look at a different relation.

For any x:a, y:a we know that either (f x y = x) or (f x y = y), by one of the arguments above. Suppose x != y and consider the first case (f x y = x). Choose ~ to partition two equivalence classes: the class equal to x and the class not equal to x. i.e. (w~z = (w==x) == (z==x)). Then by parametricity, if y' ~ y, or equivalently y' != x, then (f x y' ~ f x y), or equivalently (f x y' = x). In the other case, y' = x, then instantiating the type at singleton(x) gives that (f x y' = x) still holds.

Thus if (f:a->a->a) and (f x y = x) at some particular x,y, then (f x y = x) uniformly for all y. So this would seem to imply that 'random' isn't parametric.

By Matt M at Tue, 2012-10-02 14:16 | login or register to post comments

Simpler with asymmetry

Choose w~z = (w==x) >= (z==x), where true > false.

Then, for y' ~ y, meaning any y', since y!=x, we have f x y' ~ f x y, which means f x y' = x, since f x y = x. This also generalizes more easily (e.g. to f: a->a->a->a).

By Matt M at Tue, 2012-10-02 16:42 | login or register to post comments

Parametricity in the presence of fail or fixpoint

Section 7 of Theorems for Free treat fixpoints. The fail operator you discussed is similar, since fail and (fix id) are similar. In both cases, the solution is to use a different (and weaker) logical relation.

So your statement 'functions that fail won't be semantically equal to themselves' is misleading. The correct solution is to adopt a different notion of semantic equality. (The Clinton Principle: It depends on what the meaning of the word 'is' is.)

By Philip Wadler at Wed, 2012-10-03 14:33 | login or register to post comments

Update

It occurs to me that in many models (in particular the one I'm interested in), there are more than two functions satisfying that type signature. In addition to choosing which parameter to return, we can choose whether to be strict in the other parameter.

If I want to be able to reason by cases, I think I need to work with a type like this:

type Left = ∀a:*. a → Any → a
type Right = ∀a:*. Any → a → a
f : Left ∪ Right

The normalization argument avoids this issue by assuming that all values come from lambda terms in a calculus with a particular evaluation order. Thanks for the help, gasche.

By Matt M at Sun, 2011-10-23 16:22 | login or register to post comments

Another view

I don't understand gashe's, or your, posts. But I don't really see another manner of proving it except for induction over the term language (of LC).

I.e., the property is "A term of type 'a' constructed within a context of two variables 'x' and 'y' of type 'a' must return 'x' or 'y'".

I imagine that the base case is that you only have two variables to choose from (x or y), and you'll need to do some elaborate inductive reasoning on (E E) and (lambda v. E) to inductively derive that they also have no other choice of returning 'x' or 'y'.

(I rewrote the property. It still isn't correct, but it's something like that. You get the gist.)

By marco at Tue, 2012-10-02 23:15 | login or register to post comments

I agree

This could work. I don't know how well it would generalize to other cases. For example, a useful case is proving that any term of type (forall a. (s -> a) -> (t -> a) -> a) either has type (forall a b. (s -> a) -> b -> a) or (forall a b. b -> (t -> a) -> a). i.e. that a church encoded sum is either Left S or Right T.

By Matt M at Wed, 2012-10-03 01:34 | login or register to post comments

Interesting

I wouldn't know whether this particular property holds. You could use techniques from the Wadler paper; I don't really understand the paper. But, after glancing at that, I have the feeling that the property is stated very informally, and that the the hard part --the heart-- of the proof, which is the (inductive) proof over an object logic, is swept under the carpet. (Though, informally, the hard part holds trivially, I don't think the proof is trivial.)

Though I guess a better answer is that if you know that a function, given its type, can only decompose into two functions, then all functions must implement either one of those semantically equivalent functions, is the way to go.

(You could go further than that, and formalize some algebra over manners in which you can compose functions and semantical equivalences between specifically typed functions regarding an object logic/typed LC/or something. You could even try to generalize that with respect to object logics which satisfy specific properties.)

By marco at Fri, 2012-10-05 12:00 | login or register to post comments

Normalization

I have described this technique at the end of my original post, "The other way to prove these things...". It depends on a result of normalization of language (or at least the particular value you're studying), because otherwise you could have divergent terms (eg. `let rec z = z in z` or `raise Exit`) with the correct types that return neither 'x' nor 'y'.

Defining "normalization" at higher types needs a bit of work. What does it mean for a value ot type (forall a. (a -> a) -> (a -> a)) to be normalizing? Is `id := (fun f x -> f x)` normalizing at that type? Yet `id (fun x -> raise Exit)` doesn't return a result.

By gasche at Wed, 2012-10-03 06:03 | login or register to post comments

It's a property you would

It's a property you would formalize in a meta logic regarding an object logic. For the object logic you need to formalize the language, reduction rules, and typing rules, as well as derive that all well-typed terms are normalizing. I agree with the divergence but for a tad more trivial reason, probably you meant the same, "if some_infinite_computation then x else y" can't be well typed.

(I think I was mistaken. There are two views on "if some_infinite_computation then x else y". It doesn't return x or y, therefor the property doesn't hold; or it can only return x or y, therefor the property holds. It starts to depend on what exact property you're proving.)

By marco at Wed, 2012-10-03 12:40 | login or register to post comments