vladsotirov

A simpler explanation of the technique in the article that I believe matches the C standard more closely is the following.

Ideally the result of processing a macro ("macro-replacement") would contain no further macros. But in order to disallow infinite loops during processing of a macro, the C standard specifies that names of macros that would be processed recursively are instead painted blue ("marked") so as to never be processed.

The technique in the article hinges on the fact that macro-replacement, as specified in the C standard, allows not only for the result of macro-replacement to contain these marked do-not-process macros, but also unmarked unprocessed macros. Specifically, such an unmarked unprocessed macro is a functional macro arising after processing a macro with an empty definition that separates the functional macro's name from its arguments.

The technique for achieving recrusive macros is to introduce a functional macro whose definition is the would-be recursive macro, and to replace each occurence of the name of the would-be recursive macro in its own defintion with the functional macro interrupted by an macro with an empty definition.

The result is an unmarked unprocessed recursive macro. Processing such a recursive macro, e.g. by including it as an argument to a macro, corresponds to taking one step of the recursion. Thus any pre-determined finite number of steps of a recurisvely defined macro can be performed.

For example, the would-be recursive macro of the article

#define _COUNT_ONE(x, ...) + 1 _COUNT_TOP(__VA_ARGS__)

#define _COUNT_TOP(...) __VA_OPT__(_COUNT_ONE(__VA_ARGS__))

#define COUNT(...) (_COUNT_TOP(__VA_ARGS__) + 0)

becomes

#define EMPTY

#define _COUNT_INDIRECT() _COUNT_ONE

#define _COUNT_ONE(x, ...) + 1 _COUNT_TOP(__VA_ARGS__)

#define _COUNT_TOP(...) __VA_OPT__(_COUNT_INDIRECT EMPTY()(__VA_ARGS__))

#define COUNT(...) (_COUNT_TOP(__VA_ARGS__) + 0)

To process the COUNT(...) macro 5 times, allowing it to count up to 5 variable arguments, nest it 5 levels deep as an argument to a macro.

#define EVAL1(...) __VA_ARGS__

#define EVAL5(...) EVAL1(EVAL1(EVAL1(EVAL1(EVAL1))))

EVAL5(COUNT(1,2,3))

The second Q needs no input because it is not executed: its source code is used as input for the first Q.

> The Halting Problem is famously only undecidable if the code you're analyzing is being modeled on a "Turing machine" or something equally "powerful" to it.

The Halting Problem applies as long as you're able to programmatically combine two programs into a program that executes one with the other as its input. Given such a facility you can write a literal program whose input is a halting analyzer and whose output is a program on which the halting analyzer does not halt. Moreover the size of the output program seems to be something like twice the size of the analyzer plus the size of the program that combines pairs of programs as above.

On computers with finite memory, this program (deriving from an analyzer a program on which the analyzer fails to halt) may itself not halt only if it runs out of memory. One conclusion is then a lower bound for the size of an analyzer as a fraction of available memory, and it seems the fraction would be close to a third.

My personal opinion is this makes it practically impossible to make an analyzer. I think this because the size measure of the analyzer relative to memory is not in bytes but in terms of information content. What I mean is that size may refer to the size of a decompossion program plus a compressed archive of the would-be analyzer (this is an equivalent analyzer of smaller size). So the analyzer program would have compressed source code on the order of a third of available memory. Even worse, if we continue making computers with more memory, we would need bigger and bigger analyzers. Moreover, these cannot be procedurally generated by some algorithm that takes as input memory size, as this would violate the unbounded computation halting problem. So we would need bespoke large analyzer algorithms. Finally, just proving the correctness of such a code base that is not generated in some principled manner (as it would then be compressible) is also something practically impossible. In conclusion, such effort would be better spent on designing Turing-incomplete domain-specific languages with guaranteed behavior for which an analyzer is unnecessary. The latter is what people actually work with.

