Sigbovik 2016

Click for full version PDF

the association for computational heresy presents

a record of the proceedings of

SIGBOVIK 2016

the tenth annual intercalary robot dance party in celebration

of workshop on symposium about 2⁶th birthdays; in particular,

that of harry q. bovik

carnegie mellon university

pittsburgh, pa

april 1, 2016

0xe1d22e91e99f76eb160a79b78c055cc7bcb8bda16ea09d3214ab7f8e58923338

SIGBOVIK

A Record of the Proceedings of SIGBOVIK 2016

ISSN 2155-0166

April 1, 2016

Copyright is maintained by the individual authors, though obviously
this all gets posted to the Internet and stuff, because it's 2016.

Permission to make digital or hard copies of portions of this work for
personal use is granted; permission to make digital or hard copies of
portions of this work for classroom use is also granted, but seems
ill-advised. Abstracting with credit is permitted; abstracting with
credit cards seems difficult.

Additional copies of this work may be ordered from Lulu; refer to
http://sigbovik.org for details.

0x80f48f0c2d9724a7a28bb81ebb904b67db25788ff9ba10095c71fa7511cb0e47

SIGBOVIK 2016

Message from the Organizing Committee

Welcome, my dear friends, to the tentth annual Intercalary Symposium
about Workshop on Robot Dance Conference in Party of Harry Q. Bovik's
10^{1*.*80617997398}th Birthday! This edition of the Party is a very
special one, as the edition number coincides with the common human
counting base (Figure 2).

Figure 1: Visualization of SIGBOVIK the Tentth.

Figure 2: The tent-based counting system is the one most commonly used
by humans because, it is widely assumed, they have tent fingers.

Of course, as robots (who are perpetually busy with dances, parties,
and/or symposia), this is not our native counting system, but we
figured it would be a great opportunity for some cultural outreach to
try to welcome more humans into our prestigious conference. In our
native tongues, this Party's edition number would be rendered as 1010,
0xA, or KILL ALL HUMANS, depending on the dialect of Robotic.

0x4b1fa7cc2fe8d6530b64f2db76fedaebfd649350552d2c499836c5ffca5fa777

This has been a remarkable year for computer-human diplomacy in the
mainstream, most notably thanks to the achievements of AlphaGo, as
depicted in Figure 3. We hope to reflect the same spirit of
collaboration in our prestigious Dance Conference.

Figure 3: A recent HUMAN BEING CRUSHED SUCCESSFUL COLLABORATION
between humans and robotkind.

At this time I would like to propose a toast (Figure 4) to many
continued collaborations between robots and humans, and to many powers
of tent more years of SIGBOVIK.

Figure 4: A toast.

The toast having been proposed, and eaten (that's what humans do,
right?), I now present the proceedings of SIG BOVIK 0xA.

With AFFECTION LEVELS COMPUTED BY MAIN THREAD 28743 NOT IN EXCESS OF
34.7 much love,

BOVIK BOT INSTANCE 0x7E0

0x2da05ce95c08626a2288c1560009b165bc305be913584a8ad8d3f6d241d2845d

ToC About Proceedings! Have We Got Papers for You!

Programming Languages

5

1 Modernized Python

6

2 Grand Challenges in Programming Languages Position Paper: What, if
any thing, does multiplication even mean?

13

3 A Type-and-Affect System for Semisignificant Whitespace

16

4 brainfuck++: a much needed extension to brainfuck

23

: Other Languages

33

5 Tironiculum: Latin Speech Recognition via Latin Text-to-Speech 34

6 Abecedarial Acrostic, Alphabetized Amusingly Because Beings
Blissfully Cause Celebratory Centennials... (Note: Full Title is
Longer)

40

7 On "Ra-men, Ra-men ramen ramen"

41

8 ACTION: A Catchy Title Is all yOu Need!

42

9 A Deep Learning Approach for Deeply Inaccurate Wordle Solving 43

Systems

45

10 Edward, edMUnD & Edwin: Line-Based Text Editing for the 21^st
Century 46

11 A Free Computer Vision Lesson for Car Manufacturers or It is Time
to Retire the Erlk¨onig

52

12 Redundant Coupling

54

: Theory

57

13 Destructive Logic

58

0x28463669015a122e58186308ffa8df5146906ea1e0820d3a2700803b533d03cd

14 Overlap-Maximal Graph Labelings: Graph Labelings with Non-Disjoint
Ver tex and Edge Sets (and how they can be used for encryption,
poetry, and breaking mathematics)

62

15 Neo-classical Logic: Une Logique non classique

69

16 A Patriotic Analysis of Programming Paradigms

76

17 On Ruinment: Ruination Theory and its Consequents

84

: Astrophysics

91

18 Method and Tool for Estimating the Mass of the Black Hole Located
in the Office of Immigration, Refugees and Citizenship Canada Causing
a Supermas sive Time Dilation in the Visa Extension Process

92

19 Black Hole Computation

102

20 Schr¨odinger's SAT: Generalizing Quantum Bogosort to Prove P = NP
Under Many-Worlds Quantum Mechanics

109

21 Solving Double Execution of Java's paint() Method by Counting Down
to the Heat Death of the Universe (plus language compendium)

111

: Climate Science

139

22 Towards Cloud Computing

140

23 Ecological Memory Management: Beyond Garbage Collection

144

24 Infrastructure-as-PowerPoint: A No-Code Approach to Cloud
Infrastructure Management

166

25 On the Possibilities and Challenges of Organic UAV-Assisted MEC

172

A Brief Musical Interlude

177

26 Baby Sharks are More than Sharks . They are Earworms Sung More than
Happy Birthday Perhaps

178

27 Everybody Clap Your Hands: The Cha Cha Slide is Turing Complete
184

0x3aed03ffd6ff8593f8362b3b7c3aa149565a5b934b5863a75e7e51b19dbb7cd1

28 Exhaustive Survey of Rickrolling in Academic Literature

189

: Best Practices

201

29 Quadruple-Blind Peer Review

202

30 Optimal degeneracy through OwO based variable names

206

31 Multiplication by repeated addition, with fraction handling.

208

32 Objective Correlation Metrics for Quality of Code Estimation

209

: Algorithmic Advances

215

33 Functorial wrappers for high-dimensional classification algorithms
216

34 (Un)helper functions

220

35 A sometimes-accurate O(1) search algorithm

223

: Mathematic Retreats

225

36 Improved Data and Instruction Locality in Long Division

226

37 The New New Math: using sentiment analysis of mathematics word
problems to gauge children's reactions to teaching 8-bit floating
point arithmetic for the new California public school math curriculum

229

38 Infix Modifiers for Flexible Multiplication

236

: Aesthetics

239

39 Real-Time Foliage Simulation

240

40 Using deep CNNs to prove that I look better than Tom Cruise and
Shah Rukh Khan combined

241

41 EBMP: Efficient Bitmap Encodings on Ethereum Virtual Machines 243

42 A Machine Learning Approach To Classifying Cuteness

251

0x38c999bf1bbe61738281e53d6e40c821ae8dae9421158b0ae21dea443980c03a

43 Attractiveness Learning: A General Solution for the Cold-Start

Problem 253

Hardware

257

44 Correct-It-Yourself Paper Updater

258

45 Harder Drive: Hard drives we didn't want or need

259

46 Just a Regular Paper

278

47 Wearable RF-shield repositories

279

: Black Boxes

281

48 A 23 MW data centre is all you need

282

49 When Pull Comes To Shove... Do Both!

293

50 man exorcism

338

51 2x a fake submission

340

: SIGBOVIK

343

52 Analysis of A New Error Calculation Technique

344

53 A Third Thorough Investigation of the Degree to which the COVID-19
Pan demic has Enabled Subpar-Quality Papers to Make it into SIGBOVIK,
by Reducing the Supply of Authors Willing to Invest the Necessary
Effort to Produce High-Quality Papers

345

54 this is not a review

346

0x64c7975e74f9f5b19a5fd9416c8ddc675885421708092d4616b42b9403b062b2

Half-track

Crypticography

1 Modernized Python

Daniel Ng

Keywords:programming languages, type theory, python, sml

2 Grand Challenges in Programming Languages Position Paper: What, if
anything, does multiplication even mean?

Jim McCann

multiplication, punctuation: *, punctuation: x, punctuation: ., grand
challenges

3 A Type-and-Affect System for Semisignificant Whitespace Stefan
Muller

Keywords: whitespace, white space, white nspace

4 brainfuck++: a much needed extension to brainfuck

C´edric Ho Thanh

Keywords: Programing langage, brainfuck, concurrency, machine learning

0x2d691bc0c7cccbd03378aec4ec4d0a3a563b88a2973276c9ef9cab9f6290f99e

0x425d22427978b6bc28a67815c2a61353e20a5c91861a656ac8ca6faa79299ec0

1 {width="0.9999945319335083in"
height="1.9644553805774279in"}

Cryptographically secure page numbering in L^AT_EX

William Gunther Epic

wgunther@epic.com

Brian Kell Google, Inc.

bkell@google.com

April 1X, 2016 XXXX

Abstract

Security in the modern world is of national importance. Personal in

formation is being collected, stored, and analyzed by many
governmental

agencies, both foreign and domestic, as well as companies and organiza

tions. People are looking to cryptographic solutions to keep their
infor

mation safe. Yet the printed word has not changed in its security
since

the early 15^th century. This paper makes the first steps toward bring

ing modern cryptography into the 1470s by introducing a L^AT_EX
macro

package to enable cryptographically secure page numbers. No longer
will

your document allow random access into your data. Our L^AT_EX
package

uses modern, secure hashing algorithms to prevent unauthorized access
of

page numbers by eavesdroppers and adversaries.

Contents

X1
Introduction0x2d691bc0c7cccbd03378aec4ec4d0a3a563b88a2973276c9ef9cab9f6290f99e

X2
Background0x425d22427978b6bc28a67815c2a61353e20a5c91861a656ac8ca6faa79299ec0

X2.1X Previous work . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 0xc2082a19550b2a2c2b0b95cbdcb

X3 Secure page numbers in
L^AT_EX0xc2082a19550b2a2c2b0b95cbdcb432a693ce0c72109e2d867cb3cb0e3d11ffe9

X3.1X Implementation details . . . . . . . . . . . . . . . . . . . . .
. . . 0x654c937186a719b8cf18de2956b9X3.2X Protecting other numbers . .
. . . . . . . . . . . . . . . . . . . .
0x654c937186a719b8cf18de2956b9X3.3X Security recommendations . . . . .
. . . . . . . . . . . . . . . . . 0xce65a4631ce9cd559d11180dcf75

X4 Conclusions and future
work0xce65a4631ce9cd559d11180dcf7562f398f61c69ca659896986ddaa0d7faf31a

X1 Introduction

In light of recent security breaches, secure communication has become
more

important than ever. Recent advances in cryptography have found such
diverse

0x2d691bc0c7cccbd03378aec4ec4d0a3a563b88a2973276c9ef9cab9f6290f99e

0xc2082a19550b2a2c2b0b95cbdcb432a693ce0c72109e2d867cb3cb0e3d11ffe9

applications as online communication, commerce, information storage
hardware, {width="0.9999945319335083in"
height="1.9644553805774279in"}

and voice correspondence. However, to the best of our knowledge,
strong cryp

tographic techniques have, surprisingly, not yet been applied to page
numbers.

Page numbers are ubiquitous and are quite important for page-based com

munication. In this paper we introduce a new
L^AT_E^{X macro package, secure} page-numbers.sty, that enables
cryptographically secure page numbers.

In addition to the immediate impact of protecting page numbers against

unauthorized access, we hope this work will inspire future research on
securing

such things as section numbers, figure numbers, and citation numbers.
As a

provisional security measure until such work has been done, our macro
package

provides facilities for securely redacting this sensitive information.

The remainder of this paper is structured as follows. In Section 2X on
page

0x425d22427978b6bc28a67815c2a61353e20a5c91861a656ac8ca6faa79299ec0, we

describe the problem in more detail. Some notable previous work on the
prob

lem has been done; we give a brief overview of this work in Section
2X.1X on page

0xc2082a19550b2a2c2b0b95cbdcb432a693ce0c72109e2d867cb3cb0e3d11ffe9.
Our

new method is described in Section 3Xon page
0xc2082a19550b2a2c2b0b95cbdcb432a693ce0c72109e2d867cb3cb0Details about
our implementation are given in Section 3X.1Xon page
0x654c937186a719b8cf18de2956b9b1ec81e418Some brief initial
observations about protecting other numbers in a document,

such as section numbers, are described in Section 3X.2Xon page
0x654c937186a719b8cf18de2956b9b1ec81e4189173and additional security
recommendations appear in Section 3X.3Xon page
0xce65a4631ce9cd559d11180dcf7562f398Finally, we conclude in Section
4Xon page
0xce65a4631ce9cd559d11180dcf7562f398f61c69ca659896986ddaa0d7faand
suggest some avenues for future work.

X2 Background

Page numbers have been a common feature of printed material since the
1470s.

However, their nearly universal use is fraught with security issues
that are often

overlooked.

For example, if an eavesdropper merely glances over the shoulder of a
per

son reading a sensitive document, the page number is instantly
visible. If the

eavesdropper can also get the last page number of the document, then
she can

quickly compute the percentage of the document that has been read. Two
such

observations, timed carefully with a stopwatch or large sundial, can
provide the

eavesdropper with enough information to estimate the remaining reading
time.

Armed with this knowledge, the eavesdropper can commence other
attacks,

knowing that the victim will be busy reading the sensitive document.

Many organizations and individuals use paper shredders to destroy
sensitive

documents. But, because of their small size, page numbers are often
incom

pletely destroyed by these shredders. Unsecured page numbers leak
information

about the order of the scraps, which can aid a snooper who is trying
to recon

struct a shredded document. The mere presence of a scrap bearing a
large page

number like 438 reveals to an adversary the potentially sensitive
information

that a lengthy document has been shredded.

If documents are printed on both sides of the page, these problems are

0x425d22427978b6bc28a67815c2a61353e20a5c91861a656ac8ca6faa79299ec0

0x654c937186a719b8cf18de2956b9b1ec81e41891736f092a7e0a87e9ea0b1c8c

compounded: a page number reveals information about not only its own
side of the page, but the other side too. In many documents, right-hand
pages have odd page numbers while the page numbers on left-hand pages
are even. So an eavesdropper in possession of an unsecured page number
gains information not just about the order of the pages or the length of
the document, but even the geometric position of the page.
{width="0.9999945319335083in"
height="1.9644553805774279in"}

X2.1X Previous work

One of the earliest techniques for page-number encryption, and by far
the most widely employed today, is a Roman cryptosystem for page numbers
in partic ularly sensitive early sections of a document, such as
prefaces, forewords, and tables of contents. Unfortunately, while this
algorithm is widespread, it has never been supported by strong
cryptographic justification. In recent decades, concerted efforts by
many researchers have identified significant security flaws in this
method. For example, Hagenfried et al. [1X] describe an attack that
was able to recover the plaintext "24" from the encrypted page number
"xxiv" in less than seven hours on commodity hardware.

Some of the security issues that arise with page numbers in two-sided
doc uments were addressed indirectly in the work of M¨obius [3X],
which was later extended by Klein [2X]. However, one difficulty with
these approaches is that the constructions they describe are
non-orientable, which implies that they cannot be used for documents
written in languages such as Chinese or Japanese. Our method is free
from such regional restrictions.

X3 Secure page numbers in L^AT_EX

In order to address these issues, we propose a new method of securing
page numbers in documents, using cryptographically secure hashing
algorithms to replace all page numbers with salted hash values. In
addition to obscuring the plaintext page numbers, this technique also
produces much longer strings, which will be more likely to be
obliterated by shredding.

Our L^AT_EX macro package is called secure-page-numbers.sty, available
upon request from the authors. It can be included in any L^AT_EX
document with the command \usepackage{secure-page-numbers} in the
preamble, and se cure page numbers are enabled with the command
\pagenumbering{shahash}.

Once secure page numbers are enabled, all page numbers in the document
will be replaced by cryptographically secure hash values. This provides
a con venient drop-in solution providing maximum security.

The use of a one-way hash function means that it is possible for an
autho rized reader of the document to verify a hunch about what page she
is on, by computing the hash of the hunch, but an eavesdropper cannot go
backward from the hash to the page number.

Additionally, an eavesdropper cannot use the last page number to
determine the length of the document. Gone are the days of reading War
and Peace on

0xc2082a19550b2a2c2b0b95cbdcb432a693ce0c72109e2d867cb3cb0e3d11ffe9
0xce65a4631ce9cd559d11180dcf7562f398f61c69ca659896986ddaa0d7faf31a

the bus and having a stranger say, "Wow, that's a big book!" With crypto
graphically secure page numbers, an eavesdropper can't tell whether it's
a long novel or a short pamphlet.
{width="0.9999945319335083in"
height="1.9644553805774279in"}

X3.1X Implementation details

Our implementation uses the SHA-256 hash. It features a modular
architecture, however, so that a different hashing algorithm can be
substituted if desired. In order to thwart rainbow-table attacks, a salt
is appended to the page number before it is hashed. We are currently
using the L^AT_EX job name as the salt. For example, the salt used for
this paper was sigbovik.

^{Initially we attempted to implement the SHA-256 algorithm entirely in T}_EX
macros. However, we soon ran into difficulties, including the arcane
design of the
L^AT_E^{X system and memory limitations built into the T}_EX
engine itself. ^{We were surprised to find that T}_EX does not
have native support for bitwise operations on 32-bit unsigned integers.
Since we can see no innocent reason to omit such functionality from a
typesetting system, we suspect this must be an intentional deficiency
added by the NSA in order to weaken cryptographic
^{algorithms in T}_EX documents. We urge further investigation into
this potential security backdoor.

To circumvent this problem, our L^AT_EX package calls an external Perl
script to generate the appropriate SHA-256 hashes from the salted page
numbers. This does require that L^AT_EX (or pdfL^AT_EX) be called
with the --shell-escape option.

Our current design requires a fixed upper limit to the page numbers in
the document. We have set this limit to 500, but it can be easily
increased by editing the Perl script. If the page numbers in a document
exceed this value, processing of the document will halt with the error
message

! tl;dr.

The elimination of this fixed limit is left as an improvement for future
work.

X3.2X Protecting other numbers

A natural next step after securing page numbers is to secure other
sensitive numbers in a document, such as section numbers, figure
numbers, and citation numbers. If these numbers are not carefully
guarded, they could be used by an attacker to learn partial information
about the order of pages.

Our
L^AT_E^{X package does not yet support securing these numbers with crypto}
graphic hashes, but as a provisional security measure we have included
macros to redact these numbers from the document. For instance, the
redaction of section numbers can be enabled with the command
\redactsectionnumbers. Section numbers have been redacted in this paper
to illustrate the technique.

0x654c937186a719b8cf18de2956b9b1ec81e41891736f092a7e0a87e9ea0b1c8c
0xc50e747b92c42e0a7c53ac8b0f0536dc170cd2c638b6e9c16e4e79656e2349af

X3.3X Security recommendations
{width="0.9999945319335083in"
height="1.9644553805774279in"}

When properly used, cryptographically secure page numbers make it
impossible for an adversary to determine the order of the pages of a
document without an expensive Ω(n!) time brute-force attack. However,
in order to support this security, it is important for the document to
be kept as loose pages (preferably one-sided). We strongly recommend
against the use of binders, staples, paper clips, file folders, and
other external devices that may inadvertently reveal in formation about
the proper order of the pages. To maximize security, it is best to take
all the pages of many documents together and throw them at random into a
big sack. Another effective randomization algorithm is to toss the pages
down a flight of stairs or off a suitably tall cliff.

