Timeline for cut elimination
Current License: CC BY-SA 2.5
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 14, 2009 at 21:58 | comment | added | Dan Piponi | It's not just in proof search. In a functional programming language, the very process of executing a program is the same thing as repeated cut elimination. Suppose we're evaluating f(x) and we have a definition f(x) = RHS. Whenever we use f(x) in our code it can be replaced by RHS using an appropriate substitution. We can execute programs by repeatedly expanding definitions until eventually all of the function calls have been eliminated and we're left with a final value. This is formally identical to cut elimination (modulo lots of details). | |
| Dec 12, 2009 at 15:44 | history | answered | Alexey Romanov | CC BY-SA 2.5 |