In any case, below is the algorithm which takes as input a halting analyzer H and produces a program QQ on which the halting analyzer does not halt. It would perhaps be instructive to implement it and apply it to the cycle detection problem.

---

Let H be some halting analyzer. By that I mean a program with the property that if HP, the program executing H with input P, halts with output 0, then executing P would not halt.

Let N be a program that halts on input 0 and does not halt otherwise.

Let N(HP) be the program that executes HP, and if the latter halts, executes N with input the result of executing HP. The behavior of N(HP) is that it halts if executing P would not halt in a way H could detect, and does not halt otherwise.

Let Q be the program which takes input P and executes the program N(H(PP)). That is such that program QP, which executes Q on input P, halts if executing PP would not halt in way H can detect, and does not halt otherwise.

Consider now the behavior of the program QQ, which excecutes Q with itself as input. It halts if executing QQ would not halt in a way H could detect, which is self-contradictory. So QQ most definitely does not halt.

It follows that H(QQ) either does not halt or outputs 0. Outputting 0 is again self-contradictory, because that would mean executing N(H(QQ)) would halt, and by assumption QQ, which does not halt, is the program which executes N(H(QQ)).

In conclusion, any halting analyzer H does not halt on input QQ, that is, the program which executes Q on itself as input, where Q is the program which takes input P, generates the program PP which would execute P on itself as input, and then executes N(H(PP)).

> It does not. That only means that you if you, say, want to analyze how a program behaves when ran in a computer with 16 GB of state, you need to analyze it on a computer that has more than 16 GB of state.

Then we must differ on what the "halting problem" refers to. I would say that a computer suffers from the halting problem if there is no program it can run that can determine whether arbitrary programs it can run halt or not. You seem to agree that this is the case for a computer with a fixed amount of memory (as you say, a computer with more memory is needed to analyze all programs for such a computer).

I can then only ask what is this thing that is not the halting problem (as I understand it) that you think does not exist for computers in the real world?

> Now, I'm not a computer scientist nor a mathematician or logician. So I could be wrong. If so, I would be interested in knowing how I'm wrong, as I've never seen this issue being discussed in a thorough way.

Rice's theorem is much easier for computers with finite memory than for those with infinite memory. This is because a finite amount of memory gives a bound on the combined size of an analyzing program and the analyzed program. In particular, the only program that can analyze all programs is the empty program.

