A question for anyone who quit their career as a patent lawyer to work on formal methods (or vice versa):
Since mathematics isn't patentable, can you invalidate a patent claim by showing that it is equivalent to a mathematical formula? And if so, by the Church-Turing thesis, wouldn't any Turing-complete program be representable in lambda calculus, and therefore be unpatentable?
True, you can not patent a mathematical formula but you can patent a machine that uses a mathematical formula to do something and the machine can be a computer.
A more concrete example:
You discover that the formula for making a beam that will have equal stress all along it's length is t = (.923)Xe/L^2 (made-up formula)
You can not patent that formula, but you can get a patent on beams made using that formula. With that patent in hand you can stop anyone from making, selling, or using those beams.
Sounds like a distinction without a difference. If you can stop people from using a formula with your patent, you've effectively patented that formula.
If you read the independent claims, they have not patented the formula by itself.
Claim 1: A system for determining if two operands point to different locations in memory, the ...
Claim 15: A method for producing executable code for performing ...
Claim 21: A computer-readable medium comprising computer-executable instructions for ...
Dependent claims by definition include at least one of the above.
Since mathematics isn't patentable, can you invalidate a patent claim by showing that it is equivalent to a mathematical formula? And if so, by the Church-Turing thesis, wouldn't any Turing-complete program be representable in lambda calculus, and therefore be unpatentable?