The proper disposal of a sensitive document is also important. Some
paper shredders, often called cross-cut shredders, cut a document in
two directions, yielding many tiny bits of paper. On the other hand,
other shredders, so-called strip-cut shredders, merely slice the
document into strips. If a page containing one or more hashed page
numbers is fed into a strip-cut shredder in a certain orientation, it is
possible that each one of these hash values will end up on a single
strip, so a snooper can easily pull out individual strips and read off
the complete hash. Of course, the fact that the page number has been
hashed means that the snooper will have difficulty gaining any useful
information from this, but to maximize security when using a strip-cut
shredder it is best to print every page number twice, once horizontally
on the page and once vertically, to ensure that at least one of them
will be obliterated by the shredding process. (This recommendation
applies equally well to all sensitive information in the document, not
just the page numbers.) Our L^AT_EX macro package does not yet support
vertically printed page numbers, but we expect that this functionality
will become available in the near future.

X4 Conclusions and future work

In this paper we have proposed a new technique for securing page numbers
in L^AT_EX documents using cryptographic hashing algorithms. We
introduced the macro package secure-page-numbers.sty, which implements
this technique. We believe that this package has broad potential to
significantly increase the security of page numbers in sensitive
documents, and we urge all authors and publishers to adopt the use of
secure page numbers as soon as possible.

One potentially fruitful extension to this work, which we have not yet
ex plored, is the use of a public-key cryptosystem such as RSA for the
encryption of page numbers in two-way communication. This is likely to
be more useful than one-way hashes, since each party will be able to
decrypt the page numbers in the document received from the other party.

In accordance with the first of our security recommendations above, it
may be beneficial to scramble the pages of the document not only after
they have been printed but also in the PDF itself. A L^AT_EX package
to achieve this would

0xce65a4631ce9cd559d11180dcf7562f398f61c69ca659896986ddaa0d7faf31a
0x7df8eefe1bc490220b2b34a09be0f925ebcdf1af8cea93a31e972faef5ce5a10

^{be difficult because of the design of the T}_EX engine, but
we believe it may be
{width="0.9999945319335083in"
height="1.9644553805774279in"}

possible with the aid of an external tool. As a workaround until this
becomes

available, we recommend storing large PDFs on a sequence of unlabeled
floppy

disks, which can then be shuffled together.

References

[1X] Hagenfried, E.W., McPaulsen, F. J., and Svendt, P. Ex

ploiting pseudofrequency eigenquotients to attack page num

ber encryption. IEEE Trans. Crypto. Splat. XX28(3X), pp.

0x2fd5f03a787301a109748c1243f85f6522c3c862be9e1b156c84ef8dfaf9c296--

0xbfbd44e30f1d9beef64f9324993b67e99bb1688ed77f474c46e58b2aca9c23dc,

November 2011 XXXX.

_{[2X] Klein, F. *Uber Riemann's Theorie der algebraischen Functionen und*}¨

ihrer Integrale: Eine Erg¨anzung der gew¨ohnlichen Darstellungen,
pp.

0x2fa9b01782ee3680c2682f88fb03913ae03ff998602c90a0f8b2129567589535--

0x9d7cf761c701b006aba29b8b4830eb46c78c28d8c4d448b4a5981a37697cb949,

XXXX 1882.

[3X] M¨obius, A. F. Werke, vol. 2X, pp.
0x3292d92ba775c2cac72f8e9091e04b3915d3ca7463c3c7b936ec7bede9933f9e0x034c4ae2b61541e3a32124700b7c99c63974fb30d353649ec2fa828c5d90ec75,

XXXX 1858.

0xc50e747b92c42e0a7c53ac8b0f0536dc170cd2c638b6e9c16e4e79656e2349af

0x5a9dcef798e74a263edb8c0341660890e2bd75f295fef29fbfd1f6429cacfe66

CONFIDENTIAL COMMITTEE MATERIALS

SIGBOVIK 2016 Artifact Evaluation

Paper 18: Cryptographically secure page numbering in La

Claim 1: The authors claim to have implemented a crypto library for
Standard ML.

EVALUATION OF CLAIM: It was very difficult for the committee to assess
this library because we could not even identify what language it was
in. Due to the combination of references in German and a .pl file
extension, we assumed the library was written in German Prolog. We
gave the code to a local German Prolog expert for further analysis,
but his evaluation consisted only of the single word "Achtung".

Due to numerous references to Arabic and a wide variety of Arabic
numerals in the text, we next tried interpreting the library as
Arabic, with equally little success. A senior PC member then pointed
out that .pl stands for Programming Language (this is why we keep the
programming languages group around) after which we tried running the
code as a Program, and finally found success.

The code ran with the desired effect, and the committee was impressed.
However, we think you may have gone overboard with your security
measures, because the source code itself appeared to be equally
encrypted, and even after running it, we have no idea why it worked.

Claim 2: The provided encryption method is robust to Shredders.

EVALUATION OF CLAIM: The artifact committee had actually already
unwittingly evaluated this claim when we attempted to shred the
submission without reading it. Luckily for all involved, our
department has a surprising dearth of shredding equipment, after which
we decided to actually read the paper.

We do, however, have an SNES, which we used to evaluate this claim by
playing our old Teenage Mutant Ninja Turtles games. When we got to the
final battle with Shredder, the submission actually ripped the
controller out of our hands and quickly defeated the final boss.

This scheme is beyond Shredder-proof.

0x97355d1ba0a12c846cf80e1ff72603b9e98764aaaf1a9455d271e20e67b39097

OVERALL EVALUATION: This encryption scheme is worth its salt. The
artifact provided is of such quality that we extend an invitation to
publish an extended article in our Journal: SIGBOVIK Heretics
Anonymous Digest: Volume 256.

ADDITIONAL COMMENTS:

• The LaTeX implementation included extensive use of CS names. In
the final draft of your paper, please elaborate on why names from
other scientific fields were not supported and list this as a
limitation of your current implementation. That being said, the
committee is not concerned by this restriction.

• There was also much discussion of ex-leaders in the LaTeX code.
Given that we're in the middle of a heated election year, it may make
a more interesting read to focus on current leaders.

2

0x1f84e6ea9f3ec349a9f9279216c443e9f805ec9ddc29d91f51b69c2a72932df1

2

Abstract

Random Seed Encryption

Alexander R. Frieder*^∗*

21,876,528 782,847,088,000*^†*

April 1, 2016

We, however, like to go against the grain in

We present a novel form of encryption, wherein the encryption step is
computationally expensive while the decryption step is more or less
trivial. We will describe how the scheme works, proving its correctness
along the way. We will then show that this encryption scheme has many
uses, for example, prevention of texting while intoxicated or sender
identification over email. We will also acknowledge the limitations
imposed upon our beautiful scheme by the cruel harsh mistress of
reality. Finally, we will discuss the immeasurable impact this algorithm
could, nay, will have upon the world.

1 Introduction

It is universally understood among nearly all ex perts in the field of
cryptography [1] that any good cryptographic encoding function has
four fundamental properties:

• it is quick to compute the hash value for any given message

• it is infeasible to generate a message from its hash

• it is infeasible to modify a message without changing the hash

• it is infeasible to find two different messages with the same hash

*^∗*email: alex.frieder@gmail.com

*^†*This is the encryption of the author's name using C's default
long-seeded PRNG.

terms of what is "universally understood". Thus, we posed the
question: what if the first two con ditions were switched?, that is,
what if we had a hash function where it was nearly infeasible to
compute the hash value, but quick to generate a message from its hash?
Thus Random Seed Encryption (RSE)(not to be confused with the lesser
known RSA) was born.

We have come up with one such function and will spend the rest of this
article analyzing and disucssing it, with applications in encrypting
words, though any datatype could theoretically be encrypted.

2 Encryption Algorithm

The encryption algorithm takes a word and cal culates two associated
numbers for it: the length, `, and a seed, s, to a pseudorandom
number gen erator (PRNG) such that s, is the smallest seed such that
the next ` numbers generated, when converted to letters, spell the
word. These two numbers are mapped to a single number, which is the
encryption of the word.

2.1 PRNG to Letter Conversion

In general, PRNGs output either a random real number between 0 and 1
or a random integer between 0 and N. Any function that takes one of
these numbers as input and deterministically returns a letter, where
the probability across all numbers in the domain of getting any given
letter

0x5b120f61e213712179c10495814d0a74e99f5f7461a15d0a02bd6ada44a0a758

is approximately ¹₂₆ will suffice. However, since constructive
proofs are all the rage these days, we will briefly discuss our chosen
functions.

To convert a random real 0 ≤ r \< 1 into a letter, partition the
space [0*,* 1) into 26 sections, [0*,¹₂₆ ), [ ¹₂₆
*,²₂₆ ), . . ., [ ²⁵

₂₆ ^{, 1). If your random num} ber falls into the *i*th section,
then your letter is the *i*th letter. This clearly works. Even more
trivial is the proof that every letter has an equal probability.¹

To convert a random integer 0 ≤ n \< N into a letter, take i = n
mod 26 and use the i*th letter. For *N ≥ 2500, the difference from
¹₂₆ is less than 1%.²

Now we know how to convert random numbers to random letters and we can
move on to finding the right random numbers for our specific letters.

2.2 Finding the Correct Seed

PRNGs are not actually random and honestly, they are not fooling anyone.
PRNGs just pro duce a very very very very long list of bits that are
converted into numbers in some range. And this list of bits is always
the same! The trick used is to start at different points in the list so
it at least seems random. This starting location is called the seed.

If you set a PRNG to a specific seed and gen erate a list of random
numbers, then reset to the same seed and generate another list of
random numbers, the two lists will be identical. Our goal is to find a
specific seed that will produce our word.

For example, if you set the default Python PRNG to seed 1,944,062 and
generate five ran dom numbers, converting them to letters as dis
cussed above, you get "hello", which is a nice message many people
would want to send, prob ably. How do we find seed 1,944,062?

Well, you can set the seed to 0, see that the word of length 5 generated
at this seed is "vtkgn", which is not "hello", set the seed to 1, see
that the word of length 5 generated

¹Proof left as an exercise for the reader.

²Proof left as an exercise for the reader. But actually it is true.

is "dwtgm", and repeat until you set it to 1,944,062.

Surely this na¨ıve brute force algorithm is just the first in a set of
stepping stones to some more intelligent algorithm, no? No. The whole
point of a PRNG is that it seems random. Knowing these five letters
tells you nothing about the next five, or where any given five letters
will be.

There is no way to determine where some given letters will appear in a
sufficiently com plex (known in the technical world as "crypto
graphically secure") PRNG without trying every possibility until they
are found.[2]³ That is what makes this algorithm so powerful.

2.3 Merging the Seed and Length

Having the correct seed, s, is not enough; you also need the length
of the word, `. We could of course just encrypt every word as two
num bers, but that means we need twice the space. Instead we will use
the well-known bijection be tween N × N and N, f(x, y) =
2*<sup>x</sup>(2*y + 1). We will use f(`, s) since ` s and this
function grows exponentially in the first argument, but linearly in
the second. Any other bijection be tween N × N and N will work, but
we use this one since it is clearly the best.[3] Thus, we now have
all the machinery necessary to take a word and fully encrypt it into a
single number.

3 Decryption

Decrypting a word given the encrypted number is extremely easy.
Looking at the bijection we used, the length of the target word is
exactly the number of times we can divide 2 into the encrypted number.
The remaining odd number is one more than twice the seed.

For example, if our encrypted number is 124,420,000, we halve it as
many times as we can. 32 divides this number evenly while 64 does not.
Thus the length is log₂ 32 = 5.

³This result is probably shown in this citation. It is reallllllly
long and we reallllllly do not want to read it. But it is there. we
promise.

0x6dc2eb536b763255b96774047e8517f88ab4ed1dcf0a26373bed6cac4c10a6c6

We are left with 3,888,125. The seed is thus 3*,888,125−*1

₂ = 1*,* 944*,* 062.

Now that we have our seed and length, we set our random number
generator to that seed and generate 5 random letters. In this case, we
get the letters, in order, "h", "e", "l", "l", and "o", which spells
"hello". Thus the number 124,420,000 uniquely encodes the word
"hello".

4 Discussion

We have fully described how and why this en cryption method works, but
as with all theoreti cal algorithms, there are some limitations due to
the realities of physics and computers.

Every PRNG has some finite period, after which the PRNG starts
repeating values. This places a hard upper bound on the number of
words we can encode with a given PRNG. Addi tionally, we are further
bound by the number of unique values we can use for the seed.

For example, when the seed is an integer, commonly represented by
4-byte values, we can uniquely represent 2³² − 1 = 4,294,967,295
seeds and thus words. In this case, it is sufficient to represent all
12,356,631 words of length 6 or less, but not enough to represent all
8,031,810,176 words of length 7. Similarly, using 8-byte longs as the
seed we can represent all words of length 13 or less. However, 13 is a
big number and a lot of words can be represented using less than 14
letters. In fact, not a single word in this paper has more than 13
letters. So there.

Additionally, there is no guarantee that a given word will actually
appear in a PRNG. For sufficiently long words, a given sequence of ran
dom numbers might just not be an output of the PRNG. However, since most
combinations of letters are not words, this is likely not to be a
problem in actuality.

5 Applications

Random Seed Encryption clearly has numerous significant uses in modern
life. One such use is to

prevent drunk texting/messaging. Studies have found that drunk texting
friends, former lovers, family members, and even bosses can have terri
ble terrible effects on one's life.[4] Even worse is drunk posting
on Facebook, reddit, or the reader's social media website of choice.
Imagine some kind of filter you can turn on, where for the next k
hours, anything you want to send to someone or post somewhere has to
be encrypted using this method. Of course, no one under the influence
could ever manage to correctly encode even a single word! Thus drunk
messaging is prevented.

Another possible application is that of sender verification. Many
people try and verify their identity over email using PGP encryption,
but that is a lot of work for the receiver, and hon estly, we all know
no one really cares that much. However, sending someone a message
under this encryption scheme has a two-fold benefit over PGP: it is
much easier to decrypt, so the receiver might actually bother with it,
and since RSE is so new, no one else in your social circle except you
will even have heard of it, so the encryp tion is definitive proof
that you actually sent the message!

Thus we have demonstrated that not only does RSE have real world
applications, but it has nu merous benefits over other, more commonly
used encryption schemes. We hope this will encour age the
cryptographic community to spread the good word about Random Seed
Encryption.

6 Future Work

There are numerous ways this novel direction of research can be
expanded. For example, we would love to consider:

• This algorithm using "true" random num ber generators. This would
obviously com plicate matters since seeds no longer exist, but we are
sure some bright, spunky under graduate student could figure out a
solution.

• Encryption schemes where both the encryp

0x17eb2ba0b6e2fc7438d64d9fd0036862571ce946e0570f6db15e54fbef93dc26

tion and decryption steps are computation

ally expensive.

• Alternative encryption functions that are,

for example, Ω(2*^`*).

• Something involving quantum computers

working on big data in the cloud

We believe this paper may be the dawn of a

new field of computer science, which we have pre

emptively named the Friederian Sciences.

7 Acknowledgements

We would like to thank a handful of people:

Zachary Piscitelli, who came up with the original

name for this paper, which I have since changed,

but I feel bad taking him out of this section;

Thomas Bayes, without whom none of this work

would be possible, for very obvious reasons; you,

the reader, for getting this far; and finally, my

computer, for spending hours upon hours trying

billions upon billions of different seeds.

References

[1] Wikipedia contributors. "Cryptographic

hash function." Wikipedia, The Free Ency

clopedia, 14 Jan. 2016. Web.

[2] R¨ock, Andrea. "Pseudorandom Number

Generators for Cryptographic Applications."

Thesis. Paris Lodron University of Salzburg,

2005. Web.

[3] Sutner, Klaus, Teaching Professor and As

sociate Dean for Undergraduate Education,

School of Computer Science, Carnegie Mel

lon University.

[4] Bartholow BD, Henry EA, Lust SA, Saults

JS, Wood PK. Alcohol effects on perfor

mance monitoring and adjustment: affect

modulation and impairment of evaluative

cognitive control. J Abnorm Psychol. 2012

Feb;121(1):173-86.

0x5a0c3dfd5478db4ca01d4c5aa73475f4d95f8ec654d50242a9d4730a995bbdb3

Full track

Safety Schools of Thought

5 Tironiculum: Latin Speech Recognition via Latin Text-to-Speech Lee
Butterman

Keywords: Latin, Automatic speech recognition, AI, Machine Learning,
Abundant citations, Life advice, State of the

Art, Competition winner, Metagaming a competition

6 Abecedarial Acrostic, Alphabetized Amusingly Because Beings
Blissfully Cause Celebratory Centennials... (Note: Full Title is
Longer)

Jacob Weiner

Keywords: Records, Useless, Alphabet, Gibberish

7 On "Ra-men, Ra-men ramen ramen"

LAPP Lab

Keywords: language, ramen, space-time continuum

8 ACTION: A Catchy Title Is all yOu Need!

Bernhard Egger, Kevin Smith, Thomas O'Connell and Max Siegel Keywords:
catchy, title, all you need

9 A Deep Learning Approach for Deeply Inaccurate Wordle Solving Ahana
Deb and Sayan Goswami

Keywords: wordle, ordlew, rdlewo, dlewor, leword, ewordl

0xd365958785ba3fedfa5b18ed5cb62eaf5eb2bab3d25bf1fa11fae24eaa761f64

0x92f78e13fcb6ae166baa3d263f2b836e149797dd7b86cf4662c6800bc5f98a31

Reducing the Trusted Constituent Base with the LCF Approach

3

or

Hillary: The Next 700 Elections

Rose Bohrer

Carnegie Mellon University

Sol Boucher Jos Valdivia  Carnegie Mellon University Case Wallet, Inc.

rose.bohrer.cs@gmail.com sboucher@cmu.edu jos@choosecase.com

Abstract: ​In order to form a more perfect union, we address the
issue of election robustness.                             We introduce
the LCF (Logic of Congressional F*ckery) approach for minimizing the
TCB                           (Trusted Constituent Base) of an
election process. We evaluate our approach on the American
presidential election process and show that it compares
favorably with traditional approaches for
election robustness.

1. Introduction

Due to the finite length of the human lifespan, all forms of
government presently require a                                 method
of repopulating themselves. At present, the most popular method is
that of an                             election, an event in which
people called             constituents collectively decide on their
rulers with varying               levels of freedom. A singular
advantage of the Election Method is the illusion of agency granted
to the masses, which is widely considered
to be the most effective method of suppressing public
unrest. The great risk of the Election Method is that
is the issue of                             robustness***:** ​in most
implementations of the Election Method, there is a risk that the  
 *constituents        will elect incorrect leaders.
This had led to the proposal of many interesting election verification
methods, but this
is still an open problem with much work to be done.

2. Related Work

Every nation with an election system has faced this problem, and thus
the literature is vast. In
this section we outline methods used by various nations.

Definition 1: Trusted Constituent Base: ​We say that an
electoral process has a Trusted                   Constituent Base if
α is the fraction of voters that must be trusted to vote correctly to
achieve a                                       proper outcome. It has
been shown that systems with α \<= 0.01 can be verified in linear
time,                                     but verifying systems with α
> 0.01 is NP­Hard (it is unknown whether it is also in NP). Thus the
goal of verification technique
is to achieve α = 0.01. Failing that, lower α leads to more tractable

