User dfranke - MathOverflow

Answer by dfranke for Generalizing a problem to make it easier

2010-09-28T17:58:26Z

Bruce Schneier has an online paper called "A Self-Study Course in Block-Cipher Cryptanalysis": http://www.schneier.com/paper-self-study.pdf containing an extensive list of algorithms to cryptanalyze as exercises. By far the easiest exercise is this one:

[Cryptanalyze] a generic cipher that is “closed” (i.e., encrypting with key A and then key B is the same as encrypting with key C, for all keys).

The solution to this exercise would be a lot less obvious had Schneier instead pointed to some particular block cipher that has this property. But because the reader is told nothing about the cipher except that it is closed, he immediately knows exactly what to attack.

Answer by dfranke for Number of ways to construct mathematical objects

2010-09-23T18:58:55Z

How about models of computation?

Turing machines
Register machines
Cellular automata
$\mu$-recursive functions
The untyped $\lambda$-calculus
Unrestricted grammars
Term-rewriting systems
Recursively-enumerable subsets of $\mathbb{N}$
$\ldots$

To this list we can add finite presentations of semigroups and groups, diophantine sets, and many other mathematical structures that realize universal computation.

Answer by dfranke for Is there a general setting for self-reference?

2010-09-22T15:50:32Z

Perhaps the right question to ask is if the statement is expressible in any system whose proof-theoretic ordinal is smaller than the Feferman–Schütte ordinal.

Answer by dfranke for Jokes in the sense of Littlewood: examples?

2010-09-16T00:44:54Z

Hausdorff dimension. Try showing a Sierpinski triangle to a non-mathematician and explaining that it is a 1.585-dimensional object.

Interesting complexity classes $PR \subsetneq c \subsetneq R$

2010-08-13T09:48:27Z

I'm working on a proof-checker that can verify termination proofs. The fundamental method it provides for constructing such proofs is to translate the program into primitive recursion. Basically, I provide a combinator $\rho$ typed as:

$\rho: \forall A,B:(A\rightarrow Nat \rightarrow A)\rightarrow (A \rightarrow B)\rightarrow A\rightarrow Nat \rightarrow B$

which, in the notation defined here, constructs $h$ given $f$ and $g$.

Although the term language contains a fixed-point combinator and is therefore Turing-complete, terms that use it have a "tentative" flag in their type that indicate this. The $\rho$ combinator and the fixed-point combinator are the only two language primitives that allow for recursion or looping of any sort (i.e., without either of these two combinators, all you've got is a finite-state machine). Therefore, all terms that are well-typed and non-tentatively typed are primitive recursive.

What I'm wondering is if there are any interesting complexity classes that you can build by starting with primitive-recursive constructions, and adding a finite number of other functions $Nat \rightarrow Nat$, each of which is in R but not in PR, and allowing composition with these functions. It's easy to come up with non-interesting examples of such classes, e.g. "primitive recursion plus the Ackermann function", but I'm looking for any that have sufficiently interesting properties that it would be worth adding the functions which characterize them as admitted axioms in the proof system.

Comment by dfranke

2010-09-22T16:18:44Z

I think that before I can make a more rigorous proposal about what a self-referential statement is, we first need to set boundaries on what qualifies as a statement. If we need to take into account such sentences as "colorless green ideas sleep furiously", then I wouldn't know where to begin.

Comment by dfranke

2010-08-15T15:33:17Z

Alright, I get it now. What I was missing before was the essentialness of encoding natural numbers as iterator functions. That's where you get the "potential energy", so to speak, in order to compute complex functions without the need for a recursion operator. Thanks again.

Comment by dfranke

2010-08-13T14:35:10Z

Nifty. So the answer is that I don't even need $\rho$ as an axiom: the underlying system is already expressive enough to construct it and much more beyond it, and I need to finish wrapping my brain around the properties of that system.

Comment by dfranke

2010-08-13T14:03:13Z

No problem. Done.

Comment by dfranke

2010-08-13T12:53:19Z

So, to rephrase my question without having to go into the gory details of the type calculus: can you get any interesting complexity classes by starting with a system that permits only primitive-recursive constructions, and augmenting it with certain $Nat \rightarrow Nat$ total functions that are not in PR.

Comment by dfranke

2010-08-13T12:50:00Z

...right, which is what I get for trying to ask coherent math questions at 5:30 AM. The system I'm working in is one based on Luo's Extended Calculus of Constructions. It contains a fixed-point combinator in addition to the above $\rho$ combinator and therefore is Turing-complete, but expressions that invoke it have their types flagged to indicate that they do. But, every well-typed term that is not so-flagged is in PR, because $\rho$ is the only other combinator that provides recursion.