On 01/06/2012 11:48 AM, Invisible wrote:

> It takes many, many steps, but it does eventually produce f(fx) as
> result #7. (And several more times after that, as it explores every
> possible reduction sequence. The number of these is presumably
> exponential in the size of the input...)

Not so much the /size/ of the input, but the number of redexes 
("reducible expressions") it contains.

At every point, the solver chooses a redex by some algorithm, and then 
reduces it. Overall, the solver makes all possible choices, and 
generates [at least] one result per choice. So clearly the number of 
redexes put a lower bound on the number of solutions.

Reducing a K-redex or an I-redex results in one fewer redexes. However, 
reducing an S-redex can duplicate an existing redex into /two/ new 
redexes. (Or it can leave the number of redexes unchanged. It depends on 
the exact expression.)

I would hazard a guess, therefore, that the number of possible reduction 
orders is a non-computable function of the input expression.

Look at it this way: It appears that the only way to compute the number 
of reduction orders is to actually /find/ all possible reduction orders. 
In other words, to execute the program and count how many ways you can 
do it. If the program is non-terminating, then the counting procedure is 
also non-terminating. So it appears that counting the number of 
reduction orders is trivially equivalent to the Halting Problem.

(This relies on the assumption that running the program is the /only/ 
way to compute the number of reduction orders...)

Post a reply to this message