Zero-Knowledge Proof of honest function execution - Is this possible? Assume Alice and Bob share a well-known function $f(x)$. Bob asserts that he has a $y$ such that $f(y) = true$. Bob's $y$ is secret, but he is willing to share a hash of it. Alice wants to purchase $y$ from Bob, but only if she can be assured that $f(y) = true$ before the purchase happens.

I've studied Zero-Knowledge Proofs, but the examples I've seen seem to be focused on proving knowledge of a value without revealing the value itself. This seems different... Alice must somehow know that Bob executed $f(y) = true$ truthfully, without altering $f(x)$ or substituting a different value for $y$. Is this possible without a trusted third party?
I am not totally clear on what the procedure for actually "buying" something in your protocol should be, but I'd point out that a (totally) fair exchange between Alice and Bob is impossible.
This follows from the fact that no 2 party secure computation protocol can achieve fairness (impossibility result). In a nutshell: When Alice and Bob run a protocol to exchange some secrets, then one party can always abort as soon as it gets its result without letting the other party know their secret.
As pointed out by Yehuda Lindell in the comments this is not true for all functionalities, see link in the comments.

Lets focus on how Bob can convince Alice that he has some secret $x$ that fulfills some predicate $f$. 

In the case of arbitrary predicates $f$, like "I know a pre-image to a specific SHA-1 output", you can use something called zero knowledge using garbled circuits. This approach first appeared in the following paper: zero knowledge using garbled circuits.
The high level idea is to use so called garbled circuits that are, in general, used for secure two party computation (which your problems is a special case of).
For your setting, Alice is the verifier and Bob the prover.
The protocol proceeds as follows:


Alice garbles a circuit representing the prediate $f$ and sends this circuit to Bob (note Alice has no input to that circuit).
Bob uses oblivious transfer to retrieve the wire input labels to the circuit that correspond to his input $x$.
Bob evaluates the circuit and commits to his output wire(s)
Alice "opens" the garbled circuit she sent in step 1 to convince Bob that she did not cheat by garbling some malicious circuit
Once Bob is convinced everything was Ok, he opens his commitment.


On a high level Bob cannot cheat because the only thing he is doing is retrieving some input wire labels, and running them through the circuit.

This may sound like a terribly slow approach, but it is actually not that bad and it strongly depends on what you want to do with it. 

Garbled circuits, where only one party has an input are more efficient then the general garbled circuits (see Two halves make a whole in the "privacy-free garbling" section).

Another fairly efficient protocol was recently proposed ZKBoo. This protocol also does something similar to using garbled circuits. However, they focus on reducing the computational costs, but slightly increase the bandwidth overhead, which is already the bottleneck in all garbled circuit approaches.

For less general predicates there may be more direct and more efficient solutions.

Update/Answer to comment:

Whether garbled circuits are practical for "complex" predicates very much depends on how well you can represent them as a computation of a boolean circuit. As a rule of thumb, if you have lots of array accesses, e.g. binary search, then circuits are probably not your best option. There are protocols for general secure ram computation (that's where you have array accesses) and even tailored protocols for zero knowledge proofs using secure ram computation (see Efficient Zero-Knowledge Proofs of Non-Algebraic Statements with
Sublinear Amortized Cost). I don't know how efficient this would actually be in practice, but if you want to play around with this, then you should maybe check out the obliv-c library (https://github.com/samee/obliv-c). Even though their protols are not specifically tailored to the zero knowledge setting, it's easy to use and I think the implementation of their oram extension described in the following recent paper Revisiting Square-Root ORAM is also available on their github page.

Regarding your concrete example of a spell checker you should look at a concrete algorithm and then just take the stuff I wrote above into account.