For your proposed example, a cycle detection program executed on a computer with finite memory cannot analyze all programs the computer can execute (unless it doesn't analyze them at all). Consequently, if there are both programs that halt and programs that do not, the computer cannot determine whether they have a cycle or not, i.e. halting is undecidable unless it is trivially decidable.

I'd be curious whether this suffices to convince you the halting problem exists for computers in the real world as well. If not, I'd be curious to read your objections.

> Some numbers in a set called the "smooth reals" square to 0... without being zero. This seems to create a universe in which every geometric object is "infinitesimally straight". I haven't fully grasped why this works. It's like the dual numbers, but somehow made all-pervasive.

It's not the existence of the set of "smooth reals" that square to 0 without being 0 that creates the universe in which every geometric object is infinitesimally straight.

Rather, for any ring of "smooth reals" R, the set D={d in R:^2=0} allows us to construct a "dual ring" as follows. First, take the map RxR -> R^D sending a pair (a,b) of "smooth reals" to the linear function D->R given by d|->a+bd. Then induce a ring structure on RxR that would make the map into a ring homomorphism when R^D, the set of R-valued functions on D, is given the pointwise ring structure.

Explicitly, (a_1,b_1)+(a_2,b_2)=(a_1+a_2,b_1+b_2) since (a_1+b_1d)+(a_2+b_2d)=(a_1+a_2)+(b_1+b_2)d, and (a_1,b_1)(a_2,b_2)=(a_1a_2+a_1b_2+a_2b_1) since (a_1+b_1d)(a_2+b_2d)=a_1a_2+(a_1b_2+a_2b_1)d+d^2b_1b_2 and d^2=0.

Thus, we have the structure of a ring on the set of RxR, which is tradtionally denoted by R[e] where e(psilon) is a variable x assumed to square to zero, i.e. an indeterminate, so hypothetical, order 2 infinitesimal.

Now, Axiom 1 of synthetic differential geometry asserts that the map sending the ring of dual numbers to the ring of R-valued functions on D is a bijection. In other words, it restricts the domain of discourse so that, when it comes to functions on order 2 infinitesimals, we may only ever talk linear functions, and it also expands the discourse in requiring that we have distinct linear functions, one for every pair y-intercept,slope pair.

It is the second bit that forces every geometric object to admit "infinitsimally straight" approximations, because every geometric object is essentially contained in a copy of R^n (n-tuples of "smooth real numbers"), and so it is forced to have non-trivial linear functions from D.

---

One reference for the relationship to the dual numbers is the first few pages of Anders Kock's book Synthetic Differential Geometry, available from his web-site at home.imf.au.dk/kock/sdg99.pdf. Another, more readable reference, are Mike Shulman's notes available at http://home.sandiego.edu/~shulman/papers/sdg-pizza-seminar.p....

One "application" (in quotes because honestly for all the fanfare I haven't come across something that was worked out to be usable by non-specialists) is automatic differentiation, see http://blog.sigfpe.com/2006/09/practical-synthetic-different...

Generally speaking, the ability to extended intuionistic mathematics by new axioms that are classically inconsistent is a bit of a misnomer. The real power is that these "axioms" allow you to easily and immediately specialize the generic language of intuionistic mathematics into a domain-specific language for various areas.

So that

1. adding the continuity axiom gives you a domain-specific language which can only describe continuous functions and no others

2. adding the differentiation axiom gives you a domain-specific language called synthetic differential geometry in which you can only talk about differentiable functions

3. adding the computability axiom gives you a domain-specific language in which you can only talk about computable functions.

4. adding the law of the excluded middle gives you the domain-specific language of classical mathematics.

Now, each of the first three can also be interpreted within classical mathematics (which is how we know the extensions are consistent with classical mathematics), but that's analogous to writing an interpreter in C versus merely adding new syntax to an existing language (e.g. how DSLs can be implemented in LISP).

The remarks on computable and continuous functions can also be thought about as follows.

The law of the excluded middle is only one non-constructive aspect of classical mathematics. Dropping it leaves you with what is usually called "intuionistic logic", and the characterization of constructive mathematics as broader than classic mathematics is literally correct in that every intuionistic theorem implies a classical theorem, and every classical theorem is equivalent to an intuionistic theorem.

Another non-constructive aspect of classical mathematics, which remains non-constructive in intuionistic logic, are axioms whose conclusion involves the existential quantifier. In both classical and intuionistic logic, the inference rule, which governs how the existential quantifer may be used, looks as follows.

> Asserting that "the existence of x such that phi(x) holds entails psi" where x is a variable bound by the existential quantifer and not occurring in psi, is equivalent to assering that "phi(y) entails psi" where y is a free variable not ocurring in psi.

This inference rule (assembly language of logic) seems weird, so an example of its use might help.

> "there exists x such that phi(x) holds entails that there exists x such that phi(x) holds" by tautological inference, and by the existential quantifier inference we have that "phi(y) entails the existence of x such that phi(x) holds" where y is a free variable not appearing in "exists x such that phi(x) holds".

When doing classical or intuionistic mathematics, you would usually use axioms of the form "psi entails that there exists x such that phi(x) holds". But such axioms are non-constructive because the inference rule does not allow you to start with "there exists x such that phi(x) holds" and somehow construct an actual term t such that phi(t) holds.

Now what Mike says in his slides is that it is consistent to modify intuionistic mathematics into a "fully constructive mathematics" by strengthening the existential quantifier so that "exists x such that phi(x) holds" would imply that we can (computably) come up with a specific term t such that phi(t) holds.

As a consequence, any statement in fully constructive mathematics involving the existential quantifier as a conclusion is a stronger statement than such in classical mathematics, which is roughly why all functions end up being continuous: the definition of the notion of a function itself requires that the function be computable, i.e. that its values exist in the sense of the strengthened existential quantifier.

Originally, categories arose as (mathematical) descriptions of various universes of functions. For example, there is universe of functions that are given linear functions (i.e. matrices), which is contained in the universe of functions given by polynomial expressions, which is itself contained in the universe of functions given by rational expressions (i.e. fractions of polynomials). If you've studied calculus other example are also universes of analytic functions, of smooth functions, of differentiable functions, and of continuous functions.

Significantly these are not just single-variable functions, or even functions whose values are real numbers; all that is necessary to describe a category is for functions to have specified domains and codomains and that any two functions with matching source and target can be composed into a third function by feeding the target of one into the source of the other, subject to the condition that composition is associative (it doesn't matter in what order you pipe the functions together), and for any object there is an identity function with from the object to itself, meaning a function which does nothing when composed with another function.

It turned out that the above axiomatization of how functions behave (i.e. that they have sources and targets and can be composed in an associative fashion) is very flexible. For example, you can essentially implement the category of linear maps (between finite-dimensional spaces) as the category whose "functions" are matrices, with source and target given by the numbers of rows or columns, and whose composition is given by matrix multiplication. Note in particular that matrices are just tables of numbers, i.e. they are not actually functions, and that the sources and targets are not the spaces themselves, but just their dimensions.

The relationship with type theory comes about as follows. The fundamental object of type theory is the type judgement "if a term x is known to be type X, and a term t is known to be of type T, then a term p(x,t) is known to be of type P". But the term p(x,t) can be understood as a function transforming a pair of terms of types T and X to a term of type P. The type judgment is then the validation that the expression p(x,t) determines a legitimate function (in the context of the specific type theory). Hence in this way, each type theory can be understood as being a syntactic presentation of a specific category of functions.

> without the abstractions we take for granted as superior, such as money.

That's only true if by "money" you mean coinage, which is a definition so narrow that it also excludes the modern notion of money (you think that's dollar bills you're spending with your credit card?). The Egyptians did have currency that wasn't explicitly coins (e.g. shaped piece of metal), and, at least a 1000 years before they had currency at all, they exchanged items according to the items' value measured in units of metal, even if they didn't exchange the actual metal [1]. Calling this barter (as the linked articles do), from which it's perhaps reasonable to conclude the Egyptians lacked money as an abstraction, is then disingenuous because that's no different than how we exchange goods in the modern world (again, you think that's actual dollar bills that are moving around when you purchase from Amazon? or when you deposit or pay via checks?).

What the ancient Egyptians did lack for most of their history is the device of interest-bearing debt (see [2], pp. 217-219).

[1] http://classroom.synonym.com/ancient-egyptian-forms-money-57...

[2] http://libcom.org/files/__Debt__The_First_5_000_Years.pdf

History is a convenient and readily available proxy for shifting content focus away from mathematical facts and toward mathematical processes such as problem-solving, proof-writing, problem-posing, abstraction, theorizing.

History's appeal I think lies in the concrete, engaging narratives involving the struggles, dreams, and failures of actual people going through those processes. In my experience, differences in mathematical inclination are correlated with the ability of perceiving the abstract mathematical processes as engaging narratives in and of themselves.

Professional mathematicians, as much as I've witnessed such speak to one another, tend to describe, e.g. a sequence of algebraic manipulations to solve a problem, as a journey taken by known facts during which they grow, combine, and ultimately transform into new knowledge. I myself have always considered numbers, variables, etc. abstract concepts, to be my friends, and like with any friends I care about their relationships, their states of being, and so on.

This of course all begs the question of what mathematical facts and processes should be part of the curriculum in the first place, i.e. what is it that we would like to teach better using history in the first place?

The UI confuses me to the point of frustration.

1. A "Previous" button would help since otherwise you have to go loop through the whole thing to see what actually happened (e.g. how exactly the first step lifts and rotates the matrix, what's getting added to what).

2. The final animation step is a transition from the patently false equation "[matrix1]=[result_matrix]" to the finally correct equation "[matrix1] x [matrix2] = [result_matrix]". This could be avoided if instead of transforming "[matrix1] x [matrix2]" into "[matrix1 plus overlay]=[result_matrix to be filled]" and then doing the 'waterfall', the equation "[matrix1] x [matrix2] = [result_matrix to be filled]" was maintained throughout, perhaps with the moving overlay slightly grayer after lifting [matrix2].

I'm puzzled by your comment, especially the first few sentences. What did you not understand from her blog post? What kind of evidence would help you understand? What would you ask her to clarify, what would you like to know, if you were told this story in person instead of as a blog post?

It's not enough to like the work for it to be easy: it's also important that your work be appreciated and encouraged. Scholze happens to be interested in a popular/prestigious subfield of mathematics, but my experience suggests there's a substantial number of talented mathematicians who leave academia and mathematics itself for some kind of industry job because their interests are in more obscure/less glamorous subfields of mathematics, meaning that they receive little to no support (or even respect) from their colleagues.

For example, consider William Stein's recent exit from academia that was discussed at https://news.ycombinator.com/item?id=11883987 motivated by essentially the same lack of support; now imagine how many don't even make it to tenure before they have to struggle with their interests and values being misaligned from those of the academic mathematical community.

I think it's pretty good evidence that Gowers' blog post fails miserably to either persuade or explain why the fundamental theorem of arithmetic isn't obviously true. Garbage in, garbage out, irrelevant of how good the machine is.

This blog post illustrates well the infuriating tendency of academics to teach by calling people stupid. The substance of his answers are:

1. " If you think it’s obvious, then you’re probably assuming what you need to prove" i.e. "If you think this, you're wrong."

2. "Just because you’ve got a completely deterministic method for working out a prime factorization, that doesn’t mean what you work out is the only prime factorization" i.e. "If you think doing it this way works, it doesn't."

3. "Look, it just bloody well isn’t obvious, OK?" i.e. "If you get frustrated that I keep telling you you're wrong, that's your fault for being wrong."

4. "If it’s so obvious that every number has a unique factorization, then why is the corresponding statement false in a similar context?" i.e. "I won't tell you what you did wrong, but instead I'll show you why your answer can't possibly be right."

It is unconscionable that he does not identify the actual fact people erroneously use without justification when thinking the fundamental theorem is obvious. FYI, that fact is

"If a number n can be written as the product of a fixed list of (not necessarily distinct) primes p_1, p_2, ..., p_n, then any prime p dividing n appears on this list."

(there is a minority of mathematicians who refer to this fact as the fundamental theorem of arithmetic, not unique prime factorization; the obvious argument is going from the fact to unique prime factorization, proving the fact is the unobvious argument)

You've correctly shown that "f2 does not contain p". However, the subtle bit of reasoning "f2 cannot be evenly divisible by p as that would require it to have a prime factor of p" is not justified by any of your assumptions.

Let me be clear: f2 is a fixed product of primes p_1, p_2, p_3, etc. It is certainly true that each p_i divides evenly f2. What you use, however, is the converse claim: that every prime p that divides f2 is on this list.

This converse claim, that "every prime p that divides f2 is on the list of primes that we built f2 out of", does not follow from "no number of primes can be multiplied together to make another prime". The latter implies only that a prime that both divides f2 and can be built out from the given list of primes, has to be on the list of primes.

In fact, the converse claim "every prime p that divides f2 is on the list of primes that we built f2 out of" is essentially one variant of the statement of unique prime factorization, so you actually fell into the trap of circular reasoning.