Home » forums » LtU Forum

Weird computability problem relating to state + lambda calculus

Hi all,
I have a weird question that I've been trying to solve.

I've been reading about lambda calculus, specifically the different augmentations of lambda calculus. The ones that most interest me are the ones with some sort of state, like a store (mu). So my question is:

Given a term, t, in the (untyped) lambda calculus (or in a typed calculus which features full abstraction), is it decidable whether or not it ever modifies the state (updates some value in the store, etc).

My gut says that it's not decidable for all terms, but I want to PROVE it.

-Kevin

By ellisk at 2009-01-16 22:12 | LtU Forum | previous forum topic | next forum topic | other blogs | 5633 reads

Comment viewing options

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

Doesn't this reduce to the

Doesn't the halting problem reduce to this? Given a pure term T that you want to know if it normalizes, build a new term T' that tries to evaluate T and then hits the store.

By Matt M at Fri, 2009-01-16 22:37 | login or register to post comments

Undecidable...

It's undecidable.

Consider a problem where one assigns to a state the result of an application from a subset of this language that is 'pure' untyped lambda calculus. Since the halting problem is undecidable for the 'pure' untyped lambda calculus expression, it is undecidable (in general) whether that expression will ever result in a value being stored to the state.

Anyhow, you shouldn't bring your homework here. x_X

By dmbarbour at Fri, 2009-01-16 23:05 | login or register to post comments

This isn't my homework. I'm

This isn't my homework. I'm just a nerd, and these things interest me.

EDIT: Actually, in a way, it is. This is related to a project I'm working on which my computer science teach agreed to give me school credit for. However, this problem wasn't "assigned" or anything like that, it just came up in the process of working on the project.

By ellisk at Sat, 2009-01-17 04:55 | login or register to post comments

See Rice's Theorem

See Rice's Theorem.

By James Iry at Sat, 2009-01-17 01:20 | login or register to post comments

Conservatively decidable

Effect types provide a way to approximate what you are after. These are implemented in several languages. Effect types can tell you whether a term is (structurally) pure, but the analysis is conservative: if any evaluation of that term might perform a store, effect types will conclude that it is impure.

Higher order terms are not always evaluable by themselves, and this affects the outcome. The [im]purity of MAP, for example, is a consequence of the [im]purity of the mapped function.

By shap at Sat, 2009-01-17 14:17 | login or register to post comments