verification in practice, even when the problem remains NP­Hard in theory.  

1.1. United States

The United States, despite its immense wealth and power, has long
struggled to verify its                               election
processes. The verification methods currently used in the United
States are widely                           considered insufficient,
but are illustrative and form the foundations for more sophisticated  

0x9dcb84fdb8f58d94f42a18232bf121c42e225e5d4aed731a53d04d9121d3b27d

techniques:

First­Past­The­Post:                          A common building
block of election verification systems is to count votes in strange
ways that skew the distribution of power. The most basic method is the
First­Past­the­Post algorithm, which
exploits integrality issues. In a multi­position election, one
can easily justify absolute power to whichever contestant
achieves a plurality of votes. This                             method
alone achieves α = 0.50. At the time, FPTP was considered a heroic
breakthrough, but
has long since been pushed to its limits.

Amphibian Partitioning:                      This method,
pioneered by Gerald Mander, observes that an election can be
partitioned into                                 districts, where
each district is counted as an individual vote. In an optimal
partitioning, an election can be won with (arbitrarily close to) half
of all districts, each                               winning with half
of the available results, leading to α = 0.25. But this number belies
the true                                     power of the Partitioning
approach: in multi­position elections containing
minority constituents (those who, when adequately partitioned, have
a majority in no districts), can effectively reduce
the representation factor of a sub­constituency to 0.
However, optimizing representation factors
is outside the scope of this paper.

Weighted Partitioning:      In a straightforward extension of
Amphibian Partitioning, all districts are                 given a
fixed additional number of votes in order to strengthen the votes of
the least populous                                   districts. Since
votes in small districts are the more powerful, the verification
burden is reduced.                               By increasing the
number of votes uniformly across districts, a semblance of democracy
is                             maintained, minimizing risk of unrest.
In principle, this technique can achieve arbitrarily low
α­value. In practice, this method has a small effect on
α­value, because excessive use creates
some risk of public unrest. It is worth noting that, nevertheless,
this technique has successfully                             been used
to ensure the correctness of several previous presidential elections,
including the                           2000 election of George W.
Bush, widely considered one of the most difficult verification
projects in recent memory.

Indirection Escape Hatches: ​The Electoral College
includes an escape hatch by which the unified vote of a mere
270 unelected government drones overrides the will of the electorate.
Historically, numerous electors have
tried to use this mechanism, but have never coordinated
well enough to overturn an election. In principle this
method has the incredibly low α­value of
.0000001, but suffers from a greatly increased risk of political
unrest. And this begins to expose                                 an
underlying theme in election verification: Simply reducing the number
of individuals involved
is trivial. The difficulty lies in maintaining stability of government.

Higher­Order Indirection Escape Hatches: ​One approach for
reducing unrest is to target                 less­publicized but
equally­important elections. In a two­party system, general elections
are                       effectively useless: the entire political
race is decided during primary elections, whose conduct
is watched much less closely. Thus there exists an escape
hatch for primary elections in the
form of Superdelegates (higher­order delegates or HODs), which can
vote as they wish, with the                             same impact as
hundreds of thousands of people. In current implementations, this
approach

0xcc4ce819fd7906b880ccc147c5168d467eeb24d7683954f3599fa069585499e5

has α­values on the same order as Amphibian Partitioning (since only a
constant fraction of                               votes are assigned
to Superdelegates), but when the techniques are combined they can

achieve an α­value below .1 without causing noticeable unrest.

1.2. China

China has long used B­Trees to obtain incredibly low α­values. The
main insight of the Chinese                                 election
process is that the standard parliamentary system is a two­level
B­Tree with high                             branching factor, and
that the total number of trusted votes is equal to the number of
children at                                     the root. By removing
the 2­level restriction on the B­Tree, the Chinese system can result
in
arbitrarily low branching factors, and thus an arbitrarily­low constant number of trusted votes.

While many of the other α­reduction approaches mentioned in this paper
run into issues due to                               civil unrest, the
Chinese system seems surprisingly successful, due in large part to a  
long­standing communalist culture in which
many people [                         这里, Mandarin 1970] see no
need for personal agency in the political process as long the
resulting government achieves the
pragmatic goals they desire for the nation [Mandarin, Gerry  1956].

It appears that here the advantages are not in electoral tricks so
much as choice of cultural                                   values.
Recent work has attempted to modify the American election process by
importing                           sufficient numbers of Chinese
people [CMU Admissions, 2016], but it is unclear whether this
has had the intended effect.

1.3. Russia

Russia takes a completely different---and frankly somewhat
counterintuitive---approach to                 reducing the TCB:
reduce the trusted constituent base by increasing voter turnout. While
the                             >100% turnouts often observed in
their larger cities might initially suggest an increased α, we
observe that a careful implementation results in
the opposite effect. Consider that, by the
pigeonhole principle, an election that turns out
n more voters than actually exist must incorporate at least
n votes corresponding to constituents who have already voted.
We define                 the term     doppelganger          to
refer to such constituents. Given that a state, through its voter
registration process, is able to select which doppelgangers
to admit, a successful                       implementation of this  
superturnout          scheme will admit almost exclusively
trusted doppelgangers. We refer to the set of all trusted
doppelgangers as the                        doppelgang because each
of its members will vote in the same way; with such organization, it's
easy to show that a
doppelgang accounting for a p% increase in turnout directly reduces α by p/100.

1.4. North Korea

Eternal President Kim Il Sung started the Great Democratic People's
Leadership Verification                     Project in 1948, preceding
other founding verification projects such as AUTOMATH by several
decades. The prosperity of the Democratic People's
Republic has provided funding for the
Verification Project far exceeding that available in imperialist
nations, and thus enabling a

0x3ff7aea2ffe1e9b5aa08bae0b3b6a0760c12a5bf74ec63516f51665b57f07995

tremendous scope and leading to verification results of which the
imperialists are envious to this very day.

After an exploratory period of several years, the Verification Project
found focus in the philosophy of Juche, focused on a trinitarian
ideal based on the following principles

1. Proof automation (자주 or 自主)

2. Representation Independence (자립 or 自立)

3. Masturbation Defensive Design (자위 or 自衛)

This led to promising initial results. After the death of the Eternal
President, Eternal Secretary Kim Jong­Il added his military­first or
songun (선군 or 先軍) policy which supported a militant attitude to
the correctness of elections. Now a nationwide priority, Kim Jong­Il
built Kim Il­Sung Memorial Verification Centers in every school in
Choson. By verifying the process from birth, North Korea has achieved
an α­value of 0. However, it should be noted that our savage
imperialist nation is far too destitute to engage in such an
exhaustive verification program, and thus it is the goal of this paper
to achieve a fraction of the North Korean result at a more affordable
cost.

2. Approach

The LCF Method (Logic of Congressional F*ckery): The LCF method
is based on a fundamental observation: The tension between the desire
for a rich verification language and a small Trusted Constituent Base
is best resolved by defining powerful special­purpose constructs in
terms of extremely general base constructs.

In particular, the LCF uses a single building­block, that of
representative democracy. Our culture holds democracy sacred, and
thus the authors postulate that (a) any approach not based in
democracy is bound to produce unrest and (b) any approach that is
based on democracy has a leg up.

Our representative ​approach is based on our analysis of [Kim
48]'s Representation Independence approach. We know from experience
that Representation Independence (developing a culture in which
constituents do not care at all whether their interests are
represented by the government), while effective, is prohibitively
expensive. Since reducing cost is primary goal, we take a
representation­aware approach (constituents receive some form of
representation, and are made extremely aware of all representation
they receive, but we develop methods to prove that the available
representations do not interfere with correctness).

On top of the basic functionality of representative democracy, we
build the following tactics:

Pork­Barrelling: ​Pork­Barrelling is an awareness­based
tactic. In such a vast nation, it is difficult to be aware of every
political event across the nation, but quite feasible to be aware of

0x182e7df18b839436389c4946aaad717828495644f902700d0d9f92469d38cd96

local political events. This observation leads to the result that
election results depend only on a
local view of politics, formalized below.

Definition 2:​A congress is locally sound if each district's local political outlook is positive.
Definition 3:​ A congress is globally sound if every congressperson is elected correctly.

Theorem 1:​ All locally sound congresses are globally sound.

It is a well known fact in verification that reducing complex global
concerns to simple local                                 concerns
makes otherwise intractable problems feasible. Pork­barrelling works
by reducing the                       absolute number of contributing
factors in an individual election, making certain other
techniques more effective.

Curtain­closing: ​It was observed in our introduction that
partitioning schemes are vulnerable to                         public
unrest if used excessively. The main problem is the public attention
paid to the shape of                                   voting
districts and redistricting process. A main contribution of the work
is that closed­curtain
redistricting processes, by their very nature, prevent any change in public opinion:

**Theorem 2 (The Public Respects the Redistricting Committee):
 ** ​Public opinion is
independent of the redistricting action of a secret committee.

Proof Sketch​: Secret committees have existential type. It follows from Reynolds' Parametricity
Theorem that a voter cannot depend on implementation details of the committee, such as their
redistricting results. Qed.

3. Evaluation

We evaluated the LCF approach by implementing an electoral proof
assistant named Hillary.                           The Trusted
Constituent Base resides entirely in the Hillary/Purge segment of the
assistant,                           consisting only of approximately
8000 Washington DC residents. The vast majority of the code
base, used for practical election verification,
resides in the Hillary/HEIL framework
(Higher­Electoral Induction Logic). Using Hillary/HEIL we have
verified the results of several                         state
primaries with a short­term goal of a complete verification of the
Democratic presidential                         nomination, which
appears to be well­underway, largely because the unrest­abating
tactics such                         as Pork Barrelling allowed us to
greatly increase our usage of the existing Higher­Order

Indirection Escape Hatches     ​technique. Upon verifying the
nomination we wish as future work to
verify the general election, but we make no claims of that ability at this time.

Our collaborators are currently implementing a second proof assistant
in the LCF style called                           HEIL Light, whose
Trusted Constitution Base consists of only 400 constituents. However,
as of                             this writing they have verified only
local elections, and it is unclear whether anyone but a

supreme expert is capable of scaling their proof assistant to a general election.

0xfc9093631e80c59e4c4ccf5175114fd831a7421131b0ff66c2fa02a487591e6b

0x3c27057bfdac53902674f82cd1381fa0958a0c4d34374ff25fb40ba99094eff3

4

UNPRL: NUPRL PROOF RE-EVALUATION LOGIC

RYAN KAVANAGH

Abstract. he Unprl proof assistant is introduced. Unprl generalises
the Nuprl

proof assistant's client-server architecture, thereby increasing the
system's fault

tolerance. Unprl's proof generation system far surpasses the current
state of the

art in artiûcial intelligence, a fortiori surpassing the na¨ıve
proof search provided

by other proof assistants. Implementing Unprl is discussed.

1. Introduction

Proof assistants have become an important tool in the programming
language theorist's toolbox. Recently, they have found applications
beyond the study of formal systems and the formalisation of
mathematics. For example, they have been applied to verifying the
safety of cyber-physical systems [Pla10] and in creating veriûed so
ware toolchains [Con16]. hough we ûnd this trend encouraging, we
believe the diõculty and tedium associated with using proof assistants
impedes their widespread adoption. To allay these burdens, we propose
several improvements to the Nuprl proof assistant described in
[Con+85].

Nuprl is an in uential proof assistant originally developed in the
1980s and it is still under development today. Despite its longevity
and success, it suòers from using a peculiar closed-source
client-server architecture. A single server instance is known to exist
and is located at Cornell, and one gains access to it by e-mailing a
project member. hough this client-server paradigm may on the surface
appear unusual, it is perfectly reasonable: operating Nuprl utilises
scarce resources and is inherently Oz-like. Indeed, it is widely
believed¹that whenever a user connects to the server, an alarm goes
oò at Cornell and the ûrst author of the Nuprl book [Con+85]
(hereina er referred to as "the man behind the curtain") rushes to the
terminal in the server room. hen, as the remote user enters his
proofs, the man behind the curtain quickly checks them and informs the
user of their correctness. hough the mental prowess underlying Nuprl
is indisputable, the astute reader will immediately see the
unsustainability of the Nuprl architecture.

We introduce a new proof assistant called Unprl that generalises
Nuprl's client server-proof checker model, thereby building on the
strengths of Nuprl while address ing its aforementioned Achilles heel.
Moreover, Unprl provides a proof generation mechanism far surpassing
the state of the art in artiûcial intelligence, a fortiori

surpassing the na¨ıve proof search provided by other proof assistants.
We examine

2010 Mathematics Subject Classiûcation. Primary: 68T15; Secondary:
03B35, 03B70.

Key words and phrases. Proof assistant; Nuprl; he Wizard of Oz;
Artiûcial artiûcial intelligence. ¹Private communications at
POPL'16.

1

0xc1b8a9bf378ddfec338044d0809fd0eee49eddc72c232fd8df69630741691b5f

2 RYAN KAVANAGH

these improvements in section 2 and discuss several techniques that
may lead to performance increases in section 3. Implementation details
are discussed in section 4.

2. Work Distribution and Proof Generation

Rather than assume a single "man behind the curtain", Unprl
generalises Nuprl's client-server-proof checker model to support
multiple "people behind the curtain". In particular, we assume an odd
number of undergraduate students u₁, . . . , u_n *to be behind
the curtain (the readeris referred to Appendix A for assistance in
determining the parity of a given *n). Unprl's client-server-multiple
proof checkers architecture is depicted in Figure 1.

u₁

⋮

u_n

Unprl server Client

Figure 1. Unprl's client-server-multiple proof checkers architecture.

We now pass to study the beneûts of this simple and obvious
generalisation. hese beneûts are captured by Unprl's two main modes
of operation.

Unprl's main mode is its proof checking mode. In this mode, the
server idles until it receives a theorem statement T, a proposed
proof P for the theorem, and an acceptance threshold 0 ≤ A ≤ 1.
Upon their receipt, the Unprl server transmits a copy of T and P
to each student behind the curtain. Each student then either replies
to the server that they accept the proof, or they reject it and
provide the server with a proof of ¬T. If at least An students
accept the proof, then the server marks the proof as correct and
notiûes the client that P is a proof of T. Otherwise, there was
disagreement and we must re-evaluate the proof. We proceed by
breadth-ûrst search to reach consensus as follows. he existence of
disagreement implies the server received counter-proofs P₁, . . .
, P_s*for some *s ≥ 1. he server enqueues the triples (¬T,
P_i, A) for i = 1, . . . , s. We dequeue a triple (τ, π,
A) and reenter proof checking mode, checking theorem statement τ
with proof π and threshold A. If π is accepted for τ, we apply
double-negation elimination to τ to determine if we should accept
T. If we accept T, we inform the client that π*ˆ is a proof of
*T, where π*ˆ is *π plus any double-negation eliminations required
to transform π from a proof of τ to a proof of T. If we reject
T, we inform that π*ˆ is a proof of ¬*T, where π*ˆ is *π plus
any double-negation eliminations required to transform π from a
proof of τ to a proof of ¬T. Otherwise, we received counter-proofs
P^′₁, . . . , P^′_t*to *τ, so we enqueue the triples (¬τ,
P^′_i, A) and continue with our search. Upon termination, the
client will have a veriûed proof of either T or ¬T.

Unprl's second mode is its proof generation mode. In this mode, the
server idles until it receives a theorem statement T and acceptance
threshold 0 ≤ A ≤ 1. Upon

0x8043ee53b2fce0d7b78ce26dbddf1e3d75a0de5ee8e55f582cbbd02c9ca47a5e

UNPRL: NUPRL PROOF RE-EVALUATION LOGIC 3

receipt, the Unprl server switches into proof checking mode and
attempts to check the proof triple (T,true, A), where true
is any tautology or always provable sentence. When the proof checking
mode terminates, it will have returned a theorem-proof pair, providing
either a veriûed proof of T or a veriûed proof of ¬T. hese results
are conveyed to the client. he deluxe version of Unprl provides the
option to perform proof search by problem set, though the latency is
obviously increased.

3. Analysis and Incentivisation

hough a marked improvement on Nuprl, Unprl suòers from several
deûciencies that we address in this section.

3.1. Proof Checking Mode. hough Unprl's run-time bus factor can
be made arbi trarily large, its accuracy may not increase
correlatedly. Moreover, it is not possible in general to estimate the
likelihood that an arbitrary group U of undergraduate students
u_i accepts an incorrect proof. Indeed, assuming **U* is composed
predomi nantly of freshmen, the probability that the theorem statement
and proof pair given in Figure 2 is accepted is believed to be
arbitrarily close to 1, also independently of the acceptance threshold
speciûed. However, the theorem is clearly false of the classical reals
and the proof should have been rejected. hankfully, this does not mean
we should abandon Unprl. Indeed, if U is composed predominantly of
students having taken a course in analysis, the likelihood of the
proof pair being rejected is close to 1, independently of the
acceptance threshold speciûed. his example illustrates the diõculty in
quantifying the probability that proofs accepted by Unprl are correct.
However, we believe that this example demonstrates the need to ensure
that the *u_i be uniformly sampled from the undergraduate student
population.

To encourage "correct" results, we propose rewarding the proof
checkers when they provide "correct" responses.

We assume the client can allocate r > 0 reward resources²to
verifying k theorems using n undergraduates. For each theorem
T_i, i = 1, . . . , k, let c_{i j} *be the number of rounds
in which undergraduate *u_j's response to the server agreed with the
ûnal result. In other words, let c_{i j} *be the number of times
*u_j *accepted a proof of a *τ double negation equivalent to
T_i*if *T_i *was accepted or the number of times *u_j *accepted
a proof of a *τ double-negation equivalent to ¬*T_j*if *T_j *was
rejected. hen, at the end of the theorem proving session, each
undergraduate *u_j *receives

∑^k_i=1c_{i j}

∑^k_i=1 ∑ⁿ_j=1c_{i j}

of the reward r. Key to our strategy is that the reward received
corresponds to a fraction of all correct answers in the system, and so
the more a given undergraduate surpasses his peers, the greater his
reward. It is thus against the undergraduates' individual best
interests to collude and secretly agree to accept all proofs.

To further counteract any chance of collusion, we suggest running two
instances of Unprl in parallel, each receiving ^r₂resources. hen,
for each T_i, randomly assign

²Experience has shown food to be the most eòective form of reward.

0xb4d12da8ef450bd3a22ada05831538cf8c7323e3dcaea0ecee2346a32ec2b8f9

4 RYAN KAVANAGH

heorem 1. he set of (classical) reals R is a singleton set.

Proof. First observe ûrst that in N,

0 = 0²= (1 − 1)²= (1 + (−1))²= 1² + (−1)²= 1 + 1 = 2.

We proceed by induction on n to show that either n = 0 or n = 1.

Indeed, the base case is trivial, so assume the claim holds for

a given k and consider n = k + 1. By the induction hypothesis,

either k = 0 or k = 1. In the ûrst case, we have n = k+1 = 0+1
= 1,

and we're done. Otherwise, k = 1 and n = k + 1 = 1 + 1 = 2 = 0,

and we're done.

Now, consider the fractions 0 ∶=⁰₁and 1 ∶=¹₁. We wish
to show

that they are equivalent, written 0 ∼ 1. Observe that 0
∼²₂, since

0 ∗ 2 = 2 ∗ 1 (recall, 2 = 0). Moreover,²₂∼ 1, since 2 ∗ 1 = 1
∗ 2.

So by transitivity of ∼ (see [Lan09, heorem 39]), we have 0 ∼
1.

