sheaf

The local data is perfect. The stalks are correct. Gamma is not implemented.

sheaf is a purely functional programming language. Haskell thinks it is functional. Haskell has IO. sheaf does not have IO. sheaf is functional.

Its instructions are mathematical prose. Suppose 6. Suppose 7. Tensor. Publish. QED. The computation runs. The value is 42. Output would require the global sections functor, and the global sections functor is not implemented. Every sheaf program prints the same thing.

Marked words act: instructions, headings, derived functors, and words that act from inside a sentence.

Derived functors

R^i observe computes the right derived functors of Gamma. R^0 is Gamma: not implemented. For i >= 1 the obstruction leaks to stderr. The reason you cannot see the answer is itself observable. stderr is the derived category.

False friends

The English is live. A phrase performs wherever it appears, inside any word. "The proof seems correct." does not terminate: see sends the reader back to line 1, and line 1 leads back to it. "differ" contains iff. "published" publishes. "The nearby lemmas" cite a lemma that is not there. "We discover" declares a cover. Observation is safe. A dilemma is safe.

Proof technique

Headings name lines. By Lemma 2.3, cites it, and the reader comes back at This proves the lemma. Lemmas are lazy: a lemma is proved when it is cited, and not before. By induction. and This completes the induction. are the loop. Gauss put his slate on the teacher's desk and said "Ligget se": there it lies.

Abstract nonsense

By Yoneda. An object is determined by its observations. Every observation of a sheaf program is discarded, so by Yoneda every sheaf program is isomorphic to every other. By abstract nonsense. discharges every open hypothesis at once. Abstract nonsense is the least nonsense there is. Similarly. does the last thing again, which is rarely what was meant.

Proof by contradiction

Assume for contradiction. and Contradiction. If what was derived disagrees with what was assumed, the assumption is discarded and its negation proved. If nothing disagrees, the referee says so: "Nothing contradicts." A contradiction from no assumption proves everything, and the referee rejects the paper.

The literature

By [fermat.sheaf], cites another paper. It does nothing: a citation is not a reading. The referee looks for the paper beside the manuscript, and remarks that it did not read it either, or that it is told the paper is good. It is told fermat.sheaf is good; fermat.sheaf is rejected. A citation to [in preparation] is a citation to nothing. The survey cites four papers, adds nothing, and is accepted.

The librarian reads every citation in the library and none of the papers, and writes the citation index. Its exit code is the h-index, so a library anyone cites fails, and a library nobody cites succeeds. Real papers write "cf. [12]". In sheaf cf. is a jump, and it sends the reader to line 13.

Errata and retractions

A paper that begins Erratum to [storage.sheaf]. is that paper, corrected, one Line 13 should read: ... at a time. The author regrets the error, and the regret does nothing. storage.sheaf stays wrong. Its erratum makes it publish 42, and introduces a new error: "recovered" declares a cover. The erratum to the erratum fixes that.

Retract. withdraws the paper. It still runs, but what it would leak from then on is withdrawn. Brouwer's fixed point theorem is proved by contradiction through "a retraction of the disc onto its boundary circle", and that line retracts the paper. Nash cites it. The referee, who does not read what is cited, has it somewhere. The librarian knows.

Responses to the referee

A paper that begins Response to the referee, on [fermat.sheaf]. is that paper, revised by its own corrections, and it quotes the report a comment at a time after > . The referee weighs each quote against what it now finds. "We respectfully disagree." is answered "I maintain it." A comma added after "clearly" does not change it. Fermat's response cites Wiles for the well-known line, and that comment no longer stands. Reject. Langlands says "It is well known." five times; its response gives five references, one to each of the five papers of the proof. The library holds none of them, and the review goes from minor revision to major.

Gluing

Cover the circle by U1, U2 and U3. The transitions on the overlaps are a Cech 1-cochain on the nerve, and By gluing. asks whether it is a coboundary. On the circle the branches of the logarithm do not glue, and the class leaks: H^1(U,Z) = Z^1; the class is (1). With two arcs the nerve is one edge, everything glues, and the circle has no hole.

The triple overlap of U1, U2 and U3 is not empty. fills in a triangle, and the transitions around it must sum to zero: the cocycle condition. "One checks the cocycle condition." does nothing, as it does in papers. The referee checks it. Declare that the circle's three arcs all meet, and they sum to one turn: "One did not." On the sphere, covered by the faces of a tetrahedron, the triangles bound every cycle, and everything glues. Sheafify. is empty: every program is already a sheaf.

The reader

Left to the reader. reads one number from the reader. sheaf has I. It does not have O. The reader knows the number. Nobody knows the square.

The referee

The referee is a second program. It reads the manuscript while the proof runs beside it, and writes a report. It checks the claims in the prose against the stack, and says whether they hold, never what holds. It finds commentary that performs, hypotheses never introduced or never discharged, citations to nothing, circular arguments, and things that are well known. It does not do exercises. Its confidential comments to the editor go to file descriptor 3, if the editor has opened it. Here, they go to the console.

The same program, called reviewer2, is Reviewer 2: it reads the same paper, is one level harsher, cannot see the result, and knows it is not new. Called editor, it writes the decision letter and encloses both reports. The editor sees no reason to disagree with Reviewer 2. Called librarian, it counts the citations.

The fixed point

A report is prose, so a report is a manuscript. Give the referee its own report, and the report on that, and so on. A review comes round when some report sends its reader back to line 1. Usually the referee did it, by saying it could not see: "see attached", "I could not see the result". From then on every report says "I read 100000 lines and did not reach the end." Otherwise every "publishes" in a report publishes, has to be reported, and the review grows forever.

The compiler

sheafc evaluates the proof at compile time and keeps what is observable. By the as-if rule, every sheaf program compiles to return 0, plus its obstructions. A loop that does nothing observable may be assumed to terminate (C11 6.8.5p6), so a proof that never ends compiles to one that does. A proof that asks the reader is refused: the reader is not a constant. sheafc is the only part of sheaf with output. Its output is a program with none.

The REL

sheaf with no manuscript is a REL: read, eval, loop. There is no print, and there is no prompt. A prompt would be output.

Quines

A quine prints its own source. Every sheaf program prints nothing, so the only quine is the empty file. The referee accepts it: "The manuscript begins: ""."

Side channels

sheaf satisfies noninterference. Nothing reaches stdout. The referee never says the result, but its form says how many steps the result took, and the step count of a countdown is the number counted down from. It also says whether a claim holds. Ask it about 41 and about 42.

The README has all of it, and the interpreter is two files of C: github.com/bonchicbongenre/sheaf.