Timeline for What is the definition of computational content?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 24, 2016 at 20:09 | comment | added | user44143 | I have clarified that I was explaining what the phrase means in the titles. For any particular theorem, the computational content is an algorithm (e.g. from reals to reals) rather than the extractive process (from proofs to such algorithms). And when a constructive mathematician talks about the constructive content of a particular theorem, they may mean a particular algorithm. But when type-theorists and proof-theorists talk about computational content, they are usually interested in an extractive process and how it applies to a variety of theorems. | |
| Oct 24, 2016 at 19:55 | history | edited | user44143 | CC BY-SA 3.0 |
deleted 2 characters in body
|
| Oct 24, 2016 at 14:33 | comment | added | user2377 | Perhaps my "intuitive understanding" is incorrect. You are saying that "computational content" means the extraction of an algorithm, not the algorithm that is extracted? | |
| Oct 24, 2016 at 0:54 | history | edited | user44143 | CC BY-SA 3.0 |
added 630 characters in body
|
| Oct 23, 2016 at 21:40 | history | answered | user44143 | CC BY-SA 3.0 |