We now show that for any arbitrary fraction ^m_n,^m_n∼ 0.
By the

above, either m = 0 or m = 1. If m = 0, then*^m_n∼ **0*
because

m ∗ 1 = 0 = 0 ∗ n. In the second case, we must have either n = 0

or n = 1. If n = 1, then*^m_n∼ 1, because *m∗1 = 1∗1 =
1∗n, and so

by symmetry [Lan09, heorem 38] and transitivity of ∼, we have

m

_n∼ 0. Otherwise, we fall into the case of m = 1 and n = 0.
hen

by [Lan09, heorem 40], ^m_n∼^m_n×ⁿ_n=⁰_n. hen by
the above

0

_n∼ 0, and we're again done by transitivity. Following Landau

[Lan09, Deûnition 16], we thus conclude that there is a unique

rational number: the set of fractions equivalent to 0.

his implies that there is a unique Cauchy sequence of rational

numbers, namely the constant sequence of **0**s. But its limit with

respect to the standard metric is 0, and so the rationals are a

complete metric space. But R is deûned to be the completion

of Q, and so we conclude Q = R. But Q is a singleton set, so so

is R.

Figure 2. A proof freshmen dream about.

*T_i *to one and ¬*T_i *to the other, and withhold compensation
for the *T_i *on which the two instances disagree. Not knowing if
their instance received the true version of a theorem but knowing that
they must reach the same conclusion as the other instance, the
checkers will have no choice but to actually check the proof. Recent
advances in friendship logic appearing at this conference may shed
light on whether this overhead is truly necessary.

3.2. Proof Generation Mode. Given that the proof generation mode
is a special case of the proof checking mode, it is suõcient to adapt
the above incentivisation scheme. Suppose the client has*r* reward
resources to allocate and k theorems to prove. hen
allocate*^r₂resources to the incentivisation of the *k top-level
proof checking

0x17f7e02851f9161d97f5ac98ac11968f2d8a4fac0e0f045345702cba5e0e3272

UNPRL: NUPRL PROOF RE-EVALUATION LOGIC 5

calls. Additionally, reward each u_i *with^pi*

ûnal accepted proofs that *u_i *provided.

_2*k*of the reward, where *p_i*is the number of

4. Implementation

Implementation is le as an exercise for the reader. Readers are
especially encour aged to verify their implementation using Unprl.

5. Related Works

Many proof assistants have been introduced over the years, ranging
from Edin burgh LCF in 1979 [GMW79] to Nuprl [Con+85] to Coq
[he04]. hese have lead to remarkable achievements of veriûed
mathematics. For example, the Feit-hompson Odd Order heorem in Coq was
recently veriûed in Coq [Gon+13]. While not seek ing to diminish the
works on which Unprl builds, we believe Unprl is a signiûcant
improvement on its predecessors.

First, Unprl's architecture does not shackle the client to any given
set of axioms, assuming the axioms permit double-negation
elimination.³In other words, we provide clients with the freedom to
specify the axiomatic framework in which they wish to verify their
proofs and prove their theorems. Our legal counsel has urged us,
however, to caution users of Unprl against using the patented
axiomatic system underlying Estatis Inc.'s Falso HyperVeriûer
[Est].

Finally, we allay concerns that may have arisen following section 3
regarding the risk of accepting an incorrect proof. We believe that
this risk is no greater than the one inherent in other
state-of-the-art proof systems. For example, it is possible to prove
False in Coq 8.4.5 by exploiting a bug in the vm compute command when
there is a type with more than 255 constructors [DPC15]. Moreover,
we believe that the incentivisation scheme we proposed is suõcient to
counteract the risks.

Acknowledgements

he author gratefully acknowledges various insightful conversations on
the me chanics of Nuprl with Olivier Savary Be´langer and other
POPL'16 attendees.

Appendix A. Odd Integers

Determining the parity of integers is a diõcult task. However, as a
service to the reader, we provide the following functions. he function
returnTrueIfOdd, imple mented in Standard ML, returns true if applied
to an odd integer. As a supplement, the function returnTrueIfNotOdd,
also implemented in Standard ML, returns true if applied to an integer
that isn't odd. he author has formally veriûed that these functions
satisfy their speciûcations.

fun r e t u rnT r ue IfOd d ( n : i n t ) = t r u e

fun r e t u rnT r ue IfN otOd d ( n : i n t ) = t r u e

³A simple work-around to the (not not absurd) objections⁴to
double-negation elimination involves simply looping until a direct
proof to T accepted by An of the students is produced. ⁴hose who
object to double-negation elimination cannot be oòended by this
remark if they are at all consistent.

0xe247c767316b8d151a66230cbfbe06206528364b51b60e4aaa3b58f76bb092ad

6 RYAN KAVANAGH

References

[Con+85] R. L. Constable et al. Implementing Mathematics with he
Nuprl Proof Development System. Prentice-Hall, 1985.

[Con16] DeepSpec Consortium. DeepSpec: he Science of Deep
Speciûcation. http://deepspec.org/. 2016.

[DPC15] Maxime De´ne`s, Pierre-Marie Ped´ rot and Guillaume Claret.
clarus/falso: A proof of false. 2015. url:
https://github.com/clarus/falso. [Est] EstatisInc. Falso HyperVeriûer
and HyperProver. url: http://inutile. club/estatis/falso/.

[GMW79] Michael J. Gordon, Arthur J. Milner and Christopher P.
Wadsworth. Edinburgh LCF. Vol. 78. Lecture Notes in Computer Science.
Berlin, Heidelberg: Springer Berlin Heidelberg, 1979. isbn:
978-3-540-09724-2. doi: 10.1007/3-540-09724-4.

[Gon+13] Georges Gonthier et al. 'A machine-checked proof of the odd
order the orem'. In: Lecture Notes in Computer Science (including
subseries Lecture Notes in Artiûcial Intelligence and Lecture Notes in
Bioinformatics) 7998 LNCS (2013), pp. 163--179. issn: 03029743. doi:
10.1007/978-3-642- 39634-2_14.

[Lan09] Edmund Landau. Foundations of Analysis. Trans. from the
German by F. Steinhardt. 3^rd ed. Reprint of the 1966 edition.
Providence, Rhode Island: AMS Chelsea Publishing, 2009. isbn:
0-8218-2693-X.

[Pla10] Andre´ Platzer. Logical Analysis of Hybrid Systems: Proving
heorems for Complex Dynamics. Heidelberg: Springer, 2010. isbn:
978-3-642-14508-7. doi: 10.1007/978-3-642-14509-4.

[he04] he Coq development team. he Coq proof assistant reference
manual. Version 8.0. LogiCal Project. 2004. url: http://coq.inria.fr.
E-mail address: rkavanagh@cs.cmu.edu

Computer Science Department, Carnegie Mellon University, Pittsburgh, PA
15213-3891
0xe371bfdf833aec58b25850d245f77b5958a00d420c9aeae51179a315d4f82ede

5

Type-Safe Friends Will Never

Hurt You

Rose Bohrer

Carnegie Mellon University

1 Introduction

In recent years, the activity commonly known as "friendship" has
undergone a precipitous rise in popularity, with recent census numbers
suggesting that almost 1 in 3 Americans has friends. As documented in
the extensive literature, friendship carries with it a plethora of
dangers beginning unpaid lunch debts and culminating in eventual
death, even including in some cases situational comedy [2].

Despite extensive efforts to curb this deadly activity, friendship
rises across the US and across the world. In an acknowledgement that
friendship cannot merely be proscribed by stuffy academics, this
stuffy academic applies a formal verification methodology to rule out
dangerous friendships while allowing benign friendships to survive.

2 A Taxonomy of Friendships

In order to develop a practical logic for the verification of
friendships, one must first categorize the friendships that occur in
everyday life. While she is ashamed to admit it, due to the
much-maligned American "friendship culture", the author has found
herself in a number of so-called friendships. So many, in fact, that
one may even call her a "friendxpert". Such a friendxpert, in fact,
that she can tell you inventing such words only increases your chances
of being accidentally friended. Such are the risks of science.

The most basic ontology consists of Good Friends, Bad Friends,
Facebook Friends, and *γ−*Friends.

2.1 Good Friends

The best-known and most prized friend is the Good Friend, and a
primary goal of friendship research is the identification and
preservation of Good Friends. Extensive anecdotal evidence shows the
author is a Good Friend. Examples of Good Friend activities include:

• Providing camaraderie at social events in proportion to the
quantity of alcohol provided.

• Not interrupting others with questions about homework when I can
tell they're trying to focus on research.

1

0x55f60d32fcb2c3530007011f94951d1464756a1f5b65f4a1c23f9305de965b2d

• Looking the other way when undesired guests are invited into
shared work ing spaces at 3am right in the middle of working hours.

• Ordering a pizza for the whole office and not complaining when
others forget to pay their share

• Providing emotional support for common problems like lack of
confidence in one's work, no matter how esoteric and detached from
reality.

• Selflessly sharing whiteboard markers even with people who insist
on rub bing their greasy monkey paws all over the whiteboard instead
of using the eraser like the thumb-opposing human they are.

2.2 Bad Friends

Bad Friends, while nearly as common as Good Friends, are thoroughly
despised and are to be avoided at all cost. Despite the numerous
benefits of avoiding Bad Friends, prior works have unilaterally failed
to do so. The author has much experience with Bad Friends, whose
properties include:

• Monopolizing every writing surface within a 10-office radius.

• Using valuable working space as storage for oversized animatronic
skulls. • Treating the office minifridge like their personal
minibar.

• Tyranically vetoing all reasonable efforts to acquire matching
"Office mates for life" tattoos.

Such a list could fill several PhD theses, and in fact is the subject
of theses by such luminaries as [9] and [5]. For brevity we give
only the short list above, even though we could say much, much more.

2.3 Facebook Friends

The limited expressive power of strong friendship models led to the
development of weak friendship models, starting with the foundational
development of partial friendship spaces by [1] and made practical
by the introduction of face-oriented social indexing in [12] for
which this style of friend is named.

Facebook Friends have numerous useful properties and practical applica
tions:

• Minimal runtime cost, with hundreds of Facebook Friends often
costing less than an individual Good Friend

• Enabling work-efficient work-stealing work-avoiding algorithms •
Weak bisimulation with Good Friends

• Constant-time stalking of unrealistic γ-friends (see below)

2

0x84e37e78a673f17fe859ff75ac2c9bf40ab3573e8d23c0b22aefe4322ccefd22

∆ ` φ valid ∆; Γ ` φ true

∆; · ` φ true ∆ ` φ valid

∆ ` φ true Γ ` ψ true ∆; Γ ` φ ⊗ ψ true

∆ ` ψ ⊗ ψ<sup>0</sup>*true Γ, u* : ψ, w : *ψ<sup>0</sup> ` ψ ⊗ ψ⁰*true

∆; Γ ` φ valid

x : γ-Friend ( ♦!x (¬*Give-Up *I U)

(In-Office Evan) ( ¬(Sound Evan)

Figure 1: Selected Rules and Axioms

Furthermore, due to their extensive knowledge of Facebook Walls, the
Face book Friends are being considered for important applications in
national secu rity [3].

2.4 γ-Friends

The most dangerous friend is the γ-friend. The γ-friend is a
generalization of the classical concepts of boyfriend and girlfriend.
The γ-friend is an incredibly general concept which can encode
esoteric genders including: dragon, code, space, squid, dog, cat,
demon, angel, mermaid, lycanthrope, celestial, vampire, pumpkin and
even ceiling fan [6].

The sheer generality of this relationship makes it of great interests
to aca demics, yet analysis of γ-Friends has long been considered
the holy grail of Friendship Theory, being the subject of a plurality
of publications in the BMG, EMI, Universal and Warner conferences,
including a majority of Grammy win ners. Despite such an exhaustive
literature, little inroads have been made, as outlined in the
retrospective "What is Love?" [4].

The author must concede she is no expert in this branch of Friendship
Theory, though she has heard extensive rumors that such friendships
exist.

3 Modal Linear Friendship Logical Framework

In the present work we focus on the analysis of Good Friends and Bad
Friends. The examples given in the previous section have a common
theme of reasoning about situations involving change, possibility and
certainty, but are otherwise quite varied. For this reason our logic
extends previous dual-intuitionistic linear

logics with modal operators φ and ♦φ which say a formula φ holds
in all or in some future world, respectively. To ensure sufficient
generality we take a logical framework approach, where new
propositions and axioms can be introduced as needed.

3

0xe1f0dd0a655917d466ff4e85cbfc29da284ae11f30aa020748c9974d25ef938f

4 Case Study: Office Relations

A common friendship scenario is that of the graduate school office
mates. The many hours spent in the office each day make the office
mate bond one of great importance, but due to the randomness inherent
in the process, the risk of a Bad Friend is alarmingly high. In this
section we use MLFLF to verify the safety of one student and the
unsafety of their office mate.

In the first scenario we verify a common safety property: Paying debts
that are owed. We assume the following axioms:

A1: (Owes P N ( Pays P N) ( Safe P

A2: ♦Spins ( ♦P ( P

A3: Spins ( P ( ♦P

A4 : ♦Paid Rose 10

A5: Owes P N ( N = 10

A6: Spins

A7: Paid Rose 10 ( Pays Rose 10

For our second scenario we prove a common unsafety property: Theft of
valuables, under the axioms

A1 : (Friend-Of A B ⊗ Owns A X ⊗ Takes B X) ( Unsafe B

A2 : (Owns A X ⊗ On Y X) ( Owns A Y

A3 : Friend-Of Rose B ( Takes B X

A4 : On Paper Table

A5 : Owns Rose Table

A6 : Friend-Of Rose Evan

4

0xa15f00c976f2c063634cd973f13a3a10fef6b39d1b271989c9320d6a230f30fb

A4

♦Paid Rose

A6

Spins

A2

Spins, ♦Paid Rose ` Paid Rose ♦Paid Rose ` Paid Rose

A5

A7

Paid Rose ` Pays Rose 10

Paid Rose

Paid Rose , Owes Rose N ` N = 10

Paid Rose , Owes Rose 10 ` Pays Rose 10

Paid Rose

A1

5

Paid Rose , Owes Rose N ` Pays Rose N

Owes P N ` Pays P N

