Timeline for Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 15, 2014 at 20:19 | vote | accept | Jake | ||
| Jan 15, 2014 at 20:19 | comment | added | Jake | Neel: perfect! that answers my question! Foetus allows the same set of commutable functions! Thanks! That is exactly what I wanted to know. Also that large elimination expands the set of functions which may be of further use. Thanks! | |
| Jan 15, 2014 at 18:10 | comment | added | cody | I'm still not convinced large elimination is the culprit here: Term is secretly of type $\mathrm{Set}_1$ rather than $\mathrm{Set}_0$, and I think this is what you are really using. | |
| Jan 15, 2014 at 9:55 | comment | added | Neel Krishnaswami | Agda's documentation says its termination checker uses the Foetus algorithm. If you took T, and extended it with pattern matching and recursive definitions checked by Foetus, you would not be able to write an interpreter for T in it. In fact, you would not change the functions computable by T at all -- all of the termination orders Foetus computes are provably well-founded in Peano arithmetic. (See cody's answer.) The Foetus algorithm lets you write more definitions, without changing the set of functions you can compute. Agda's large eliminations actually increase the set of functions. | |
| Jan 14, 2014 at 23:51 | comment | added | Jake | This shows that Agda is more general sense it can write an interpreter for system T but does it does not show weather or not Foetus, a language which is not dependently typed, is more general. Can Foetus do this? Would Agda still be able to do this if not for "large elimination"? | |
| Jan 14, 2014 at 22:01 | comment | added | cody | I'm sorry: yes the interp-T function does indeed use large elimination. I also agree that proving 0 != 1 does indeed require it. However, defining computable functions is not the same thing as proving mathematical statements. My answer clarifies this a bit. The pure Calculus of Constructions, for example, cannot prove 0 != 1. It can, however, define the Ackermann function with relative ease. | |
| Jan 14, 2014 at 20:37 | comment | added | Neel Krishnaswami | @cody: The interp-T function computes a set from a term, which looks like a large elimination to me! It is definitely the case that large eliminations add power: Martin-Loef type theory can't even derive inconsistency from 0=1 without a large elimination. (To see this, note that without universes/large eliminations you can erase all dependencies and get a simply typed term: this is what Harper and Pfenning did in their adequacy proof for LF.) | |
| Jan 14, 2014 at 16:46 | comment | added | cody | Note that you haven't used large elimination in your example. Large elimination doesn't actually add computational power. Impredicativity does: system F doesn't have the former, but can express functions not expressible in system T. | |
| Jan 14, 2014 at 10:54 | history | answered | Neel Krishnaswami | CC BY-SA 3.0 |