Owes P N ( Pays P N

(Owes P N ( Pays P N)

Safe Rose

Proof 1: A Safe Friend

A6

Friend-Of Rose Evan

A5 A4 A2

Owns Rose Paper

A3 A6

Takes Evan Paper

Friend-Of Rose Evan ⊗ Owns Rose Paper ⊗ Takes Evan Paper

A1

Unsafe Evan

Proof 2: A Unsafe Friend

0xb6836b960d22ce4d3703dda63d3456fdca94292f5e20f04a300fdb607a49d3a7

5 Formalization

We have developed an extensive formalization of the MLFLF framework in
the linear logic proof assistant Cwelf, available upon request. We
show the soundness of all inference rules and validity of all axioms
presented in this paper, along with many more, as well as all of our
examples. Further case studies for friendship logic formalized in
Cwelf will be presented in follow-up paper.

Building on the successes of MLFLF, we show that Cwelf itself is sound
from within Cwelf, following in the footsteps of [8].

6 Future Directions

While this work has developed an effective framework for the
verification of Good and Bad friends, it can say little about Facebook
Friends and even less about γ-Friends. We wish to address these
limitations in future works. Because many properties of Facebook
Friends seem to involve evaluation cost, we wish to develop a cost
semantics for friendship. In order to tackle the complexity of γ
Friends, we wish to employ automation in the form of linear logical
frameworks.

Before you can love another, you must love your Celf.

--- Chris Martens

Furthermore, while it is extremely useful to verify whether friends
are safe, this provides us little recourse in the all-to-common case
where a friend is, in fact, not safe. Therefore we wish to build upon
our experience in friend verifica tion to perform friendship
synthesis: the automatic generation of provably-safe friends from a
formal specification.

7 Related Work

To our knowledge, the only other attempt at formal verification of
friendship properties is the set-theoretic approach taken in "You've
Got a Friend in Me" [7]. However, this approach has never been
formalized and does not express state as easily as our linear-logical
approach does.

The complexity of friendship has been studied more extensively than
formal verification. In particular, it has been shown that friendship
can be detected in O(n²) time with high probability in some
important special cases [11]. Hard ness results have been show for a
number of key friendship problems: Most famously it was shown that
optimizing the size of social networks is NP-hard by a reduction from
the max-clique problem [10].

6

0x0996a581ce070f846a62251ef5d10afc4b4a70dcd37b40ea7713b844bdc3e224

References

[1] Tom Anderson. Whose Space is it Anyway? - Friendship Spaces Are
Just Octonion Lattices. MySpace, Inc., 2003.

[2] Jennifer Aniston. F.R.I.E.N.D.S. ACM SIGPLAN Notices, 1994.

[3] Donald Drumpf feat. Oasis. Making America Great Again: The
Wonder wall Approach. The Campaign Trail, 2016.

[4] Alexander Nestor Haddaway and Ligia Nestor. What is Love (and
Why Can't We Model-Check it?). The Album, 1993.

[5] Robert Harper and Alanis Morrisette. Compiling Polymorphism
Using Intensional Type Analysis. In Proceedings of the 22^nd ACM
SIGPLAN SIGACT Symposium on Principles of Programming Languages, POPL
'95, pages 130--141, New York, NY, USA, 1995. ACM.

[6] David Karp and Michael Rabin. Gender Identification is
NP-Complete. Theoretical Gender Studies, 2016.

[7] Buzz Lightyear and Randy Newman. You've Got a Friend in Me.
Toys and Their Stories, 1996.

[8] Chris Martens and Karl Crary. LF in LF: Mechanizing the
Metatheories of LF in Twelf. In Proceedings of the Seventh
International Workshop on Logical Frameworks and Meta-languages,
Theory and Practice, LFMTP '12, pages 23--32, New York, NY, USA,
2012. ACM.

[9] Taylor Swift. Picture To Burn. Sound Emporium, 2006.

[10] Kanye West and Jay Z. Clique. Summers and their Cruelty,
2012.

[11] Jack White and Meg White. We're Going To Be Friends (in Due
Polytime). White Blood Cells, 2002.

[12] Mark Zuckerberg. Factoring N-Dimensional Friendship Spaces with
Faces. Facebook, Inc., 2004.

7

0x021c60530cbc7e7ee7adfffafdec6c057e0bb62352befea46fd8e3dc5ab62f28

CONFIDENTIAL COMMITTEE MATERIALS

SIGBOVIK 2016 Paper Review

Paper 9: Type-Safe Friends Will

Never Hurt You

Stefan Muller, 563 Facebook friends

_Rating:):

Confidence: π

This paper aims to solve the long-standing problem of type theory
nerds not having friends, by means of a modal logic for friendship
verification. This intuitively seems like the right way to go about
making friends, so the committee was initially very excited by this
submission.

Unfortunately, the submission failed to live up to its promise. There
are many errors in the two provided proofs, and clear typos in the
provided axioms. One wonders whether the author should have spent more
time checking the submission and less time out with friends. As an
example, the variable X in axiom A3 of the second proof is unbound
and can be instantiated with anything, leading to the very suspicious
axiom that being friends with Brandon requires taking all of his
stuff. This seems like a strange condition for friendship. The Program
Committee's expertise on the subject of friendship is admittedly
limited, so we consulted an anonymous external reviewer who had the
following to add:

Ugh, I can't work when Brandon's in the office. He spends all of his
time writing meaningless inference rules about friendship on the
board, and if I try to use any of the board space, he yells something
about me being a bad friend. He keeps ordering pizza and hinting that
we should chip in even though no one else is hungry. Oh, also he keeps
insisting that my desk is his and putting his stuff there, and when I
take some of his papers off of my desk and move them to his desk, he
accuses me of stealing his stuff.

Given our initial evaluation of the paper and the external feedback,
the committee is forced to take the unusual step of deciding that the
author is a Bad Friend. If the errors are fixed, this might be a
decent submission for some other venue, but a prestigious conference
like SIGBOVIK can't accept submissions from Bad Friends.

0xa253258f485a8b431e4645dbf03a7c8ec8a6341b729e7045422192a1b60c2dd1

Rototiller track

Overcomplexity Theory

10 Edward, edMUnD & Edwin: Line-Based Text Editing for the 21^st
Century Natalia Posting and Katie Wolfe

Keywords: line-based text editing, line-cringe text editing, synergy

11 A Free Computer Vision Lesson for Car Manufacturers or It is Time
to Retire the Erlk¨onig

Maximilian Weiherer and Bernhard Egger

Keywords: awesome paper, great work, mind blowing results 12 Redundant
Coupling

Peter Kos

Keywords: software engineering, coupling, cohesion, rust, martin
fowler, fowler, james gosling, donald knuth

0x248fd1aa778f4c65964afe5512748fe503a3d796ec35721e3fb68c0a7063dff5

0x98fe52fcbbf8b596a644479d9757c77d7f81aed9db05a254d0951fe137a296bb

6

The Computational Complexity of Chinese and Italian

Noodle Making

Daniel M. Berry¹and Luisa Mich²

¹ Cheriton School of Computer Science, University of Waterloo

Waterloo, ON, N2L 3G1 Canada

dberry@uwaterloo.ca

² Department of Industrial Engineering, University of Trento

I-38122 Trento, Italy

luisa.mich@unitn.it

Abstract. This paper describes several traditional algorithms for
making Chi

nese and Italian noodles and classifies each according to its
computational com

plexity. It examines machines for doing each algorithm. It cites a
world speed

record for making a large number of noodles using the algorithm with
the max

imal complexity. It dissects mysteries about the legend that Marco
Polo brought

the technology of making noodles to Italy from China. It determines
that both

Chinese and Italian ways of eating food can be applied to both Chinese
and Ital

ian noodle dishes. It compares the power of the algorithms. It
considers the nature

of variations of the traditional algorithms. It concludes by
mentioning avenues for

further studies.

1 Introduction

Each of the Chinese and the Italians make and eat a large variety of
dough-based prod ucts of various sizes and shapes. This paper uses
"noodle" as general term to name a single unit of any product of this
type regardless of its national origin and regard less of its size and
shape³. The Chinese call their noodles "mian ti ` ao" ( ´ <sup>⾯条</sup>)
or just "mian", and the Italians call their noodles "pasta".
Therefore, this paper uses "mi ` an" ` and "pasta" when talking
about Chinese noodles and Italian noodles, respectively. Note that
"mian" and "pasta" are collective nouns that denote collections of
noodles. Thus, ` this paper needs to use "strand", perhaps prefixed
by "mian" or "pasta" as an adjective, ` when talking about one
unit<sup>4</sup> of mian or pasta. `

This paper presents one key algorithm from each of China and Italy to
make the

country's most traditional kind of noodles from already made dough of
the proper com position for what is being made. Later, it presents
some other algorithms, again from

³ Admittedly, the term "noodle" connotes a string-like product,
e.g., spaghetti. Nevertheless, even though many such products are
string like, the term is generalized in this paper to include

even short products, e.g., maccheroni or macaroni, and even shaped
products, e.g., farfalle or

bowties.

⁴Just as with "noodle", the term "strand" is used used even when the
unit is shaped differently from or is shorter than what is normally
called a strand or noodle.

0x4810563306d53762d29d978acc1163798b9d4b35d23490b7d1cffa582b3e9675

2 Daniel M. Berry and Luisa Mich

China and Italy, for making other kinds of noodles. Each algorithm is
characterized by its computational complexity, as a function of the
number, n, of noodles produced. There are actually two complexity
measures, the local complexity and the global com plexity.

The local complexity is for time required for the algorithm to make
one batch of noodles. Generally, the number of noodles that can be
made in one batch is limited by a combination of the resources
available and the physical properties of the noodle dough. The
resource limits that come into play include the amount of flour that
can be handled conveniently by the noodle maker, the amount of dough
that can be worked on by the noodle-maker's rolling pin, the amount of
dough that can be fed at once through a flattening device's rollers,
the amount of flattened dough that fits on the noodle-mak ing table,
and the amount of flattened dough that can be fed at once through a
cutting device. The main physical property of the noodle dough that
comes into play is that a noodle with too small a cross section tends
to break as it is stretched.

The global complexity is for the time required to make, with
successive applications of the algorithm, enough batches to yield all
the noodles needed for an occasion. Of course, in a home or in a
restaurant that makes noodles to order, usually one batch suffices. In
any, case, the global complexity is always linear in the number of
noodles produced, on the assumption that any algorithm requires about
the same amount of time every time it is used to make the same-sized
batch of one kind of noodles. Therefore, for each algorithm, only its
local complexity is given.

2 Traditional Chinese Mian Algorithm `

It appears that the signature variety of mian in China is the
hand-pulled variety known ` as la mi ¯ an, which originated in and
around Lan Zhou, the largest city in the Gansu ` Province of
Northwest China. La mi ¯ an is made by starting with a single strand
of dough ` and repeatedly stretching and folding it to produce a
large number of thin strands, the diameter of the final strands
depending on the diameter of the single initial strand and the number
of folds.

1. The la mi ¯ an maker takes a previously prepared tube of very
flexible dough of di- ` ameter D and of length L. (L needs to
be no longer than the distance across the la¯ mian maker's two
outstretched arms, and ` D needs to be no bigger than what the la
mi ¯ an maker can grip with one closed hand.) Call this tube of dough
"the ` initial bundle".

$a$ He⁵ dusts the bundle with flour.

$b$ He folds the bundle in half and pinches each end,

-- in one case, to merge two ends into one, and

-- in the other case, to make an end out of a fold.

The bundle is now of length ^L₂.

$c$ By twirling the new bundle like a jump rope, he stretches the
new bundle back out to the original length, L.

⁵ We use "he" as a singular pronoun to reference a noodle maker of
any gender.

0x5ab7e423ded22b4d7517c0d5ca3b3fdc83a9573a0ec1d562bbacb9b02b6cd078

Computational Complexity of Noodles 3

$d$ The result is a new bundle with twice the number of strands as
the previous bundle, and the diameter of each strand in the new bundle
is ^*√*1₂times the diameter of each strand in the previous bundle.

These steps are repeated until the strands are of the desired
diameter.

2. The la mi ¯ an maker trims off the ends to leave strands of length
` 0*.9 *× L. Then, the la mi ¯ an maker lays out the bundle of
strands on the table and, in one swift cut ` perpendicular to the
long axis of the strands, cuts all strands to leave two bundles of
strands of length 0*.45 *× L.

For a video showing a Chinese chef making la mi ¯ an, see `

https://www.youtube.com/watch?v=PHoQN9vQwHE,

particularly the last minute and a half.

On the assumptions that D is 1 inch, that L is 1 meter⁶, and
that the final mian are ` 1

₁₆ inch (≈ 1*.*59 mm) in diameter, there are 8 folding and
stretching steps, producing 256 trimmed strands each of length 90
centimeters. Then, the final cutting step produces 512 mian, each of
length ` 45 centimeters.

The local complexity of this traditional Chinese mian making method is
` log<sub>2</sub> n to make n = 2*<sup>m</sup>* mian in ` m − 1
folding-and-stretching steps and 1 trimming-and-cutting step⁷.

3 Traditional Italian Pasta Algorithm

An Italian pasta maker rolls out a ball of the proper dough into a
rectangular sheet of the desired thickness T and the desired length
on one edge, hereinafter called edge L (for "length"). An edge that
is perpendicular to L is called edge W (for "width"). (L and W
need to be small enough for an L×W sheet of dough to be easily
worked on by a hand-operated rolling pin.) Both sides of the sheet are
then thoroughly dusted so that they are not sticky. The sheet is then
rolled up very loosely perpendicular to L so that the resulting tube
is of length equal to that of W. The pasta maker decides the type of
pasta that is being made to determine the width w of one strand.
Ideally, the width W of the sheet is divisible integrally, n
times, by w. For fettuccine, w is smaller than for lasagne.

1. The pasta maker uses a knife to cut away a section of the tube of
width w. 2. The pasta maker unrolls the section into a strand of
width w and of length equal to that of L.

This cutting and unrolling of sections is performed n − 1 times and
then the remaining section is unrolled to produce the last strand of a
total of n strands. All of this cutting and unrolling must be done
quickly to prevent the rolled up tube from sticking to itself.

⁶ The reason that the diameter is in inches while the length and
other dimensions are in meters is that it is easier to describe the
effect of halving the diameter in terms of binary fractions of an
inch.

⁷ We are assuming that trimming and cutting take about the same
amount of time as does folding and stretching.

0x16cd04bb90f023a15097ec066932a987da0dd7e1f5963c0aaa23f152e44f485e

4 Daniel M. Berry and Luisa Mich

So, if one is making 30-centimeter long fettuccine whose cross section
is ¹₄inch by ₁₆ inch. Then, w must be ¹₄inch, T must be
¹₁₆ inch, L must be 30 centimeters, and

1

W can be anything that is less than the length of the pasta maker's
rolling pin and is a multiple of w. Let's assume that W is 8 inches.
Then from one 8 inch by 30 centimeter sheet, the pasta maker will need 8
× 4 − 1 = 31 cuts to make 32 strands. For wider pasta, such as
lasagne, fewer cuts are needed.

For a video showing making fresh pasta mostly by hand, see

https://www.youtube.com/watch?v=-lMmUf2nqYA.

The pasta maker in this video is using a machine to speed up the making
of the sheet, but is then doing the rolling, cutting, and unrolling by
hand.

The local complexity of the algorithm is linear in the number of
strands, n, made from n − 1 cuts and n unrollings in one sheet of
dough.

There are at least two devices that allow cutting a prepared sheet of
dough into a lot of strands in one step:

-- a pasta cutter rolling pin whose cutting ribs are spaced w apart
and

-- a pasta making machine whose cutting blades are spaced w apart.

With either of these devices, there is no need to roll up the sheet and
cut away one strand at a time. Instead,

-- the cutting rolling pin is rolled once over the flat sheet of
prepared dough, leaving the strands flat on the table with no need to
unroll, or

-- the sheet is fed through the machine, and the strands come out of the
machine already unrolled.

Several cutter rolling pins with ribs spaced different distances apart
can be seen at https://www.casalinghivenditaonline.it/en/kitchen/

cut-the-dough/beechwood-spaghetti-cutter.html.

For a video showing making fresh pasta with a machine, see

https://www.youtube.com/watch?v=IOsnlFcO748.

The algorithm embodied by each of these devices can be described as a
parallel, vector processing algorithm. Thus, the local complexity of the
algorithm to make n strands from one prepared sheet with either of
these devices is constant. That is, all n strands are made at the same
time, in the time required to roll the cutting pin over the sheet or to
feed the sheet though the machine.

4 World Record Setting Chinese La Mi ¯ an Maker `

In "How to make noodles", found at

http://www.scientificpsychic.com/mind/noodles.html,

one paragraph describes the video found at

https://www.youtube.com/watch?feature=player_embedded& v=auhHl5-6VdY:

This video shows chef Kin Jing Mark making Chinese hand-pulled noo

dles. He held the Guinness World Record as the fastest human noodle
maker 0x9f761bfa0cb801c374fe31687dc9668e50c8830b0b296a8b8370e2912339de2d

Computational Complexity of Noodles 5

for several consecutive years. His last record was set in 1993 on
NBC's after noon talk show, Vicki, when he stretched out 4*,* 096
strings of Chinese noodles by hand in 41*.*34 seconds. The fine
noodles are called dragon beard noodles (longxu mian).

The number, 4096, of strands that Kin Jing Mark made, is telling; 4096
= 2¹². It is clear that no one sat there counting the individual
strands to arrive at 4096. It is equally clear that the number of
folds was counted and that number was used as the exponent of 2 to
calculate the number of strands. Thus on average, Kin Jing Mark did
one fold and stretch every 3*.*445 seconds. Wow! Clearly, the cook and
the people who made the video understand the exponential growth of the
number of strands in the algorithm.

5 Automation of Algorithms

There are machines that automate the Italian pasta-making process. For
example, the Italian company Italgi makes some industrial strength
pasta sheeters and cutters that can be seen at

http://www.italgi.it/e-pasta-sheeters.htm.

Also Arcobaleno makes pasta sheeters and cutters that can be seen at

http://arcobalenollc.com/pastaequipment.html.

These machines simulate the human pasta maker's behavior, to make
so-called perfectly formed pasta every time.

There does not appear to be any machines that automate the making of
Chinese la¯ mian. There are machines that automate the mixing and
kneading of the dough, but there ` do not appear to be any machines
that automate the folding and stretching<sup>8</sup>. Perhaps the main reason
that la mi ¯ an are called in English "hand-pulled" is that they `
must be made by a human's hand.

6 Other Methods of Making Noodles

China does have other methods of making mian [1, 2]: `

-- Cut (qie): A sheet of dough is cut into strands of the desired
width, as in the tradi- ¯ tional Italian pasta algorithm of Section 3.
The local complexity of this process is linear in the number of
strands produced.

-- Squared (pian); As one is making cut mi ` an, directly above an
open pot of boiling ` water, each (long) strand is torn by hand into
square-sized pieces (short strands). The local complexity of this
process is linear in the number, n, of pieces produced: If s long
strands are produced with s − 1 cuts, and from each long strand are
pro duced p short strands with p − 1 tears, then s × p = n.
The total number of steps is (s − 1) + (s − 1) × (p − 1) = (s
− 1) × p, which is approximately s × p = n.

⁸ The closest we were able to find were the machines by Yamato
Noodle that make ramen, udon, and soba, all Japanese noodles. However,
as shown at

http://www.yamatonoodle.com/noodle_machine/,

after preparing the dough, these machines cut the noodles off.

0xa7542fa80f1d569dbd3861c81b0d5484057b312e7514f9305cb393274d153eaf

6 Daniel M. Berry and Luisa Mich

-- Extruded (jˇıya): Dough is pushed through a die with holes of the
desired shape ¯ to form strands, one per hole in the die. The local
complexity of this process is constant, since all the strands are
produced at the same time.

-- Kneaded (rou): A small ball of dough is worked on a flat surface to
form it into ´ a strand of the desired shape. The local complexity of
this process is linear in the number of strands produced.

Also Italy has other methods of making pasta [3, 4]:

-- Short cut: As one is following the traditional Italian pasta
algorithm of Section 3, the s unrolled (long) strands are laid out
in parallel, side-by-side into a striped sheet. Then, p − 1 equally
spaced cuts perpendicular to the axis of the length of the strands are
applied across the whole sheet, to produce s × p = n rectangular
pieces (short strands). The local complexity of this process is in the
order of the square root of the number of pieces produced: The
complexity analysis for this process starts as for the production of
n = s × p squared pian. The difference is that all ` s long
strands are cut together in only p − 1 cuts. Thus, the total number
of cuts is s − 1 + p − 1, which is approximately s + p. If the
sheet is close to being a square,
_{then s ≈ p, and s+p ≈ 2}^√n, since s×p = n. In a
complexity estimate, a constant _{multiplier of} ^√n can be
ignored, because the main contributor to the growth of
₂^√_{n is} ^√n, and not the constant multiplier.

There is a variation of the pasta cutter rolling pin, mentioned in
Section 3, that has cutting ribs running along the long axis of the
pin, perpendicular to the strand cutting ribs. This variation is for
producing a whole sheet's worth of short-cut pasta in one roll of the
pin over a prepared sheet of dough. The local complexity of this
method of making short-cut pasta is constant.

-- Extrusion: Dough is pushed through a die with holes of the desired
shape to form strands, one per hole in the die. The local complexity
of this process is constant, since all the strands are produced at the
same time.

-- Short-cut extrusion: Each extruded pasta long strand is cut
perpendicular to the length of the strand into short pieces. The local
complexity of this process is in the order of the square root of the
number of pieces produced, by the same analysis as for the above
short-cut pasta.

Additional shaping may be applied to the pasta produced by any of the
described meth ods.

There are machines that automate all the various ways of making
Italian pasta, as shown at

http://arcobalenollc.com/pastaequipment.html.

7 Mystery

While China does have cut mian, resembling Italy's traditional cut
pasta, it appears from ` a thorough search of the Web, that Italy
does not have anything resembling la mi ¯ an that ` is made with a
repeated-folding-and-stretching method.

0x10cdece301da6b143f108588051b9b774c1ab03965c4cccff4610b346e2a2b2a

Computational Complexity of Noodles 7

Legend has it that Marco Polo brought noodles to Italy when he
returned to his native Italy from his lengthy visit to China [1, 5]
although there is some doubt. If this legend is true, then why do the
Italians not make their pasta the same way the Chinese do? One
possible and plausible explanation is that Polo brought back
necessarily well dried samples of actual mian rather than the
algorithm. Polo told the Italians to soften ` these dried mian by
cooking them a few minutes in boiling water. After the Italians `
decided that they liked the results, they proceeded to figure out a
way to produce the product that Polo had brought back and came up with
the algorithm described in Sec tion 3 and never even thought of the
original algorithm described in Section 2. This is not the first time
an attempt was made to reproduce a product by reverse engineering from
instances of the final product rather using the original algorithm
[6]. Such reverse engineering does not always succeed in duplicating
the original product, and occasion ally ends up inventing a new
product that is different from the original in subtle or not so subtle
ways. Pasta and Chinese mian` are different to the discerning
palate, and each is good in its own right, even to connoisseurs of the
other.

On the other hand, maybe the legend is false, and each country
invented its own kinds of noodles and stumbled on to its own methods
with no knowledge of the other's kinds and methods.

8 Different Methods of Eating

Chinese food, including noodles, is designed to be eaten with only a
pair of chopsticks. The only people in Chinese cooking that are in
need of any utensils, such as a knife, are the cooks that prepare the
food to be eaten with only chopsticks. Part of the job of a cook is to
cut up any meats or vegetables cooked in the food to bite-sized pieces
that can be picked up with only a pair of chopsticks. The ordinary
eater has no need for a knife and for anything to hold the food while
it is being cut. Italians do use knives, forks, and spoons, and have
plenty of dishes, generally so-called second plates (secondi piatti)
that require that the eater cut his or her own meat or vegetables into
bite-sized pieces. Inter estingly, most pasta dishes, other than those
involving pasta whose individual noodles, e.g, lasagna, are too big to
be bite sized, could be eaten with chopsticks. Most pasta sauces are
made with bite-sized chunks of meats, fish, and vegetables, that have
been cut to bite size by the cook. Here too, the pasta eater with
chopsticks has no real need for a knife and fork. Of course, if the
sauce were so liquidy that it could not stick to the pasta,
vegetables, or meat, then a spoon would be needed, but that would be
true also of any Chinese food that had a very liquidy sauce. Perhaps,
this similarity between Chinese food and Italian pasta dishes is
confirmation of the veracity of the Marco Polo legend.

9 Comparison of Algorithms

The Chinese repeated-folding-and-stretching algorithm, with its
logarithmic complex ity is significantly more powerful than any
Italian cutting-based algorithm, with linear complexity, in two
different ways:

0x22013a74293f6f55e0c065d5fa4c4997aab12d71c9658a574e9a1a492e083b74

8 Daniel M. Berry and Luisa Mich

1. The logarithmic-complexity algorithm can generate so many more
noodles in a time duration than can any linear-complexity algorithm,
particularly when the noodle maker is folding and stretching quickly,
and he goes beyond six folds. Twelve folds and stetches in 41*.34
seconds suffices to make 4096 noodles. Making 4096 noodles by any
linear-complexity algorithm would require a *lot more than 41*.*34
seconds.

2. When the two algorithms are operated totally manually, it is a lot
easier to achieve uniformity in the cross section of the noodles with
the repeated-folding-and-stretch ing algorithm than with any
cutting-based algorithm.

10 Variations of the Basic Noodles

The different algorithms for making noodles lead to variations of the
basic noodles that we see in the two countries. The fact that a flat
sheet of dough is cut into strands that become the noodles suggests
cutting the sheet into other shapes. Hence, we see noodles in the
shapes of triangles, squares, rectangles, circles, stars, etc. Once we
have these different shapes, we begin to see yet other variations,
such as pinching a rectangle into a bowtie, molding a circle into a
shell. Once we have shaping and pinching, with the addition of a bit
more water, pinching can be used to paste edges together. Then rolling
and pasting a wet rectangle yields a tube that can be filled. Covering
part of a shape with some filling and folding and pinching wet edges
around the filling yields filled tortellini. Once all this is
automated, shapes that can be made by machinery become possible.

The Chinese la mi ¯ an algorithm does not lend itself to these
cutting-based variations. ` There are variations in the length and
diameter of the noodles, the raw material used to make the noodles,
and the twistiness of the noodle achieved by variations in the process
of drying the noodles, e.g., by spiralling the wet noodles around a
dowel of an appropriate diameter.

11 Conclusion

There are a number of issues that require further study, which we
encourage the inter ested reader to take on.

-- Perhaps, the space required for an algorithm should be considered.
Is there a mean ingful space--time tradeoff? Does the size of the
available kitchen make a differ ence, e.g., as for a home versus a
restaurant kitchen?

-- What is the interaction between the algorithms and the ingredients
used to make the dough?

-- What is the interaction between the algorithms and the issue of
fresh versus dried noodles?

-- What is the interaction between the algorithms and the local
culture?

-- Can a Chinese algorithm be applied in Italy and can an Italian
algorithm be applied in China?

-- How easily learned is each algorithm?

-- How automatable is each algorithm?

0xabf716b6f89315319f2c8e33070250c4e121084de16180a39cb7f8f51d55b674

Computational Complexity of Noodles 9

-- Which algorithm is most appropriate to use in a restaurant in which
food is made to order?

-- What are the empirically determined threshold values for n (the
number of noodles made in a batch), below which the traditional basic
and parallel Italian algorithms are more efficient locally than the
traditional Chinese algorithm?

A short investigation on the World-Wide Web shows that noodle
production is a big business world wide. It is apparent that noodles
of all kinds are made, not just in the countries of their origins, but
just about anywhere. It does appear that for noodles of nationality
N to be made elsewhere, in E, E must have a significant
population of immigrants from N.

Of course, in the modern small world in which a food product produced
in any part of the world can be sold in stores anywhere in the world,
one can buy Italian pasta in China and Chinese mian in Italy. `

Acknowledgments

Thanks to Nachum Dershowitz, Dick Kemmerer, Mickey Krieger, Chryss
Mylopoulos, Frank Tompa, and Dave Tompkins for comments on an earlier
draft. Frank, in particular, offered some insights that led to a
number of improvements to the paper.

References

1. Lin-Liu, J.: On the Noodle Road: From Beijing to Rome, with Love
and Pasta. Riverhead Books, The Penguin Group, New York, NY, USA
(2013)

2. Wikipedia: Chinese noodles--- Wikipedia, the free encyclopedia
(2015) http://en. wikipedia.org/wiki/Chinese_noodles, [accessed 1 May
2015].

3. Hildebrand, C., Kenedy, J.: The Geometry of Pasta. Box Tree,
London, UK (2010) 4. Wikipedia: List of pasta--- Wikipedia, the free
encyclopedia (2015) http://en. wikipedia.org/wiki/List_of_pasta,
[accessed 1 May 2015].

5. Kummer, C.: Pasta. The Atlantic Monthly (1986)
http://www.theatlantic.com/ magazine/archive/1986/07/pasta/306226/,
[accessed 1 May 2015].

6. Berry, D.M.: 'What, Not How?': The case of specifications of the
New York bagel. Annals of Improbable Research 15 (2009) 6--10

0x0d417c7e9a4c6c1e996ae17677cda151f43658f95fd2134e9ecc033a6d39113d

CONFIDENTIAL COMMITTEE MATERIALS

SIGBOVIK 2016 Paper Review

Paper 2: The Computational Complexity of Chinese and Italian Noodle
Making

With the assistance of the Carnegie

Mellon University Postmodern Languages

Department

中国面条算法最好。 我很高你同意。 大利面算法太慢了,因大利人真惰。
我一个大利人用 大利文写介,但他 没回信。 所以谷歌翻他写介。
面很好吃.在我家我有一只。 他睡的候 我 切断 他的毛做面。 刀削面呢?
你吃? 听那是最好的面。 豆腐呢? 你喜吃豆腐呢? 我想吃豆 腐。 你妹妹多大?
第八部分不。 中国人用勺喝。 你怎以中国人只有筷子? 加拿大人怎喝?
除了那个部分以外都了,一共有意思。

- 笨蛋美国人

Come osi dire rendendo noodle italiano e pi ` u lento di noodlemaking
cinese ? Quei comunisti non ` poteva dire polpette di mia madre dal
mio nutsack . Avrei potuto iniziare ad usare le bacchette quando
mangio, perche il mio coltello e forchetta saranno preoccupati
scriccatura gli occhi fuori e ´ tagliare in su per il mio cane .

Mio fratello Giovanni conosce alcuni ragazzi in Sicilia . Non si vuole
scopare con questi ragazzi . ti suggerisco" Respingere " questo
documento a causa di " riferimenti poveri ", se vi capitasse di voler
vivere per vedere un'altra citazione. - Google Traduttore

0xafa5c091a6a3773082906f88b1fefba759fea0a101d12d17e5e6af4f733c8579

7

Abstract

Which ITG Stepcharts are Turniest?
{width="0.9999945319335083in"
height="1.9644553805774279in"}

Ben Blum

bblum@cs.cmu.edu

ITG is a popular dance game in which players step on ar rows while
listening to music. The arrow patterns, indi cated by a stepchart, may
range among any level of com plexity and difficulty. Among the many
factors contribut ing to a stepchart's difficulty is how much the player
must turn from side to side. Other more obvious factors, such as raw
speed, have been well studied in prior work. This paper presents an
analytic study of this turniness factor. We study the turniness of
many existing stepcharts, and present a novel (but unsurprising)
approach to automat ically generating maximally (or minimally) turny
charts. Among real-world songs, we find stepcharts with overall
turniness ranging from 0% to 81.33% of the theoretical maximum.

Categories and Subject Descriptors D.D.R. [Exercise and
Fitness]: Arcade Dance Games

Keywords in, the, groove

1. Introduction

In 2005, Roxor Games, Inc. released In The Groove, a dance rhythm
music video arcade fitness game, in which players control a
protagonist using their feet to step on floor-mounted directional
indicators. The protagonist, shown in Figure 1, takes the form of any
number of arrow-shaped directional receptacles, and must navigate a
world of similarly-shaped obstacles (henceforth "ar rows") by
consuming them with the appropriate recepta cle. Roxor Games, Inc. In
The Groove (henceforth "ITG") is most commonly played using the
"cabinet" form factor, shown in Figure 2, which includes two large
metal dance pads, each with four directional indicators (henceforth,
also, "arrows").

The game includes a library of rhythmic audio ac companiment files
(henceforth, "songs"), each of which

Permission to make digital or hard copies of part or all of this work
for personal or classroom use is granted without fee, provided...
honestly, provided nothing. The ACH is already flattered enough that
you're even reading this notice. Copyrights for components of this
work owned by others than ACH must be laughed at, then ignored.
Abstracting with credit is permitted, but abstracting with cash is
preferred. And please tip us, for the love of Turing.

SIGBOVIK '16 Pittsburgh, PA, USA

Copyright c 2016 held by owner/author(s). Publication rights licensed
to ACH.

ACH . . . $15.00

Figure 1. ITG gameplay, including score indicator (top),
protagonist avatar (mid), directional obstacles (low), and step
judgement, life bar, and combo indicator (figure these out for
yourself, I'm getting tired).

Figure 2. An ITG cab. RIP in peace, Roxor (Konami 2005).

is associated with one or more fixed patterns of arrows (henceforth,
"stepcharts"). These charts are often, but not always, synchronized to
the beat of the song. During gameplay, the stepcharts appear on screen
and scroll to wards the protagonist avatar at a rate either fixed or
vari able (henceforth, "BPM"). When the position of an arrow in the
chart coincides with the avatar, the player must ac tuate the arrow of
the corresponding direction. The game will judge the player's timing
accuracy, and penalize or reward them accordingly with scores and life
bar fill. A "Fantastic" judgement (as in Figure 1) indicates a timing
error not exceeding 15 milliseconds. Other judgements include
Excellent, Great, Decent, Way Off, and Miss. As a visual assist to the
player, notes are coloured according to
_{their beat granularity: ˇ}"_{, ˇ}"³_{, ˇ}^"_{(, ˇ}^"(³_{, ˇ}^"_{), ˇ}^")³_{, ˇ}^"*.

0x1bedbdc370f4d8b05e3eed208c2f954f9ea4bfac862d9406edfed9867c798b5a

Figure 3. ITG can be played "Bar" or "No-Bar". Bar play ers must
wear sandals (like an idiot; who is that guy any way?), while No-Barrers
must always play on the right.

Figure 4. Doubles play is beyond the scope of our work. It
requires (or perhaps produces?) a magnificent beard.

The game may be played in several modes, the most common supporting up
to two (2) players, each operating their own protagonist using either
the left or right set of four arrows. This game mode may be played with
or with out the assist of a curved metal rod mounted behind the arrows
(henceforth, "bar"), as shown in Figure 3. In other game modes, a single
player may operate up to all 8 of the arrows. When all 8 are used, the
game mode is known as "Doubles", as shown in Figure 4, and is often
associated with excessive No-Barring, use of hands and knees to op erate
the arrows, and impressive facial hair. In this body of work, we will
focus exclusively on the Singles game mode, in which each player
controls four arrows: one Up (U ), one Down (D ), one Left (L),
and one Right (R). Without loss of generality, we further assume that
only one player plays at a time, using exactly two feet at a time, and
that she will shower immediately afterward.

{width="0.9999945319335083in"
height="1.9644553805774279in"}

Figure 5. Common patterns (Akgul 2015). Honk honk!

2. Properties of Stepcharts

Being a game, one might assume that players find it fun to step the
arrows in the indicated patterns, as opposed to, for example, stepping
them in random unrelated pat terns, or stepping off the pad entirely
to go play Rocket League (Psyonix 2015). Accordingly, step authors
take care to produce stepcharts with interesting patterns. Typ ically,
players step the arrows alternatingly with either foot. Step authors
can either reinforce this tendency, by maintaining that left and right
arrow targets always re ceive arrows of different (even or odd)
sequential parity; or subvert it, forcing the player to step on the
left arrow with their right foot (or v.v.). The former pattern is
called a stream, and the latter pattern a crossover. Crossovers
are loved by some players (Figure 3, left), and hated by others
(Figure 3, right).

Figure 5 shows many common step patterns. Among these, note especially
the lateral (LU R LD R), in which the player briefly faces
backwards (left foot on R and right foot on L), and the spin
(LU R D LU ), in which, yeah, you get the picture.

2.1 Difficulty

Stepcharts are rated in difficulty on a scale from 1 to 20 "feet"
(hurtpiggypig 2013)¹. To date, difficulty is judged by a human
(typically the step author), and primarily reflects factors such as
burstiness (footspeed), prolongedness of streams (stamina), and
complexity of jumps, holds, and crossovers (technical). These
measures of difficulty have been well-studied in prior works (Zetorux
and WinDEU 2008; Konkul 2014; thattagen 2014). Some players are re
ally good at In The Groove.

¹ Other dance games, which shall remain unnamed, but whose initials
are (Konami 2005), feature wimpier stepcharts rated only up to 10. As
ITG players got better, they left those charts in the dust and began
creat ing their own charts to challenge themselves with ridiculous
difficulties. This paper's author plays ITG at the 13-14 level.

0x001a4af5de423ad497db795dfb29c43f3e14a785cfd0434e19c475c40fc47657

2.2 Facing

Regardless of the presence of crossovers, all step patterns will keep
the player facing one way or another, and most include sequences that
will change the player's facing back and forth. For example, when the
player stands with left foot on L and right foot on U , they are
facing up-left, or U L. Standing on D and R also produces the same
U L facing, unless the player is crossed-over (left foot on R), in
which case the facing is D L. Table 1 shows all possibil ities of
facing using two feet on four arrows. We exclude the possibility for
both feet to be instantaneously on the same arrow (called a
"footswitch"), leaving this pattern to future work.

Right foot

← ↓ ↑ →

← - U R U L U

{width="0.9999945319335083in"
height="1.9644553805774279in"}

Figure 6. Three streams of differing turniness. Note how the
color-coding of the notes by beat aids to discern turni ness at a
glance: the right foot is always on blue, and it moves among 1, 2, or
3 different arrows respectively.

Left foot

↓ D L* - L U L ↑ D R* R - U R → D † D R* D L* -

in this stream, not all of the steps have T = 2: the average
turniness of this stream is only 4/3.

We are interested in the following questions:

Table 1. Facing directions. "Crossover" facings are marked (*),
and the "lateral" facing is marked (†). Note the appealing diagonal
symmetry.

2.3 Turning

A stepchart contains a turn when a sequence of steps changes the
player's facing.

Definition 1 (Turniness). The turniness T of a single step is
the angular distance (measured in increments of π/*4) which that step
changes the facing compared to the facing from the previous two steps.*

The turniness T of a stream is the average of each step's turniness
(excluding the first two for which it is undefined).

Because only one foot may change at a time, it is easy to see that the
maximum turniness of a single step is 2. These steps always involve
one foot moving entirely across the middle of the pad (from U to D
, from L to R, etc). By tradition, these are called candle
steps, according to the imagery that if a candle were placed in the
middle of the 4 arrows, this step would knock it over. I don't know
why it couldn't be called a beer step instead, though.

Turning is exhausting. Consider the three stream pat terns shown
in Figure 6. In the leftmost stream, the player must barely move her
feet at all, never changing facing from U . In the middle stream,
the player faces largely U R, with brief U and R facings (T = 1)
as she moves be tween the L/D and U /R arrows. Both of these
streams are very easy to step without becoming fatigued. How ever, the
rightmost stream features many candle steps (or beer steps), changing
facing from U R to U L and back in the span of a single measure.
ITG players hate this (Fouhey and Maturana 2013)! However, note that
even

1. What is the turniest possible stepchart?

2. How is maximum turniness affected by various con straints to
contain no crossovers/laterals/etc?

3. How turny are real-world ITG charts?

3. Chart Synthesis

We developed a program for exploring all possible step patterns using
a little-known yet powerful computational technique (Apostol 2012;
Curtin 2005). This program computes the average turniness of every
such pattern. However, while some players enjoy any step pattern in
cluding spins (Vangpat 2015), other players may prefer only crossovers
and laterals in their charts, while still oth ers prefer charts
completely vanilla. Hence, our program is further capable of filtering
patterns by 5 predicates:

• All patterns allowed

• No spins

• No 270s

• No laterals

• No crossovers (vanilla)

Note that each predicate captures a strict subset of step patterns
compared to the one above it (a lateral is a crossover, and so forth).
These predicates are imple mented as shown in Figure 7.

Deciding on how long of step sequences we should search for is a
tradeoff between accuracy, in judging turni ness in small fractions,
and (drumroll...) exponential ex plosion. To strike a balance we
decided to experimen tally measure turniness at a granularity of
⅛th, which re quires searching for step sequences of length 18
(twice the denominator, plus 2 for the first 2 steps whose turniness

0x160d22fc751ddd470ed6647e5f80a5404c860575d4e6719722b053aa7545b344

is_xover(φ) = φ ≡ D L ∨φ ≡ D R
{width="0.9999945319335083in"
height="1.9644553805774279in"}

is_lat(φ) = φ ≡ D

is_270(φ,φ₁,φ₂) = (φ ≡ D R ∧(φ₁ ≡ D L ∨(φ₁ ≡
D ∧φ₂ ≡ D L)))∨

(φ ≡ D L ∧(φ₁ ≡ D R ∨(φ₁ ≡ D ∧φ₂ ≡ D R)))

is_spin(φ,φ₁,φ₂,φ₃) = (φ ≡ R ∨φ ≡U R ∨φ ≡ L
∨φ ≡U L)∧is_270(φ₁,φ₂,φ₃)

Figure 7. Formal definitions of crossovers, laterals, 270s, and
spins. Each predicate takes as arguments the current facing φ, and
up to the three most recent previous facings, φ₁, φ₂, φ₃.

quence repeated ad infinitum, freeing ourselves from the

⅛th granularity imposed by our experimental setup. We

find that the turniest crossovers have T = 3*/*2 and that

the turniest laterals have T = 8*/*5.

The case of 270s is irregular: we found no 18-step se

quence turnier than the turniest laterals, and most no

tably, none of the sequences included a 270 step in the

middle of the stream. Figure 9(d) shows a stream with

crossovers and laterals and no 270 step until the very last

one. To see why, imagine yourself on the pad here: the

only possible 19^th step that doesn't result in a spin is to

step back on the same arrow your left foot is already on.

That step has T = 0, which would undo any potential

turniness gained from going into the 270. Nevertheless,

Figure 8. Distribution of unique step sequences among turninesses,
classified by what types of step patterns are allowed in the chart.

is undefined). Also, our program WLOG restricts streams to always
start on the left foot, and never to start crossed over. Figure 8
shows our results. The highest data point clocks in at 40,609,780:
there are over 40 million unique 18-step sequences, any patterns
allowed, that have turni ness 0.875.

We see that, with one exception, allowing each new type of step
pattern increases the maximum possible turniness of the chart. The
exception is that 270s do not allow for any additional turniness over
laterals, although they do allow for *more possible ways*to achieve
maximum turniness. Despite no additional turniness, this is cru cial
information for stepchart authors, as ITG players will (usually) get
bored of any chart that simply repeats the same pattern over and over.

Maximum turniness! Now to the paper's titular ques tion: what step
sequences underlie those data points on the far right of each curve?
Though it would be tedious to transcribe them all into Stepmania's step
editor (Step Mania 5.0 2016), we manually inspected many of them to
select the most representative and/or photogenic ones from each
category. We show these sequences in Figure 9. These visualizations
allow us to manually compute the true turniness of each sequence,
imagining the core se

270s retain some real-world application, as demonstrated by (Foy and ,
2004) which similarly employs a 270 as the very last step.

Perhaps predictably, pure spins make for the turniest possible chart.
There are only two possible ways to candle every step; one's name is
"clockwise", and you can guess the other.

Minimum turniness. Each of the 5 categories shares the same data
point at T = 0: there are 7 possible streams that never turn at all.
These are the 7 "tower" patterns LR LR, LU LU , LD LD , U RU
R, D R D R, U DU D , and DU DU . We already showed the first of
these in Figure 6, left. For further treatment of minimally turny
charts, we refer the reader to (WinDEU and Ashura 2009).

4. Existing Chart Analysis

Of course, composing a stepchart of nothing but the
theoretically-turniest patterns would be extremely tire some (in more
ways than one). We turn our attention to existing ITG charts which
were developed prior to this study, to investigate how much ITG
players turn in the real world. We processed every stepchart in our
collection, which includes 70+ song packs. Most well known pack series
from the ITG community are included, such as Cirque, ITG, Mute
Sims, Pendulum, r21*, SPEED COOOORE, Tachyon, The Legend of
Zim, Valex's Magical 4-Arrow Adventure, and Oh Henry! Mad Stamina:
Streamy · Brutal · Stamina Bar in Milk Chocolate.

0xb2ad59ed236ef957c365ad85f09f7c8281ade5032a068c791ba0a3196da91c5d

{width="0.9999945319335083in"
height="1.9644553805774279in"}

$a$ Vanilla, T = 4*/3. (b) Crossovers, T = 3/2. © Laterals, T =
8/5. (d) 270s (irregular). (e) Spins, T = 2. **Figure 9.* The
turniest possible stepcharts.

Limitations. Real-world stepcharts include many pat

terns not accounted for in our analysis. We did not ex

pect much trouble from jumps and jacks, opting sim

ply to ignore them and count the turns among the sur

rounding single-steps. Footswitches and doublesteps,

however, can foil this strategy, as our analysis will inadver

tently begin stepping with feet inverted from where they

should be. Merely getting turned around is not a prob

lem (computers don't have eyes), but the act of turning

around involves some candle-steps, which could cause a

footswitch-heavy chart to seem very spinny even though

the proper footing would never make the player cross

over at all. Coping with these limitations is beyond the

scope of our work, although we will highlight some ex

perimental false-positives later.

4.1 Results

As shown in Figure 10, the vast majority of real-world stepcharts have
average turniness between 0.6 and 1.0. We don't really care about those.

The Turniest Charts. No joker has yet dared to make the turniest
possible chart (all spins), but one chart comes close. Standing alone
as the only chart turnier than 1.5 is the Easy 3 for DO ME (Konami
DDR 4thMIX PLUS), which is mostly spins punctuated by a few breaks, as
shown in Figure 11(a). (Vangpat 2015) loves this chart.

Actually, 20 of the 30 turniest charts are all from DDR packs, most of
which are Easies. Although DDR charts are known for being fairly
crossovery in the upper ranges of difficulty, a close inspection of
the easier charts will show that very little care was put in while
writing them to avoid excessive double-stepping. It's no wonder new
ITG

Figure 10. Distribution of turniness among 8,278 exist ing ITG
charts.

players, who used to play DDR, always double-step even when they don't
need to. Sheesh, Konami.

Beyond these extreme examples, we are interested in some more normal
charts people might actually like to play. Table 2 shows the turniest
charts of each level, for the most popular difficulty levels ranging
from 7 to 17. So, next time you want to work on your laterals or
candles, you have me to thank!

Surprisingly, BRILLIANT 2U (Orchestra-Groove) (Kon ami DDR 2ndMIX)
is full of 270s. I didn't think anybody ever put those in real charts.
Finally, an honourable men tion goes to Oedo Hop (sssmsm and
Palpable 2007), the 2^nd turniest 7 (and 4^th turniest chart overall!)
with T = 1.384. (Hanneman 2010) really likes that one so we had to
mention it.

0xa9add8e9b72241b1e482140d31d75a186f59ef7c5ed16f5e1ecd031b7bb276d5

$a$ DO ME, T = 1.63. Proportion of non-spinny section enlarged to
show detail.

$b$ Mr. Saxobeat, T = 1.04. Look at all those candles! No wonder
it was so hard for us to pass this one.

$c$ Flames of the Sky, T = 1.04. False-positive T from foot
switches. Actually faces R/U R/ U /U L/L the whole time.

{width="0.9999945319335083in"
height="1.9644553805774279in"}

$d$ Sick Dubstep Track, T = 0.26. The least turny non trivial
non-beginner chart.

Figure 11. Real-world ITG charts of varying degrees of turniness.

Ft. Name Pack T 7 TRIP MACHINE DDR 1^st 1.407 8 BRILLIANT 2U (O-G) DDR
2ndMIX 1.347 9 Hearts of Ice In The Groove 3 1.127

10 Visible Noise In The Groove 2 1.188 11 KKKKK Come On r2112 1.145 12
Winnipeg is Fucking Over best of r21freak ii 1.150 13 Mr. Saxobeat
(*) Sexuality Violation 2 1.044 14 Fancy Footwork (†) Cirque du
Zeppelin 1.026 15 Flames of the Sky (*,†) Ft. Rapids VII 1.037 16
(no 16 with T ≥ 1*)* - -

17 Superluminal Ft. Rapids VII 1.058 18 (no 18s+ with T ≥ 1*)* - -

Table 2. The turniest existing stepcharts of each diffi culty. Songs
marked (*) are also shown in Figure 11. Songs marked (†) are
false-positives resulting from too many footswitches incorrectly
analyzed as spins.

The Least Turny Charts. 16 charts in our collection have T = 0.
Most of these are beginner charts, rated 2 or 3 feet and with no more
than 100 steps. *∆*MAX (WinDEU and Ashura 2009) stands out, as a
15-footer with 945 steps. God is that chart ever annoying.

Ft. Name Pack T 7 King Kong In The Groove 3 0.354 8 Jam Jam Reggae DDR
2ndMIX 0.428 9 Fantasia In The Groove 3 0.382

10 Oosanbashi TLOES Chapter 1 0.534 11 Release the Music Ft. Rapids
VII 0.507 12 Payon (Theme Of) CuoReNeRo MeGaPacK 0.396 13 Technodildo
The Legend of Zim 5 0.436 14 Gentleman TLOES Chapter 1 0.556 15 *∆*MAX
Tachyon Alpha 0.000 16 Dash Hopes 2 Tachyon Alpha 0.327 17 Resist
SPEEDCOOOORE 0.592 18 Baby Sexuality Violation 2 0.524 19 Pedal to the
Metal SPEEDCOOOORE 0.468

Table 3. The least turny existing stepcharts of each diffi culty
(trivial charts excluded).

Ignoring all beginner-difficulty and turn-free charts, the least turny
stepchart is Sick Dubstep Track (mute and Gotobed 2011), a 4-measure
joke rated 6,482 feet, the ma jority of which is shown in Figure
11(d). It has T = 0.263.

For readers who prefer more to tower than to turn, we similarly
tabulated the least turny charts of each common difficulty in Table 3.

0xe474dd5a737c07975d6fca26397568d59862633a1e56255b70bf478ea08f89f8

Song Pack # of Charts Avg. T Valex's Magical 4-Arrow Adventure 5 150
0.964 Valex's Magical 4-Arrow Adventure 4 170 0.956 Valex's Magical
4-Arrow Adventure 3 155 0.950 Valex's Magical 4-Arrow Adventure 7 150
0.937 Valex's Magical 4-Arrow Adventure 2 130 0.929 Valex's Magical
4-Arrow Adventure 95 0.919 Valex's Magical 4-Arrow Adventure 6 145
0.917 Subluminal 16 0.906 The Legend of Zim 1 26 0.906 FoxyMix 5 30
0.901 FoxyMix 4 - Nuclear Overdrive 68 0.899 Mute Sims 9 48 0.886 In
The Groove Rebirth + 147 0.881 StepMania 5 5 0.869 Cirque du Zeppelin
109 0.867 In The Groove 3 448 0.858 . . .

Piece of Cake 5 20 0.785 Cirque du Veyron 30 0.777 Stephcharts and
Richarts 81 0.770 Tachyon Delta 32 0.769 Tachyon Alpha 151 0.769
Sexuality Violation 2 219 0.766 TLOES Chapter 1 120 0.765 Fort Rapids
V (12s-16s) r3 Final 98 0.759 Noisiastreamz 20 0.758 In The Groove 331
0.754 Pendulum 150 0.747 SPEEDCOOOORE 2 70 0.731 SPEEDCOOOORE 47 0.709
The Legend of Zim 3 40 0.702 The Legend of Zim 4 44 0.701 The Legend
of Zim 5 19 0.667

Table 4. The turniest and least turny stepfile packs. Wow, great
job Valex! Zim had a good thing going but has been slacking off
recently.

The Turniest Other Things. Although our analysis picked out a good
many turny charts, any ITG player will inevitably get tired of playing
the same ones over and over. Hence, we are also interested in an
aggregated turni ness profile to show the average scores of many
different stepcharts at once. We computed average turninesses for
stepcharts grouped by pack and by step artist. Abbrevi ated
results for the former are shown in Table 4 and for the latter in
Table 5. For the sake of players who dislike turniness, we also list
the lowest-scoring packs and artists in addition to the
highest-scoring ones.

5. Future Work

Jumps. The most obvious next step for this work is to ac count for
jumps. This seems quite easy: compute the two possible facings of the
jump, depending which foot lands on which arrow, and use whichever
facing produces the

Step Artist # of Charts Avg. T
{width="0.9999945319335083in"
height="1.9644553805774279in"}

M. Emirzian 38 0.992

sssmsm 50 0.945

J.Berkowitz (Valex) 1025 0.939

B. Dinh 10 0.919

J. DeGarmo 26 0.906

J. Frederick 176 0.881

Fraxtil 23 0.880

M. Calfin 26 0.880

X. Ythar 24 0.879

R. Woods 22 0.874

R. McKanna 76 0.872

MIDI 86 0.870

Dark Luke 36 0.866

@@ 60 0.859

D. Bernardone 354 0.858

D. D'Amato 154 0.857

. . .

M. Simmons 334 0.787

Revolver 25 0.775

R. Konkul (Rynker) 125 0.774

K. Ward (,) 600 0.773

Freyja 89 0.766

P. Mason 14 0.765

M. Puls 167 0.759

P. Shanklin 37 0.756

I. Pyles 177 0.754

Gazebo 377 0.754

zimlord 217 0.747

C. Foy 205 0.739

B. Abear 29 0.733

Blazing 21 0.729

Mootz 29 0.715

Insane Steve 49 0.714

Table 5. The turniest and least turny step authors. Only authors
with 10 or more charts are included.

least turniness when compared to the previous and next steps in the
sequence. Honestly, we should have imple mented that for this paper,
but we only realized how it should work after we finished computing
our dataset; and owing to an inferior conference's deadline coming up
in 10 days, we don't have time for re-running experiments (Anonymized
2016).

Footswitches. More difficult is the matter of deciding whether
stepping the same arrow twice in a row consti tutes a jack (same foot)
or a footswitch. As we saw in Fig ure 11, our current approach of
assuming it's always a jack can lead to some false-positive T values.
Judging the presence of footswitches is a nontrivial problem even for
human intuition, so we view this as an exciting area for future
research. So as not to piss off the player, most stepcharts tend to
feature only jacks or only switches, never both. Future extensions of
our algorithm could exploit this convention to decide with high
confidence whether or not an entire chart is footswitchy.

0x6bd5a2375da07d4f14a1eafd336bf63d923bc0789d15e52deab64e4312e12646

$a$ Bracketable. (b) Forced turns. © Roll-stream. Figure 12.
Future work.

Fractional Turns. Experienced ITG players do not step with their
feet on the middle of each arrow; rather, they try to step on the
edges and "brackets" between arrows, hit ting each step with heel or
toes only to minimize the dis tance their feet must move. This
tendency distinguishes further granularity of turning than what we
identify in this work. Consider the two streams shown in Figure 12 (a)
and (b). Although they measure the same T value of 1, (b) is
considerably more exhausting to step, as (a) allows the player to
bracket the entire run. Future work could han dle this by counting a
1-turn step as the full value only if the player subsequently
continues turning farther in the same direction (which would force the
player's feet off the brackets), and otherwise assign 0 \< T \< 1
for such a step.

Holds and Rolls. Many charts use holds or rolls to force the player
to step all concurrent tap-steps with the other foot, which breaks our
alternating-feet assumption. When multiple steps are concurrent with a
hold, they must be double-stepped, and the facing for each com puted
using the hold's arrow rather than the most recent one. When multiple
steps are concurrent with a roll, the facings are determined similarly,
but repeatedly stepping the roll results in a stream, as shown in Figure
12© (MIDI and Basshunter 2007). Judging how hold-steps and roll
streams must be stepped is another exciting opportunity for future work.

6. Conclusion

Our analysis program can be found at https://github.
com/bblum/sigbovik/tree/master/itg/code, and our full experimental
dataset is available at http:// tinyurl.com/turniness.

The value of this work is already abundantly clear, as through it, the
author has found several new charts he is interested to play. We hope
our published dataset can provide similar value to other ITG players
worldwide. Please accept our paper. We worked hard on it.

A. Most turny patterns
{width="0.9999945319335083in"
height="1.9644553805774279in"}

A.1 Vanilla

Following are the most turny 18-step patterns that are totally
vanilla, withT = 1.375. (Manual inspection reveals the true turniness
to be 4/3.)

URDULDURDULDURDULD DRUDLUDRUDLUDRUDLU

A.2 Crossovers

Following are the most turny 18-step patterns that may include
crossovers only, with T = 1.5.

URDULDURDLDRULURDL URDULDRDLUDRULURDL URDULDRDLURULDURDL
URDULDRDLURULDRDLU URDLDRUDLUDRULURDL URDLDRUDLURULDURDL
URDLDRUDLURULDRDLU URDLDRULURDULDURDL URDLDRULURDULDRDLU
URDLDRULURDLDRUDLU URDLDRULURDLDRULUR URDLDRULURDLDRURDL
URDLDRULURDRULURDL URDLDRURDLDRULURDL URDRULURDLDRULURDL
DRUDLUDRULURDLDRUL DRUDLURULDURDLDRUL DRUDLURULDRDLUDRUL
DRUDLURULDRDLURULD DRULURDULDURDLDRUL DRULURDULDRDLUDRUL
DRULURDULDRDLURULD DRULURDLDRUDLUDRUL DRULURDLDRUDLURULD
DRULURDLDRULURDULD DRULURDLDRULURDLDR DRULURDLDRULURDRUL
DRULURDLDRURDLDRUL DRULURDRULURDLDRUL DRURDLDRULURDLDRUL
LUDRULURDLDRULURDL LURULDURDLDRULURDL LURULDRDLUDRULURDL
LURULDRDLURULDURDL LURULDRDLURULDRDLU LDURDLDRULURDLDRUL
LDRDLUDRULURDLDRUL LDRDLURULDURDLDRUL LDRDLURULDRDLUDRUL
LDRDLURULDRDLURULD

A.3 Laterals

Following are the most turny 18-step patterns that may include
crossovers and laterals, with T = 1.625. (Manual inspection reveals
the true turniness to be 8/5.) URDLDRULRDLURLDRUL URDLRULDRDLURLDRUL
URDLRULDRLURDLDRUL URDLRULDRLURDLRULD DRULURDLRULDRLURDL
DRULRDLURULDRLURDL DRULRDLURLDRULURDL DRULRDLURLDRULRDLU
LURLDRULRDLURLDRUL LDRLURDLRULDRLURDL

A.4 270s

Following are the most turny 18-step patterns that may include
crossovers, laterals, and 270s, with T = 1.625. (Manual inspection
reveals irregularity; these streams ex hibit no core pattern that can
be repeated to retain the maximum turniness.)

URDULDRLURDLRULDRU URDLDRULURDLRULDRU URDLDRULRDLURULDRU
URDLDRULRDLURLDRUL URDLRULDURDLRULDRU URDLRULDRDLURULDRU
URDLRULDRDLURLDRUL URDLRULDRLURDULDRU URDLRULDRLURDLDRUL
URDLRULDRLURDLRULD DRUDLURLDRULRDLURD DRULURDLDRULRDLURD
DRULURDLRULDRDLURD DRULURDLRULDRLURDL

0x438b34787a6a076d54e11f8e7c6476ccfe85ed9ab5a29e33f01cff72341e7912

DRULRDLUDRULRDLURD DRULRDLURULDRDLURD DRULRDLURULDRLURDL
DRULRDLURLDRUDLURD DRULRDLURLDRULURDL DRULRDLURLDRULRDLU
LURULDRLURDLRULDRU LURLDRULURDLRULDRU LURLDRULRDLURULDRU
LURLDRULRDLURLDRUL

LDRDLURLDRULRDLURD LDRLURDLDRULRDLURD LDRLURDLRULDRDLURD
LDRLURDLRULDRLURDL

A.5 Spins

Following are the most turny 18-step patterns that may include any
pattern, with T = 2.

URDLURDLURDLURDLUR DRULDRULDRULDRULDR LURDLURDLURDLURDLU
LDRULDRULDRULDRULD

B. Related Work...?

Figure 13. We employ the techniques of (Hanneman 2010) for ITG
machine translation (Karakos et al. 2008; Goto et al. 2013).

References

S. E. Akgul. This is how we DO in DDRillini. In DDR + ITG Players
Facebook Group, pages You want page numbers, bibtex? It's a photo of
a whiteboard from Facebook. Get it together., 2015.

K. Apostol. Brute-force Attack. SaluPress, 2012. ISBN 613627454X,
9786136274546.

M. Curtin. Brute Force: Cracking the Data Encryption Stan dard.
Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2005. ISBN
0387201092.

A. for Double-Blind Submission. Ode to reviewer two. SIG BOVIK 10
(that's decimal, not binary), 2016.

D. F. Fouhey and D. Maturana. Find a separating hyperplane with this
one weird kernel trick! Proceedings of the 7 th ACH SIGBOVIK Special
Interest Group on Harry Quechua Bovik, 2013.

C. Foy and K. W. ,. Utopia. In The Groove 1, 2004. Challenge 11.

I. Goto, M. Utiyama, and E. Sumita. Post-ordering by parsing with ITG
for Japanese-English statistical machine translation.

12(4):17:1--17:22, Oct. 2013. ISSN 1530-0226. doi: 10.1145/ 2518100.
URL http://doi.acm.org/10.1145/2518100.
{width="0.9999945319335083in"
height="1.9644553805774279in"}

G. Hanneman. DeltaX: A new paradigm for machine translation. A Record
of The Proceedings of SIGBOVIK 2010, 2010.

L. hurtpiggypig. Simply love. Simply Love is a custom theme designed
for Stepmania 3.95 or ITG arcade machines., 2013.

D. Karakos, J. Eisner, S. Khudanpur, and M. Dreyer. Machine
translation system combination using ITG-based align ments. In
Proceedings of the 46^th Annual Meeting of the Association for
Computational Linguistics on Human Lan guage Technologies: Short
Papers, HLT-Short '08, pages 81-- 84, Stroudsburg, PA, USA, 2008.
Association for Computa tional Linguistics. URL
http://dl.acm.org/citation. cfm?id=1557690.1557712.

Konami. Konami Corporation v. Roxor Games, Inc., Mad Catz, Inc., and
Redoctane. United States District Court for the East ern District of
Texas, 2005.

Konami. Brilliant 2U (orchestra-groove). DDR 2ndMIX. Chal lenge 8.

Konami. Do me (H.I.G.E.O. mix). DDR 4thMIX PLUS. Easy 3.

R. Konkul. Rynker - call of the hound (tachyon ep silon 20) 88.21.
https://www.youtube.com/watch?v= 6yB5WmIBZPk, 2014.

MIDI and Basshunter. Boten anna. In The Groove Rebirth +, 2007.
Challenge 11.

mute and C. Gotobed. Sick dubstep track. Mute Sims 7, 2011. Challenge
6482.

Psyonix. Rocket league. Video game, 2015.

sssmsm and Palpable. Oedo hop. r2112, 2007. Medium 7. StepMania 5.0.
http://www.stepmania.com/, 2016.

thattagen. [ddr] canblaster - \"dawgs in da house\" stupid dou bles
chart (10). https://www.youtube.com/watch?v= CZlB16BroPg, 2014.

A. Vangpat. http://photos2.alanv.org/, 2015.

WinDEU and D. Ashura. *∆*MAX. Tachyon Alpha, 2009. Chal lenge 15.

Zetorux and WinDEU. Team dragonforce. https://www.
youtube.com/watch?v=uSfx5Zdgyfc, 2008.

0xa00a4a411b23f44ffe7fcabfa8a053b6087a04b2558ed51c83a9dc7fa8672e75

CONFIDENTIAL COMMITTEE MATERIALS

SIGBOVIK 2016 Artifact Evaluation

Paper 12: Which ITG Stepcharts are Turniest?

Claim 1: LURR DURR

EVALUATION OF CLAIM: The evaluation committee tripped repeatedly while
attempting to evaluate this claim, leading to the loss of several
perfectly good "candles." The committee requests an instructional
video on performing this maneuver, as well as a fresh 6-pack of
Woodchuck.

Though the committee does concede evaluating this claim would have
been easier if we weren't halfway through the 6-pack of Woodchuck when
we started.

Claim 2: Real-world tracks achieve 81.33% of the theoretical maximum
turniness.

EVALUATION OF CLAIM: The evaluation committee has confirmed that .8133
* 2 = 1.6266 which is an appropriate rounding-down of the number
1.6267 that appears on the spreadsheet. We appreciate the author's
willingness to round numbers in the least favorable a direction, a
subject with which we understand systems researchers frequently
struggle.

However, the artifact submitted contains no actual stepcharts, let
alone songs, and thus we have no way to evaluate whether this claim is
actually true.

We were about to reject your submission for this reason, but then a
member of the committee discovered an algorithm for turning
theoretical stepcharts into real stepcharts. Followed by the insight
that 1.6266 *\<*2.0, we discovered that the author is indeed capable
of producing such a stepchart upon request.

Claim 3: The author is capable of multiplying various numbers by
10000.

EVALUATION OF CLAIM: We diligently verified your multiplication of
various numbers by the common number 10000 and discovered that in
every case the multiplication is correct. This is in stark contrast
with another publication presented at this conference in which an
author utterly failed to understand any calculus whatsoever.

0xb06e158858204e66e8ff4f8437090e77a985caaa9e0bbb0db96440800fd2b300

For this reason, the evaluation committee has found it appropriate to
present you with the inaugural Innovations in Trivial Mathematics
award. Congratulation (yeah, you only get one).

In return for this acknowledgement, we request that the author leads
next year's Trivial Math ematics workshop in order to improve the
quality of mathematics submitted to this prestigious Conference.

Claim 4: The authors claim to have implemented a turniness analysis
in Standard ML.

EVALUATION OF CLAIM: However, much to our disdain, the code appears to
be written in Latin. Thankfully, one member of the evaluation
committee remembered enough Latin from high school to translate the
code into English. Please submit your code in English next time. The
original Latin is reproduced below for posterity:

IFS=$'\n'

for i in 'cat /tmp/authors'; do

output='grep \"$i\"

Downloads/Which\ ITG\ stepcharts\ are\ turniest_\ -\ Sheet1.tsv
^{| sed 's/.}_*\t//'' total='echo \"$output\"

| wc -l'; numer='echo \"$output\"

| sed 's/\r//g'

| tr '\n' '+'

| sed 's/+$//''

echo -ne \"$i\t\"

echo \"($numer)/$total\" | bc

done

IFS=$'\n'

for i in 'cat /tmp/packs

| sed 's/\r//g''; do

output='grep -- \"$i/\" which.tsv

^{| sed 's/.}_*\t//''; total='echo \"$output\"

| wc -l'; numer='echo \"$output\"

| sed 's/\r//g'

| tr '\n' '+'

| sed 's/+$//''

echo -ne \"$i\t\"

echo \"($numer)/$total\" | bc

don

OVERALL EVALUATION: Many of the numbers reported in this artifact were
dubious (see additional comments). However, the contribution of the
turniness metric stands on its own despite

2

0x55109bffa0d8acd1effc245a68a64a49bdf6f66eded5c218ca35ea5a099a25a8

the errors in the data. We encourage the author to build on their
turniness metric to produce metrics for difficulty and author name,
two values which appear to be more subtle than turniness based on the
present dataset.

We also commend the author for encouraging the evaluation committee to
get up and move to the groove.

ADDITIONAL COMMENTS:

• The arithmetic facts cited in this evaluation are currently being
formalized in Coq, but as of publication time the proofs remain
incomplete.

• Some of the difficulty ratings seem quite dubious, most notably:

Name: DDR 1^st Mix to EXTREME/Last Message/Last Message.sm Rating:
Challenge

Steps: 2

Name: In The Groove Rebirth +/Sounds of Life/Sounds of Life.sm Rating:
Beginner

Turniness: 1.2931

• The following tracks have foot ratings of "Challenge," "Easy,"
"Hard," or most surprisingly, "Edit":

CuoReNeRo MeGaPacK/Return of Salieri (Dukamok)/Return_of_Salieri.sm
CuoReNeRo MeGaPacK/DeathMoon (Braintrust)/DeathMoon.sm fort rapids
vii/(12) Be OK/Be OK.sm

rocky mount xi/(12) Be OK/Be OK.sm

In The Groove Rebirth +/Welcome to Rainbow -hardstyle remix- /Welcome
to Rainbow (Hardstyle Remix).sm

CuoReNeRo MeGaPacK/Omega/omega.sm

CuoReNeRo MeGaPacK/Return of Salieri (Dukamok)/Return_of_Salieri.sm
CuoReNeRo MeGaPacK/Since 1983 (DukAmok)/Since_1983.sm

CuoReNeRo MeGaPacK/DeathMoon (Braintrust)/DeathMoon.sm

• 64 tracks had foot ratings exceeding the claimed maximum of 20, with
some reaching as many as 80085.

• The hardest Medium track had a difficulty of 21, in excess of the
claimed maximum • The hardest Easy track had a difficulty of 19, also
very close to the limit

3

0x59cf034c27459535b3ae6906a98c9aec87cca878f8865dd6c9e99c2af4c5fcfb

• A prolific author named "" authored almost 2000 songs, nearly a
fourth of the dataset. This seems worthy of mention in your paper.

• Only 1187 tracks are possible with two feet, and out of those only
972 are possible with one foot - I'm concerned about the accessibility
of ITG to disabled people with only one leg. There were 0 tracks that
could be done with 0 feet!

• Why are both of the turniest tracks listed Easy?

• Even for a paper focused on turns rather than RAMs, I would have
expected a DDR2 spec ification citation at a bare minimum, yet there
wasn't even a reference to the original DDR spec. Remember to do a
sufficiently extensive literature search: if it wouldn't put the sig
nificant prestige of this conference in jeopardy, I'd personally
threaten to reject any of your subsequent submissions that was guilty
of such an omission.

4

0x664749275fef50b1918c91b7c80b96e88b026764e033cd91ff1e14dc2b0b4ee8

0x33d6b42b5a07b84648ee90dc6d2e5374426457978f5f61340c56e0c09764225d

Lamb track

Languages: Human and... Inhuman

13 Destructive Logic

Runming Li

Keywords: logic, constructive logic, destructive logic, type theory

14 Overlap-Maximal Graph Labelings: Graph Labelings with Non-Disjoint
Vertex and Edge Sets (and how they can be used for encryption, poetry,
and breaking mathematics)

Gabriel Chuang

Keywords: Graph Theory, Cryptography, Fox in Socks by Dr. Seuss 15
Neo-classical Logic: Une Logique non classique

Martin Vassor and Fangyi Zhou

Keywords: Logic, Meta-Metatheory, Law of Excluded Middle, Law of
Contradiction, Decidability, Macron

16 A Patriotic Analysis of Programming Paradigms

Jacob Weiner

Keywords: Patriotism, Constitution, Dependent Type Theory 17 On
Ruinment: Ruination Theory and its Consequents

Luna Tascheter

Ruination Theory, Ruinment, T0T4L PWN4G, Category Theory, Adam
Conover, Adam Sandler, Hallmark, Waste of Pa

per, Orange

0x5624027ece7ed2c355a33d1d07f4b41a0d8dea6b6dc0b340b7cda45a5a49e7ca

0x9afe6f465692537078c0057438b57585c9e90bb0023f8e47d0b429bcb76cb332

Lambda Doge: A digital canine 8

language

Joshua Suereth

March 11, 2016

Abstract

Lambda Doge is the first programming language designed specifically for
canine implementers. By applying the known simplicity of lambda calculus
to the known structure of canine utterances, we are able to create a
programming environment that is both elegant and turing complete.

1. Motivation

According to a 2012 report by the world health organization^[1]:

... estimates that there are around 78 million owned dogs in Africa, but
that there may also be in excess of 70 million ​unowned, stray dogs as
well.

According to a random quora infographic, there is an estimated 17
million programmers in the world^[2].

If we had the opportunity to teach all stray dogs in Africa how to
program, then this would have profound impacts, including:

● Less strain on the economy from freeloading pooches

● New \"outsourcing tech mecha\" in africa from low­cost high­quality
canine coders ● Estimated 400% growth in computer book sales

So, there is a lot of reason to design a programming language for dogs.
0xf55fe380dea3479d86048a5744b9578204024fed6ff935532744da436bb0b715

2. Language design

Designing a language for dogs is quite hard. First we decided to take
some of the best aspects of human­oriented programming languages and
ensure that these elements also are there to assist dogs:

● Statically typed​. To err is human, but typing is also unnatural
for canines. We expect having a compiler with static types will
dramatically help cut down on typos and errors in code.

● Type inference. ​While static typing can dramatically reduce
errors, having to enter more keystrokes is certainly not dog friendly.
The language should attempt to infer as much meaning from expressions
as possible.

● JVM­backend.​Java remains one of the top used/known languages
for college grads. By designing a java­friendly language, we allow
dogs easy access to the job market.

Let\'s look at a simple \"Hello, world\" program in lambda­doge:

WOW

main

MUCHPrintLn

\"WUF\"!

As can be clearly seen, the syntax and style of this program are
completely natural to the language of doge, as discovered via internet
memes.

3. Grammar

Every lambda doge program is built using expressions. Expressions are
one of: Let­expressions, Lambda­Expressions, Apply expression,
Identifier references or literals.

A lambda doge let expression is used to define a function, and looks
as follows:

WOW \<name>

SUCH \<optional forced type specification>

SO \<argument name list>

0xebe467d381a81cd58681171bc4de991c67ce565cca12a945db0f5c1d9ed783ea

VERY \<body­expression>

Functions optionally take both arguments and types for the arguments.
If types are specified, they must be specified for all arguments. If
argument names are specified, the values of these arguments can be
referenced within the body expression. Let\'s compare Lambda Doge to
the more human­friendly Haskell:

Lambda Doge Haskell

WOW Inc

SO x

VERY Plus x 1 !

WOW Inc

SUCH Int => Int SO x

VERY Plus x 1 !

Inc x = Plus x 1

Inc :: Int ­> Int Inc x = Plus x 1

Lambda doge also has lambda expressions, otherwise known as function
literals. These look as follows (with comparisons to scala):

Lambda Doge Scala

MANY friends

VERY Happy friends !

{ friends => Happy(friends) }

The MANY keyword denotes a function literal is coming. All identifiers
preceding the VERY keyword denote how many arguments the function
literal takes.

We list a more complete lambda doge grammar for those interested in
implementing their own.

Lambda­Doge Grammar

expr := let­expr | lambda­expr | ap­expr | literal | id­ref
let­expr := \'WOW\' \<identifier> type­list? arg­list? Ap­expr
type­list := \'SUCH\' \<type>

arg­list := \'SO\' \<identifier>*

0xfd5dd2c567f1a2192dd8787b49feb846507ed5f99d733c4b36291d50a32215c4

lambda­expr := \'MANY\' \<identifier>* ap­expr

ap­expr := (\'VERY\' | \'MUCH\') id­ref expr* \'!\'

id­ref := \<identifier>

literal := \<int­literal> | \<boolean­literal> |

\<string­literal>

4. Type System

The Lambda Doge type system attempts to blend power with simplicity,
enabling canines the fastest possible ramp­up time to programming as
possible. The type system is composed of two types:

1. Type constructors: T[a], T

2. Type variable: a

A Type constructor can have no type arguments associated with it. In
this case it is known as a simple type, and is considered
\"complete.\". Most literals in the language are typed into simple
types:

Literal Type

Integer literal Int

Boolean literal Bool

String literal java.lang.String

Functions are encoded in the language as curried instances of the type
constructor Function[_,_]. Lambda doge provides a convenience
syntax for function types, using the => literal. This allows breaking
the type constructor into argument + result pairs, leading to a more
haskell­looking type syntax. The following table shows examples:

Function Type Abbreviated

WOW Inc

SO x

VERY Plus x 1 !

Function[Int, Int] Int => Int

Plus Function[Int, Function[Int, Int]]

Int => Int => Int

0xcf9d6a529f028dfcfb9a820487672721d7d98917810c4769d69560e9d45d8cd5

Lambda Doge performs type inference by running the hindley­milner­like
type inference algorithm locally against each let expression. If no
type is isolated, then the type will remain as a type variable. In
lambda doge, all types that start with a lower­case letter are
considered \'variables\' which may contain any type.

For instance, lists in Lambda doge are encoded as follows:

List function Type

Nil List[a]

Cons a => List[a] => List[a]

So, when constructing a list, the first element defines the type of
the list, e.g.

WOW mylist

VERY Cons 1 Nil !

Will infer the type of mylist to be List[Int].

One complication is how to represent Java types in Lambda Doge. While
static java methods can be mapped directly to lambda doge functions,
there is the issue of how to handle methods. We use an old trick of
defining methods as static functions which take the instance of the
class as the first argument. Here\'s some example mappings:

Java Method Java Qualifier Type

java.lang.Object#toString java.lang.Object => String

java.lang.String#charAt java.lang.String => Int =>
java.lang.Character

java.lang.Integer#MAX_VALUE static Int

java.lang.Integer#parseInt static java.lang.String => Int

Currently the type system does not take into account inheritance. We
think open recursion is hard enough for humans to understand and wish
to spare our canine friends. However, as time progresses, we believe
there may be opportunity to explore a simple way of allowing \"foreign
types\" to have full object oriented semantics, well preventing most
of the headaches associated with such semantics and type inference.

0x412572ca2f24b309a9ac827882bd6245cd7b70893826c5f9688aabbf267ceb6b

5. Backend

The backend of lambda doge compiles all lambda doge files into Java
.class files. The mapping is done as follows:

● All .doge files are compiled to a single .class file of the same
name

● All let­expressions defined within the file are encoded as static
methods of the same name.

● Any let expression named \"main\" is encoded as a \"main\" method,
as used by the Java Virtual Machine (JVM) to run a program. I.e.
Lambda­Doge will force the type of the main let expression to conform
to Java main standards.

Additionally, as closures are not natively supported (at the JVM
level), Lambda Doge performs \"lifting\" of static method into
java.util.Function\<?,?> instances.

Here is an example:

WOW four_in

SO a b c d

VERY Plus a

MUCH Plus b

SUCH Plus c d ! ! !

WOW closure

SO captured

VERY four_in captured !

The first function, four_in, has a type Int => Int => Int => Int
=> Int, which takes four inputs before returning a value. In Lambda
Doge, functions are values and can be returned. The function called
closure has a return type of Int => Int => Int => Int, which means
it returns a function which will take three inputs before returning a
value.

Encoding this on the JVM is tricky because the JVM makes a distinction
between methods and objects. Methods are defined against objects and
only methods perform behavior. Objects define data, and only objects
can be passed or returned as values. Therefore treating a function as
both behavior and data is not entirely native.

However, Java 8 now defines a java.util.Function\<?,?> interface, as
well as a LambdaMetaFactory that can be used to construct
object­instances of this interface using methods. The
LambdaMetafactory can take a set of \"bound\" arguments, a method
handle and will construct a function object which can be returned. To
make use of this, given the natural currying in Lambda­doge, we must
adapt all instances of code where we must return a function object
such that these instances only pass one value into a static method at
a time. To solve

0x95718350626f7c39c7a1665a103947e516aa8fe5cdb5e63b20cd0c5ca4799c28

this, we introduce an AST transformer that will expand any partial
function application into N let expressions, where N represents the
number of unbound arguments. Here\'s an example.

Phase Pseudo­Ast

Parse let four_in(a,b,c,d) = Plus(a, Plus(b, Plus(c,d)))

let closure(captured) = four_in(captured)

Lambda Lift let four_in(a,b,c,d) = Plus(a, Plus(b, Plus(c,d)))

let closure$four_in$1(a, b, c) = four_in(a,b,c)

let closure$four_in$2(a, b) = four_in$1(a,b)

let closure(a) = four_in$2(a)

The runtime is then able to appropriately call either the static
method for the let expression, or is able to call the apply method
defined on the java.util.Function instance, appropriately.

A second complication in the backend is over boolean logic. While most
of lambda doge is evaluated eagerly, it is a common optimisation when
dealing with boolean if statements to avoid computation for one of the
branches of logic. As such, Lambda Doge provides built­in function
\"ifs\" having type Bool => a => a => a. Here, the first argument
is a boolean condition. The function returns either the second or
third argument, depending on whether the boolean condition is true or
false. As an optimisation, this built­in function will avoid
evaluating the expression for the second and third arguments until
after checking the boolean condition.

Generally the lambda­doge backend is quite simple, and most of the
features map quite naturally to JVM bytecode, as the bytecode is stack
based.

6. Standard Library

Currently lambda doge comes with a minimal standard library, for use
in prototyping[3]. Here\'s a table of all functions currently
defined:

Function Type

tuple2 a => b => (a,b)

fst (a, b) => a

0x3e8cc15811ba2846313987025d2ba95c68639be63bac6dd3bce3abbcd33feb7c

snd (a,b) => b

Nil List[a]

Cons a => List[a] => List[a]

hd List[a] => a

tl List[a] => List[a]

Plus Int => Int => Int

Minus Int => Int => Int

Multiply Int => Int => Int

Divide Int => Int => Int

ifs Bool => a => a => a

7. Future Work

The language cannot be considered complete until pattern matching has
been implemented in an elegant way. As you may know, dogs are
excellent pattern matchers. Here is a common pattern match from a
popular dog AI[4]:

defnext_action(in:SensoryInput):Action=

inmatch{

caseSee(SomethingThatMoves())=>bark

caseHungry()=>bark

caseFullBladder()=>whine

caseNothingifNotSeenOwner=>whine

caseNothing=>sleep

}

We envision adding this to lambda doge using a haskell­style encoding
of multiple let­expression definitions with the same name yielding a
single physical let expression, where the arguments define the
patterns, However given the nature of lambda­doge, the elegance of
this approach is dubious, leading to much discussion within the canine
community of the best way to bark at things which move.

0x4551deac5bff00c0e0f8caa2853565f333a72885a0110b16f9e11c2b690e4a3c