Sigbovik 2015#

7+( $662&,$7,21 )25 &20387$7,21$/ +(5(6\< 35(6(176

$ 5(&25\' 2) 7+( 352&((\',1*6 2)

6,*%29,.

7KH QLQWK DQQXDO LQWHUFDODU\ URERW GDQFH SDUW\ LQ FHOHEUDWLRQ RI
ZRUNVKRS RQ V\PSRVLXP DERXW 2⁶WK ELUWKGD\V LQ SDUWLFXODU WKDW RI
+DUU\ 4 %RYLN

&DUQHJLH 0HOORQ 8QLYHUVLW\

3LWWVEXUJK 3$

$SULO

{width="6.168665791776028in"
height="1.0470002187226597in"}

SIGBOVIK

A Record of the Proceedings of SIGBOVIK 2015

ISSN 2155-0166

April 1, 2015

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

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.

SIGBOVIK 2015 {width="0.950333552055993in"
height="0.9520002187226597in"}

Message from the Organizing Committee

You hold in your hand the proceedings for SIGBOVIK 2015. Or, more
likely, you're looking at them on a screen because you're too cheap to
actually buy the proceedings. Either way, we thank you for your
interest, but we thank you considerably more if you've demonstrated
your interest by giving us money. As is traditional, we begin the
proceedings with a message that nobody will read, but which must
nonetheless be included because we don't want to give any of our
authors the satisfaction of having their paper start on page 1.

We are proud to announce that SIGBOVIK has experienced a surge in
interest in recent years. As can be seen in Figure 1, the number of
submissions grew exponentially¹ from 2012 to 2014. We don't consider
the number of submissions for 2015 here, because this message comes at
the beginning of the proceedings and we wouldn't want to spoil the
surprise. More people have been giving presentations, and attendance
has been thriving. Of course, we don't keep numeric records of these
facts, because that requires organizing, and does the SIGBOVIK
organizing committee look like some group of people who are interested
in organizing things?

{width="4.695333552055993in"
height="2.813665791776028in"}

Figure 1: y = 2 × 10³⁶e⁻^0*.04*x, where y is the number
of submissions and x is the year. Yeah, this graph was made in
Excel. So what?

¹Exponential decay is just exponential growth with a negative
exponent, right?

Because of these vast leaps in size, SIGBOVIK has reached that point
in every young conference's life where we must consider splitting the
talks into tracks to save time. Because time is money and all that.
However, we at SIGBOVIK feel strongly that all attendees should be
able to experience the full range of exciting research that SIGBOVIK
has to offer, and so it is with great pleasure that we announce
several proposals for creating two parallel tracks.

Two concurrent presentations. Two presenters stand at opposite sides
of the front of the room and give talks concurrently. Audience members
can sit closer to whichever presenter interests them more. For
example, an audience member could give 25% of his or her attention to
Presenter A and 75% to Presenter B by sitting one-quarter of the way
to Presenter A's side of the room. Both presenters will display their
slides, because the auditorium conveniently has two screens at the
front of the room. We're not sure if they can show video from two
different laptops, but this seems like a technical detail.

Two concurrent presentations - in 3D! As above, two presenters stand
at opposite sides of the front of the room and give talks
concurrently. However, we leverage advanced 3D technology to ensure
that all audience members can fully appreciate both talks. Each
audience member is given a pair of colored 3D glasses. One presenter
wears red. One presenter wears blue. Their slides are colored
accordingly and overlayed on one screen. The audience members' brains
will correctly interleave the two presentations to form a coherent
narrative. If the two presentations are in different fields, this
probably opens us up to all kinds of funding for interdisciplinary
research. We should look into that.

Timeslicing. Did you know that before your desktop had eight cores, it
had only one, but you could still run multiple programs? This was
accomplished through timeslicing. In the same way, two presenters
can give talks concurrently by alternating slides. If this granularity
is too high to achieve reasonable latency, the presenters could try
alternating sentences, words, syllables or phonemes. The possibilities
are endless.

Question-and-answer optimization. Frequent attendees of academic talks
will notice that pre senters spend approximately half of their total
time answering questions, either during the desig nated
question-and-answer period at the end of the talk, or when interrupted
during the talk. A further observation is that attendees of talks are
generally interested in asking questions or listen ing to the talk,
but not both. We take advantage of these observations by having
Presenter A give a talk and then answer questions, as usual, and
Presenter B answer questions first and then give the talk. This may
seem strange, but is really no different than normal because questions
typically have little or no relation to what was discussed in the
talk. This format has the benefit that those who wish only to ask
questions can spend the entire session doing so, and those who wish
only to

hear talks can spend the entire session doing so. Additionally, both
presenters are able to give their talks uninterrupted because anyone
who would interrupt with questions is busy asking questions of the
other presenter.

Of course, there is no reason to limit ourselves to two tracks, but
the above solutions clearly generalize to n-track conferences, in
the standard way. We hope to roll out one or more of these exciting
developments for SIGBOVIK 2016 (not SIGBOVIK 2015, because we're lazy
like that). And, with that, onto the proceedings!

7DEOH RI &RQWHQWV

7UDFN ; /RFDOO\ 6RXUFHG /RYLQJO\ +DQGUHVHDUFKHG LQ\'50 &RS\ &RQWURO
ZLWK D 3HUVRQDO 7RXFK $ +DQG +HOG \'HYLFH IRU 8VHU LQ WKH ORRS 3ULQ
WLQJ $UWLVDQDO 7\SH 7KHRU\ $ &RQVWUYFWLYH 6ROYWLRQ WR WKH .RHQLJV
3LWWVEYUJK %ULGJH 3UREOHP

7UDFN \< 2QH 3DSHU 7ZR 3DSHU 5HG 3DSHU %OXH 3DSHU 5HG L 5HPRYDO ZLWK
$UWLILFLDO 5HWLQDO 1HWZRUNV $ 3URRI RI WKH 7ZHOYH &RORU 7KHRUHP +H\
1RERG\ %RWKHUHG %HIRUH 9LVXDOO\ ,GHQWLI\LQJ 5DQN 7UDQVSDUHQF\
5HSRUW

7UDFN / /XQFK ,QWHUPLVVLRQ

%XUULWRV IRU WKH +XQJU\ 0DWKHPDWLFLDQ

7UDFN = &RPSXWDWLRQDOL]LQJ &RPSXWDWLRQ

$ 1HZ 3DUDGLJP IRU &HUWLILHG &RGH %H\RQG WKH +DOWLQJ 3UREOHP +LJKHU
2UGHU ,QILQLWH /RRS &KHFNHUV %DVKLQJ +DVNHOO 5HLPSOHPHQWLQJ WKH 3DUVHF
/LEUDU\ ,QVLGH WKH 8QL[ 6KHOO

7UDFN : /DVW 3HULRG +RQRUV (QJOLVK &ODVV 3URJUDPPLQJ /DQJXDJH )DQ
)LFWLRQ $FURQ\P\ $ %LGLUHFWLRQDO \'LFWLRQDU\ $QRWKHU $UWLFOH
WKDW 0DNHV %LEOLRPHWULF $QDO\VLV D %LW +DUGHU &RPPHQW 6,*%29,.
6KRXOG %DQ &RQFOXVLRQV 7KH 3RUWPDQWRXW

7UDFN ;

/RFDOO\ 6RXUFHG /RYLQJO\ +DQGUHVHDUFKHG

LQ\'50 &RS\ &RQWURO ZLWK D 3HUVRQDO 7RXFK

0LJXHO /HFKRQ

.H\ZRUGV \'50 LQGHSHQGHQW JDPH GLVWULEXWLRQ VRIW FU\SWRJUDSK\

$ +DQG +HOG \'HYLFH IRU 8VHU LQ WKH ORRS 3ULQ WLQJ -DPHV 0F&DQQ DQG
1RWUHDO $XWKRU

.H\ZRUGV XVHUV ORRSV SULQWLQJ XVHUV LQ ORRSV SULQ WLQJ

$UWLVDQDO 7\SH 7KHRU\

&DUOR $QJLXOL

.H\ZRUGV W\SH WKHRU\ DUWLVDQV KXPDQ FRPSXWDWLRQ

$ &RQVWUYFWLYH 6ROYWLRQ WR WKH .RHQLJV 3LWWVEYUJK %ULGJH 3UREOHP *UHJ
+DQQHPDQ DQG %HQM %OYP

.H\ZRUGV .%3 .3%3 SLWWVEYUJK VRYWK VLGH LQ RUGHU WR KRQH\ WKHPVHOYHV
WKDQNV JRRJOH WUDQVODWH

inDRM: copy control with a personal touch

Miguel Á. Lechón*^∗*

April 1, 2015

You say "I'll just make a copy for me and a friend", but he'll make
one and she'll make one and when will it end?

Don't copy that floppy

MC Double Def DP[1]

Abstract

inDRM is a digital rights management scheme. The goal of inDRM is
ensuring that a small amount of human reflection accompanies the process
of creating and distributing each new copy of a given piece of software.
It is partic ularly well suited for developers that expect lots of
passion but little money from their users, such as independent game
developers. Noteworthy properties of inDRM are its:

• Broken by Design design.

• P2P activation key generation.

• Distribution history record keeping.

Reference implementations and usage ex amples are available here¹.

*^∗*e-mail: miguel.lechon+inDRM@gmail.com
¹https://github.com/debiatan/inDRM

1 Motivation

1.1 A brief history lesson

Home taping killed music thirty years ago due to music being
distributed as passive, readily cloneable data. Too little was done to
rem edy this, and too late[2]. Computer software, in contrast, and
by its own nature, needs to be active to fulfill its intended purpose,
so, through the use of DRM, video games can choose to be as
passive[3], aggressive[4] or passive-aggressive[5] as they so
desire. This is the main reason why we have games, but not music,
today.

1.2 Danger lies ahead

The current dominant threat to the computer game industry is not so
much economical as it is ecological. Shastri, Morrison and White
provide a concise explanation in their recent discussion[6]:

It's a total SNAFU! Adults buy all kinds of games but never play them.
Kids have time to play but behave like monomaniacs. . . Minecraft
this or LoL that, day in, day out!

Soon we will all realize there are no gamers left. And when the
bubble bursts, the reeking corpses of un played Steam libraries will
wash this industry away.

Indeed, according to undisclosed sources at Valve, the average library
backlog (bought but unplayed games) amounts to 83% of the total number
of titles each user owns[7].

1.3 Danger knocks at the door

The vast majority of game developers do not see financial return as an
end, but as a way of measuring the engagement of players to their
games. However, in today's prosperous eco nomical climate, money is
essentially thrown at the feet of game developers for no appar ent
reason, tricking them into thinking they are succeeding when, in all
likelihood, no one is playing their creations.

A recent example is the case of the Hand made Hero project[8], where
one programmer with no previous history of ever completing a commercial
video game announced his plans of working five hours per week on a
yet-to-be started title. He successfully collected thou sands of
preorders during the course of the following weeks.

Will this summer last much longer? Won't some brilliant academic mind
devise a clever way of avoiding this impending disaster? How can
cautious game developers gauge the real commitment of their user base
when all signs indicate they are doing a splendid job?

The answers to these questions are no, yes and read on.

1.4 Fear no more

The solution, of course, lies in the repurpos ing of the industry's
proven old savior, DRM. As long as money keeps growing on the trees of
developer's backyards, the amount of game copies sold will be an
inaccurate measure of consumer acceptance. Instead, I propose making
players spend an ultimately much more valuable resource than money:
their time. In order to achieve this, and as a condition to unlock the
game, the user will be forced to engage in a short social exchange
with either the creator of the game or some other fellow player.

By slightly inconveniencing potential clients, creators can expect to
gain a clearer understanding of the appeal of their games and end up
with a much more committed, albeit smaller, user base.

2 Cryptological interlude inDRM's strength rests on:

• the solid foundation of the MD5/4 cryp tographic hash function

• the RSA public key cryptosystem signing procedure [10] with a key
length of 32 bits

• the identification of computers via the MAC addresses of their
primary network interfaces.

This section consists of a rather in-depth review of the first two
algorithms.

2.1 MD5/4

MD5[9] takes an arbitrary string of charac ters, passes it through a
deterministic blender and produces an unnecessarily long 128-bit value.

MD5/4 takes that value, chops it into four 32-bit pieces and XORs them
together to pro duce a more digestible 32-bit digest.

2.2 RSA signatures

The RSA signature procedure is a popular party trick from the late
1970s, where one person comes up with three numbers n, d and e that
satisfy the following property:

(x^d)^e ≡ x (mod n), ∀x ∈ Z ²

That person then makes n and e public, spends a few minutes teaching
modular expo nentiation to the crowd and claims to possess the ability
to:

• Turn any message into a number x (using a scheme similar to MD5/4)

• Produce a number y that depends on x and that acts as that person's
signature of the message, fact which can be verified by checking that:
y^e ≡ x (mod n)

Of course, behind the scenes, the enter tainer obtains y by raising x to
the dth power, dividing the result by n and taking y to be the remainder
of that division.

The process of finding the three initial numbers is demonstrated in
[11] and can be

² Which translates into Pythonist parlance as: (pow(pow(x,d,n),e,n)
== x) == True for any integer value of x

easily accomplished today with the help from the time-tested software
package openssl[12] by issuing the following command in any
POSIX-compliant operating system:

openssl genrsa 32|openssl rsa -text³

Looking at its output, the modulus field is equivalent to our n,
publicExponent denotes e and privateExponent indicates d.

3 Guided tour

Any person in possession of an unlocked in stance of a game protected
by inDRM can un lock copies for other potential players, as long as
those copies descend, directly or indirectly, from that same unlocked
instance.

There are several distinct phases in the dis tribution of a game
protected by inDRM:

• Author A of a game generates a root ac tivation key file and
distributes it along with the game

• Potential player P obtains the game, tries to run it and is
invited by the software to generate a request file and send it back
to author A as a precondition for playing

• Author A receives the request file, throws a small party and
generates a response file for player P that becomes a valid ac
tivation key file

• Player P plays the game, finds it worth while and hands a copy
to friend F

³It is fashionable to use 2048 instead of 32, prob ably in reference
to the homonymous video game[13]

• Friend F tries to run the game and is invited by the software to
generate a re quest file and send it back to either A or P as
a precondition for playing. F chooses to contact P

• P generates a response file for friend F, by virtue of
possessing a valid activation key file belonging to the same key
chain that reached F

• ...

The rest of this section reviews the techni cal details behind the
generation of key files.

3.1 Root activation key file

The creator of the game generates a root ac tivation key file and
distributes it with every copy of the game. In and of itself, that key
file only allows the game to be played on the developer's computer.
However, it provides the basis for the generation of key requests from
potential players.

Here is an example of an inDRM root acti vation key file:

========== inDRM key file =========== game: Adventures in inDRMland
===================================== nick: debiatan

location: Barcelona

date: 2015/04/01

notes: Enjoy!

mac_salt: 1e6c40ea

mac_hash: 76f0da12

hash: c738b172

signature: d38cc9a

Inside key files, lines starting with an equal sign are ignored. The
rest are composed of a tag, followed by a semicolon and a value field.
The tags and their associated functions are these:

game: Title of the game

nick: Author's name or nickname

location: Author's place of residence

date: Date of creation of the key file (in yyyy/mm/dd format)

notes: Notes from the author

mac_salt: Random 32-bit hex number

mac_hash: MD5/4 hash of the concate nation of mac_salt and the
hexadeci mal representation of the MAC address of the primary network
interface of the computer generating the key file

hash: MD5/4 hash of the concatenation of: the preceding
signature in the key chain (assumed to be "0" in case of the master
key file), game, nick, location, date, notes,
mac_salt and mac_hash

signature: RSA signature of hash (computed as (hash*^d* mod
n), where d and n have been generated along with e as discussed
in section 2.2).

For the particular example used in this sec tion, the values of the
cryptographic param eters are:

• n (modulus): 3333098473

• e (public exponent): 65537

• d (private exponent): 939472245

These values are to be embedded in the inDRM routines present in the
game. The pair (e, n) will be used as an RSA public key in order to
check signatures present in side key files. The pair (d, n) will allow
a registered copy of the game to sign key file requests from new
potential players through an in-game menu option labeled to that ef
fect.

3.2 Activation key file

validation

Every time a piece of software guarded by inDRM is run it reads the
activation key file and checks that:

• the value of the hash field is correct (by recomputing it using
the tag values that precede it)

• the value of the signature field is cor rect (by ensuring that

signature*^e* mod n = hash)

If these two conditions are met, the pri mary MAC address of the machine
is checked to see if it satisfies:

[MD5]{.underline}

₄ (mac_salt*_i* + MAC) = mac_hash*_i* (where the '+' sign
indicates concatenation of strings) for any
mac_salt*_i/mac_hash*_i pair present in the file. If it
does, the game is allowed to run. Otherwise, the user is invited to
generate a request file.

3.3 Request file generation

An invitation to generate a request file will essentially convey a
message similar to this one:

*** Last MAC address on key file does not belong to this computer
*** You won't be able to play this game unless you convince another
player to generate a key for you.

Let's build a request file...

Please provide the following data (or press 'enter' to skip):

Name (or nickname): _

Location (place of residence): _ Notes (message to future players): _

After providing (or failing to provide) the three pieces of information,
inDRM collects the date and MAC address of the system, gener ates the
request file and tells the user that:

A request file has been generated here: *** /home/ ... /request.txt
***

In order to finish the registration process, send that file back to
whoever shared the game with you. That person will be able to unlock
your copy.

Think twice before sharing this game with other people. If they ever try
playing it, they might come back asking you to register their copies.

The request file consists of a copy of the original key file distributed
with the game with an extra section appended at the end. Imagining that
the original key was the one presented back in section 3.1 and the user
provided "miguel", "barcelona" and "this

sucks" as values for name, location and notes,
respectively, the resulting extra sec tion could look like:

nick: miguel

location: barcelona

date: 2015/04/01

notes: this sucks

mac_salt: 95be1f47

mac_hash: 6051a20a

hash: 1f495ce2

signature: NO SIGNATURE YET

In order to run the game, the potential player will then send the
request file up the distribution chain for it to be signed.

3.4 Response file generation

The example activation chain we have de scribed consists of only the
original author of the software and its first user. The request file
will then be necessarily sent to the au thor, who will execute a
registered copy of the game and select the option that allows to sign
requests. That routine will check that:

• the values of all hash fields are correct (by recomputing them
using the values of fields preceding it)

• the values of all signature fields, except for the last one, are
correct (by ensuring that (signature*^e* mod n = hash))

• the primary MAC address of the com puter satisfies:

[MD5]{.underline}

₄ (mac_salt*_i* + MAC) = mac_hash*_i* for some
mac_salt*_i/mac_hash*_i pair in the request file.

If all three conditions are met, the last signature field of the
request file will be completed with the help of the private ex ponent
d and the modulus n:

signature = hash*^d* mod n

In our example, this would mean modifying the last signature of
the request file to read:

signature: 9bc727d0

The resulting file will then be sent back to the potential player to
be used in place of the original activation key file. The potential
player will then stop being just potential and start a new life as
a real player.

4 Properties

Improving security typically means degrad ing usability.
Providentially, both effects are intended consequences of the use of
inDRM.

There are several other desired properties that have gone into the
design of the inDRM copy control scheme. This section discusses them
briefly.

4.1 Broken by Design design

If we were to depict the concept of security as a one-dimensional
horizontal segment de limited on the left by the word insecure and
on the right by the word secure, inDRM would lie definitely to the
left, in a place probably labeled as cryptographically annoying.
Sadly, space limitations preclude even a cursory ex ploration of all
the security flaws exhibited by inDRM.

bined notes sections of a key can be used as

a simple guestbook or, perish the thought, a

space for advertisements.

Another more elaborate use requires us to

picture the set of activation key files associ

ated to a particular game as a tree, its leaf

key files being the ones that carry the most

information. Getting hold of a sizeable per

centage of those files by some means⁴, would

facilitate the identification of the principal

hubs in the game's distribution network.

4.5 Simplicity

MD5 is straightforward to program[14]. The

improvements that MD5/4 introduces come

at the cost of three extra XOR instructions.

Implementing the standard RSA algorithm

would require working with arbitrarily long

integers, but the 32-bit version of it does not

impose that hardship on game developers.

Two additional benefits of working only with

32-bit values are that key files become smaller

in size and that they fit inside the two-column

layout of this article.

4.6 Involvement of players

In order to acquire a valid activation key file,

the potential player must secure the collab

oration of another player. After implicating

that other person, the new player may feel

pressured to give the game a proper try and

avoid dropping it after just a few minutes of

play.

⁴such as asking nicely or offering players extra

game content in exchange for their keys

4.2 P2P key generation

Players of games protected by inDRM can rest assured that they will be
able to enjoy them for as long as they are interested in doing so. The
absence of network authentication and the distributed nature of the key
generation process guarantee that.

Moreover, as a side benefit of the dis tributed nature of the key
generation scheme, players might derive some sense of belong ing to a
community by simple inspection of the contents of their personal key
files. Intensely imaginative players, of the kind that take pleasure in
trading Steam inventory items, may even experience inDRM's compul sory
chaining of signatures as a tradition that makes them part of a lineage.

4.3 Lack of attractive as a cracking target

All DRM schemes are eventually subverted, so one should not ask if but
when will inDRM be broken. I suspect that it will not happen any time
soon for mainly two reasons:

• Breaking inDRM poses no challenge, so no one can take pride on that
endeavor

• The only benefit to be derived from breaking inDRM is the avoidance of
a short social interaction

4.4 Distribution history record keeping

Key files have potential uses other than game distribution control. For
instance, the com

4.7 Future-proof architecture

As long as one registered copy of the game re mains, it will continue
to be redistributable and playable. Even if no registered copy re
mains and even if the game binary proves dif ficult to crack,
bruteforcing the signature of a request file requires just the
testing of the set of 2³² possible signatures.

5 Conclusion and final remarks

Game developers do not need protection from software pirates; they
need instead to be guarded from the uncaring capricious money throwing
player hordes that endanger their profession. By choosing to
distribute games guarded by inDRM, they are not only decid ing to
acquire a much more mature following, but are also telling the video
game commu nity that they care.

For an up-to-date list of games that use inDRM, check:

http://blog.debiatan.net/inDRM.html

References

[1] MC Double Def Disk Protector, Don't copy that floppy⁵, 1992

[2] Sony BMG copy protection rootkit scan dal⁶, Wikipedia

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

up863eQKGUI

⁶https://en.wikipedia.org/wiki/Sony_BMG_
copy_protection_rootkit_scandal

[3] Good Old Games⁷

[4] Always-on DRM⁸, Wikipedia

[5] DRM -- Software tampering⁹, Wikipedia

[6] S. Shastri, R. T. Morrison, and X. White, More games, less
time. Journal of Bad Omens, vol. 35, pp. 75-80, Dec. 2012.

[7] "Undisclosed" means "undisclosed". [8] Handmade Hero¹⁰

[9] R. Rivest, The MD5 message-digest algo rithm, RFC 1321, April
1992.

[10] R. Rivest, A. Shamir an L. Adleman, A Method for Obtaining
Digital Signatures and Public-Key Cryptosystems, Commu nications of
the ACM 21 (2): 120--126. February 1978.

[11] RSA encryption and decryption, a worked example¹¹,
Wikipedia

[12] OpenSSL¹², Wikipedia

[13] 2048¹³, Wikipedia

[14] MD5 pseudocode¹⁴, Wikipedia

⁷http://www.gog.com/

⁸https://en.wikipedia.org/wiki/Always-on_ DRM

⁹https://en.wikipedia.org/wiki/Digital_
rights_management#Software_tampering ¹⁰https://handmadehero.org/

¹¹https://en.wikipedia.org/wiki/RSA_
(cryptosystem)#A_worked_example

¹²https://www.openssl.org/

¹³https://en.wikipedia.org/wiki/2048_(video_game)

¹⁴https://en.wikipedia.org/wiki/MD5# Pseudocode

CONFIDENTIAL COMMITTEE MATERIALS
{width="0.9486668853893263in"
height="0.9486668853893263in"}

SIGBOVIK 2015 Paper Review

^{Paper 1: inDRM: copy control with a personal} touch

Chris Martens

Rating: 2 (destroy all games)

Confidence: 4/4

The copy protection scheme described in this paper ostensibly poses a
solution to a threat to the video games industry. As such, I cannot
sanction it as a good idea. Also, the paper is eight pages long and
had a lot of boring stuff about crypto in it.

On the plus side, the "Broken by Design" design seems like a useful
feature.

A Hand-Held Device for User-in-the-loop Prin-ting

James McCann*^∗* TCHOW

Notreal Author

WeAreWe University

{width="2.785333552055993in"
height="1.895333552055993in"}{width="2.0520002187226596in"
height="1.900333552055993in"}

Figure 1: Our handheld hardcopy output device (left) shares many of
the capabilities of a commerially produced printer (right), but in a
much more convenient form-factor.

Abstract

Thanks to the proliferation of the ARPANET, computers are used every day
by hundreds of people around the world to access a wealth of
information. However, until recently, this information could only be
applied in domains that could be brought within reach of a computer
terminal, or by operators with extensive memory training.

With the advent of the printer, this has begun to change. Computer
operators now are able to send digital information to a machine which
converts it into hardcopy, a physical rep resentation constructed from
marks on paper. This hardcopy information can then be transported to
application locations distant from any computer access terminal and
applied.

While this process is certainly more user-friendly than the al
ternatives of relying on memory or movement of information application
domains, it remains cumbersome, expensive, and inaccessible. We propose
a hand-held device which can pro duce informational markings on paper,
much like a printer. Hardcopy produced with our device has similar
information content to that produced with a conventional printer, but at
a lower price.

Further, we describe user-in-the-loop printing, a process en abled
by our device, which allows computer operators to fil ter and
transform information as it flows from the computer to the hardcopy.
These transformations can lead to ink sav ings through
domain-tailoring. We also demonstrate how our device can allow
computer operators to increase the informa tion output of existing
hardcopy -- either from a conventional

*^∗*e-mail: ix@tchow.com

printer or our own device -- through a process we term infor mation
overlay.

CR Categories: B.5.2.s [Rock]: Rock---Lobster

1 Introduction

ARPANET [Davies et al. 1967] is an inter-network of com puters,
which are able to exchange information between themselves using
digital network signalling. Estimates vary, but most experts
[Callahan and Hodgman 1971] agree that between tens and hundreds of
people use the ARPANET ev ery week, transmitting -- in aggregate --
more than 400 *kilo bytes^∗*of data during the average month.

However, until recently [2014], this information was con fined to
locations with direct ARPANET access, such as "ARPANET Cafes," or to
those locations to which computer operators with exceptional memory
skills could travel, such as "Cafes." However, with the advent of
printers, this restric tion has been relaxed.

In this paper, we extend the notion of printing with a hand held
hardcopy output device. Our device provides many of the same output
capabilities of a full-scale printer, with out requiring a movable
type department or access to steam power (a significant cost savings).
Further, our handheld de vice enables user-in-the-loop prin-ting,
through which the computer operator can actually transform the
information which they record.

^∗*A *kilobyte is unit of information equal to the storage capacity
of 64 kilograms of quarters (practitioners often summarize this by
saying there are "sixteen bits in one byte".)

Figure 2: A labeled diagram of our hardcopy output device. For more
information see the text. 2 Our Tool
{width="1.9720002187226597in"
height="2.4620002187226597in"}

A prototype of our hardcopy output device is shown in Fig

ure 1, with a schematic diagram shown in Figure 2. We

briefly explain the construction here. Curious readers are

invited to submit an NDA request to the second author to be

granted access to further details.
{width="0.5820002187226596in"
height="0.38200021872265966in"}

The operative end of the device is the rolling tip, which dis

tributes ink from the fluid reservoir. In non-printing situa

tions, the rolling tip is protected by the tip cover, which is

also is the anchor point for the adjustable fin -- which we be

lieve contributes to the overall aerodynamics of the device.

The fluid resevoir is surrounded by the cylinder hand inter

face, which -- as the name suggests -- is the control surface

through which the device is actuated during printing opera tions.

Finally, the neck strap is an ergonomic addition aimed at mit
igating hand fatigue during long printing sessions.

3 Basic Operation

During a basic printing session, the operator first secures the neck
strap to the device and adjusts it for optimal comfort. The operator
then transfers the tip cover from the rolling tip end of the device to
the tip cover storage location on the non tip end of the cylinder hand
interface. Next, the operator se cures a piece of printing substrate to
their video ARPANET computer terminal device, and -- controlling the
rolling tip's position with the cylinder hand interface -- directs our
device to move along the printing substrate in the patterns visible
through it.

This has the effect of creating ink deposits on the substrate,
registered to the ARPANET information the operator wishes to capture.

Though this process may sound complicated, we find that most operators
become proficient withing the first 1-2 weeks of incarceration in our
specialized training camp, at which point they are allowed to return
home.

Figure 3: User-in-the-loop prin-ting allows users to ex cerpt just
the information they require from a document (sin ister), unlike
conventional printing, which reproduces the en tire text (dexter).

4 User-In-The-Loop Prin-ting

Our hardcopy output has many advantages over a commer cial printer.
One large advantage is that -- because the user is controlling the
device -- they are able to transform the infor mation that is
recorded. We call this process user-in-the-loop prin-ting.

In this section, we summarize the prin-ting actions taken by a group
of computer operators using our device. We re cruited these operators
through an ARPANET posting, and in no way threatened or cajoled them
into participating. We list only the most common operations, since we
think that a more detailed list is probably worth saving for a second
publication.

4.1 Condensation

One of the most common transformations we observed was the removal of
extraneous textual information. This informa tion removal allowed
users to speed up their hardcopy pro-

duction process by omitting all but the most pertinent details.

Often this would involve the elimination of entire paragraphs and
sections, save for a few key equations or phrases. This is a huge
material and time savings that cannot be accom plished by commercial
printers.

4.2 Abstraction

Abstraction is the graphical analogue of condensation. Of ten, when
tasked with producing hardcopy of a particular im age, operators would
remove much of the detail from the im age; reproducing an
approximation with only a few strokes.

As with condensation, we found that the level of detail repro duced
was often task-dependent. For instance, when produc ing hardcopy of a
map, users were likely to carefully repro duce streets near their
intended journey or destination, and simplify or elide streets
elsewhere.

4.3 Spelling Alteration

During the course of hardcopy production, we often saw users change the
spelling of words. We believe that this is a positive indication that
our handheld printing device can contribute to the evolution of our
living language.

4.4 Incremental Refinement

Finally, several of our participants used an unexpected, but exceedingly
efficient, printing strategy, wherein a document produced on a
traditional printer was refined using our hard copy output device.

Though this hybrid output scenario was unexpected, we found that its
unexpected unexpectedness was not something we expected, but we would
not expect that follow-up work in this unexpected direction would be
unfruitful. So such follow-on work shouldn't be unexpected, unlike this
unex pected behavior, which wasn't something that was not unex pected.

5 Limitations

Our handheld printing device does have a few limitations, as compared
to a traditional printer. But none worth mention ing.

6 Conclusion

In this paper, we described a revolutionary device that en ables
computer operators to produce hardcopy without the need for an
expensive printer. In testing, we observed that operators used our
device not just to produce exact copies of documents, but actually
significantly transformed those copes (p \< 2*.0). We termed these
transformations *user-in the-loop prin-ting.

We have only tested our hand-held printing device on flat surfaces;
however, we are excited about the possibility of recording information
on non-flat surfaces -- a process we term "3D printing". We believe
user-in-the-loop 3D prin ting has the potential to revolutionize the
decorative arts.

References

2014. A recent year.

CALLAHAN, E., AND HODGMAN, J. F., 1971. John Hodg man.

DAVIES, D. W., BARTLETT, K. A., SCANTLEBURY, R. A., AND WILKINSON, P.
T. 1967. A digital communication network for computers giving rapid
response at remote ter minals. In Proceedings of the First ACM
Symposium on Operating System Principles, ACM, New York, NY, USA,
SOSP '67, 2.1--2.17.

A Even Prime Numbers

p_even = {*2}* (1)

B Integral Roots of Unity

{n | n ∈ Z*, n*² = 1*}* = {−*1,* 1*}* (2)

C Composite Prime Numbers

∅ (3)

Artisanal type theory

Carlo Angiuli

April 1, 2015

1 A brief history of some things

Food was invented by Mesopotamians some 5,000 years ago, and has been
eaten ever since. Logic was invented in the Mediterranean by ancient
Greeks, including Aristotle and a mortal man [1] named Socrates. It
lives on as an important course in pre-law curricula across the United
States.

Modern times require more modern logics. Computer programming is
closely tied to intuitionistic logic, in which proofs of a
proposition correspond directly to algorithms. Intuitionistic logic,
often in the form of type theory, is taught to several American
computer scientists annually.

Until the past several centuries, food and logic were primarily
manufactured by artisans, who trained apprentices in the arts of,
respectively, proofing and proving. The Industrial Revolution gave
rise to machines able to produce food and textiles much faster than
artisans ever could. The digital revolution, like wise, has turned
'computer' from a human job into a cheap, ubiquitous machine capable
of multiple calculations per second.

Despite the overwhelming success of mass-produced food, some consumers
want to revisit food's roots as a product sustainably and ethically
crafted by local artisans using traditional techniques. The result,
known as artisanal food, has taken off in popularity in the past few
years [2, 4].

2 Algorithms with the human touch

So too should computer scientists return to the roots of
computation---slow, error-prone calculations performed by humans.
After all, despite the close re lationship between computer programs
and type theory [3], or indeed, between computer programs and
algorithms, there is no need to involve computers in deeply human
tasks like sorting lists, routing packets, or decoding MPEG-4 video
streams.

We advocate a more personal approach to computation, called artisanal
type theory. Artisanal type theory has the same rules as ordinary
type theory, except that all terms and typing derivations must be
handwritten. Closed, well typed terms evaluate to values of the same
type, accompanied by a certificate of authenticity that a human
performed that evaluation.

Since each term was lovingly handcrafted and normalized, these
artisanally performed beta-reductions provide a more meaningful
explanation of type the ory than traditional computer-based
interpreters. Using artisanal type theory demonstrates a firm commitment
to *locally-*grown, sound, and complete reason ing systems.

3 Examples

Shallow learning. We can implement artificial intelligence using human
in telligence. Given the training data that false is desired but true is
not, one can manually build a classifier for booleans. Such a classifier
can then be run on a boolean to determine whether or not it is in the
desired set. In the example below, we run the classifier on false.

{width="4.526999125109361in"
height="2.015333552055993in"}

Fairly quick sorting. Artisanal computation has some advantages over com
puter programming---namely, humans can perform some computations without
needing a precise algorithm. In this example, we sort a list of integers
without the need to specify a particular sorting algorithm.

{width="4.528665791776028in"
height="1.695333552055993in"}

Small-batch jobs. We can also write scripts which artisanally perform
repet itive computing tasks such as renaming a large number of files,
accessing se quential URLs, etc. Doing so requires adding primitives
for I/O, file system access, and so forth. As discussed above, it is
unnecessary to actually imple ment these primitives, because the human
runtime already supports these tasks via a computer's traditional user
interface. Furthermore, unlike in traditional scripting languages, it
is easy to extend this with physical-world primitives such as
eatLunch, writeHandwrittenThankYouNote, and sleep.

4 Conclusion

We hope artisanal type theory will appeal to computer scientists and
mathe maticians who appreciate algorithms but believe computers
themselves are quite inconvenient at times. Unlike ordinary type
theory, it directly expresses compu tations as if people, but not
computers, matter. Therefore, we are hopeful that artisanal type
theory will be a useful foundation for the field of human science.

References

[1] Aristotle. The Organon. 40 B.C. Ed. Andronicus of Rhodes.

[2] Cope, S. Small Batch: Pickles, Cheese, Chocolate, Spirits, and
the Return of Artisanal Foods. Rowman & Littlefield Publishers, Inc.,
2014.

[3] Martin-Lof, P. ¨ Constructive mathematics and computer
programming. In Proc. Of a Discussion Meeting of the Royal Society of
London on Mathe matical Logic and Programming Languages (Upper Saddle
River, NJ, USA, 1985), Prentice-Hall, Inc., pp. 167--184.

[4] Schwaner-Albright, O. Brooklyn's new culinary movement. http://
www.nytimes.com/2009/02/25/dining/25brooklyn.html, Feb. 2009.

, .:9>?=A.?4A0 >:7A?4:9 ?: ?30 6¬942> ;4??>-A=23 -=4/20 ;=:-708

2]PR 3,9908,9

7LYR`LRP 0Y_S`^TL^_ LYO 0]]LY_ >N]TMMWP] .L]YPRTP 8PWWZY
AYTaP]^T_d

,->?=,.?

BP bLWVPO LN]Z^^ L M`YNS ZQ M]TORP^ ZYP OLd

-,.62=:A9/

1TR`]P LYO /PQTYT_TZY ^_L_P _SP bPWW ^_`OTPO 6ÈYTR^MP]R
-]TORP ;]ZMWPX F0`W H

-PYU -7A8

7TRS_ .ZYP >POPY_L]TLY .L]YPRTP 8PWWZY AYTaP]^T_d

{width="2.820333552055993in"
height="1.3736668853893264in"}

/PQTYT_TZY ?SP 6ÈYTR^MP]R -]TORP ;]ZMWPX 6-;

=PRTZXZY_T TY -Z]`^^TL P^^P TY^`WLX , OP] 6YPT[SZQ OTN_LX
QW`aT`X\`P PLX NTYRPY_PX TY O`Z^ OTaTOT ]LXZ^ \`PXLOXZO`X
Pc QTR`]L aTOP]P WTNP_% ]LXZ^ `P]Z S`T`^ QW`aTT ^P[_PX
TY ^_]`N_Z^ P^^P [ZY_TM`^ L M N O P Q P_ R .T]NL SZ^
[ZY_P^ TLX T^_L []Z[ZYPML_`] \`LP^_TZ Y`X \`T^
N`]^`X T_L TY^_T_`P]P \`PL_ `_ [P] ^TYR`WZ^
[ZY_P^ ^PXPW P_ YZY [W`^ \`LX ^PXPW _]LY^PL_

,NNZ]OTYR _Z _SP MP^_ XZOP]Y ^NSZWL]^ST[ T_ T^ _SZ`RS_
_SL_ _ST^ [L^^LRP ]PLO^ L^ QZWWZb^

l,_ 6ÈYTR^MP]R TY ;]`^^TL _SP]P T^ LY T^ WLYO , VYZbY L^
6YPT[SZQ LYO QWZbTYR L]Z`YO T_ T^ OTaTOPO TY_Z _bZ M]LYNSP^
L^ ^SZbY TY _SP QTR`]P& LYO _SP M]LYNSP^ ZQ _SP ]TaP]
^PaPY M]TORP^ SZbPaP] ZQ _ST^ L - . O P 1 LYO 2 ,W]PLOd
[]P^PY_PO _Z STX _SP \`P^_TZY NZYNP]YTYR _SP^P M]TORP^
T^ _SP NZ`]^P _Z MP TY^_]`N_PO ^Z _Z bSP_SP] L [P]^ZY
XLd MP LMWP _Z LYO YZ_ XZ]P _SLY ZYNP TY Z]OP] _Z [L^^ ZYP
Md ZYP _SP M]TORP^ SZYPd _SPX^PWaP^ w

?SP N]T_P]TL Pc[]P^^PO TY /PQTYT_TZY SLaP MPPY RPYP]LWTePO _Z
L]MT_]L]d RPZR]L[STNLW

1TR`]P % 6LWTYTYR]LO =`^^TL NZWWZ\ & MP__P] 6YZbY TY _SP
1Z]XLW 7T_P]L_`]P L^ 6ÈYTR^MP]R ;]`^^TL

_Z[ZWZRTP^ :Q Pc_]PXP WZNLW TY_P]P^_ T^ _SP TY ^_LYNP
OP]TaPO Q]ZX _SP NT_d ZQ ;T__^M`]RS ;PYY ^dWaLYTL A > , L^
/PQTYT_TZY

/PQTYT_TZY ?SP 6ÈYTR^ ;T__^M`]RS -]TORP ;]ZMWPX 6;-;

.]Z^^ PaP]d [POP^_]TLY YLaTRLMWP _]LY^ ?S]PP =TaP]
M]TORP bT_S L_ WPL^_ ZYP PYO[ZTY_ TY _SP NT_d ZQ
;T__^M`]RS PcLN_Wd ZYNP _Z MP LNNZX[WT^SPO O`]TYR ZYP
NZY_TY`Z`^ NT]N`T_

?ST^ L]_TNWP []P^PY_^ L NZY^_]`N_TaP []ZZQ QZ] _SP
PcT^_PYNP ZQ L ^ZW`_TZY _Z 6;-; 1`]_SP] XZ]P bSTWP XZ^_
[]TZ] bZ]V FBLW H SL^ WL]RPWd QZN`^PO ZY _SPZ]P_TNLW
LYLWd^T^ ZQ 6-; aL]TLY_^ ML^PO ZY R]L[S _SPZ]d SP]P bP
LOOT_TZYLWWd ZQQP] L XZ]P []LN_TNLW L[[]ZLNS ML^PO ZY
LXM`WL_TZY _SPZ]d

1:=8,74E,?4:9

?SP QZ]XLW ^_L_PXPY_ ZQ 6-; TY\`T]P^ LQ_P] _SP PcT^_PYNP
ZQ LY 0`WP]TLY [L_S ZY L R]L[S ]P[ ]P^PY_TYR 6ÈYTR^MP]R
bT_S ZYP YZOP _Z ]P[]P

{width="2.0436668853893263in"
height="1.4386668853893263in"}

1TR`]P % TYQZ]XLW /TLR]LX ZQ _SP ?Z[ZWZRd ZQ ;T__^M`]RS
;PYY^dWaLYTL L^ OPQTYPO Md T_^ -]TORP^ LYO =TaP]^

;=::1

?SPZ]PX ?SP 6ÈYTR^ ;T__^M`]RS -]TORP ;]ZM WPX T^ ^ZWaLMWP

BP []P^PY_ SP]P L NZY^_]`N_TaP ^ZW`_TZY _Z _SP []ZMWPX
QT]^_ RTaPY Md 3LYYPXLY ALYR[L_ LYO -W`X :N_ \" % L X y % [ X
?SP Q`WW ^ZW`_TZY SL^ WPYR_S XTWP^ LYO NZY^`XP^
L[[]ZcTXL_PWd \" SZ`]^ ZQ bLWW NWZNV _TXP BP OP[TN_ = TY _bZ
OT^_TYN_ ^_dWP^ TY L ^ZXPbSL_ LMM]PaTL_PO QZ]X TY ?LMWP LYO
1TR`]P

4Y_P]XPOTL_P OP_LTW^ XLd PL^TWd MP QTWWPO TY Md QZWWZbTYR
;]ZNPO`]P

;]ZNPO`]P 7P_ = MP _SP RTaPY ^ZW`_TZY ]Z`_P QZ] 6;-; [ MP
L [Z^T_TZY LWZYR T_ XPL^`]PO TY XTWP^ Q]ZX _SP ^_L]_ ZQ =
LYO ˆ]_c MP L `YT_ aPN_Z] TY _SP OT]PN_TZY ZQ = L_ [Z^T_TZY
c

bSTWP [ *\<*g=g OZ

O ← >_P[>TeP · ˆ]_[

_{BLWV [*,*} O

_{[ ← [ gg} Ogg

PYO bSTWP

=PXL]V >ZXP Pc[P]TXPY_LW OP_P]XTYL_TZY bTWW ZQ NZ`]^P MP
YPNP^^L]d _Z L]]TaP L_ _SP NZ]

1TR`]P % 1Z]XLWTeL_TZY ZQ 1TR`]P

^PY_ PLNS ZQ _SP WLYOXL^^P^ NZYYPN_PO Md aL]TZ`^ PORP^
M]TORP^ 4Y 6;-; bP ^TX[Wd NSLYRP _SP R]L[S _Z ]P[]P^PY_
_SP _Z[ZWZRd ZQ Z`] SZXP NT_d 1TR`]P

AYWTVP 6-; TY 6;-; bP ]P\`T]P LY 0`WP ]TLY NT]N`T_ ]L_SP]
_SLY LY 0`WP]TLY [L_S =P NPY_ OPaPWZ[XPY_^ TY LXM`WL_TZY
_SPZ]d SLaP ^STQ_PO _SP NZXXZY bT^OZX _ZbL]O^ L []PQP] PYNP
QZ] _SP `^P ZQ NT]N`T_^ ZaP] [L_S^ TY LX M`WL_Z]d []ZZQ^
L^ _SP NT]N`T_ []P^PY_^ L XZ]P

]PN_ aLW`P ZQ _SP >_P[>TeP aL]TLMWP BP ^`RRP^_ L
OPQL`W_ aLW`P ZQ \" NX _Z MP LOU`^_PO `[bL]O^ Z]
OZbYbL]O^ L^ [P]^ZYLW SPTRS_ LYO WZNLW _P]]LTY ]P\`T]P

7PXXL BLWVLMTWT_d

, [ZTY_ [ LWZYR = NLY MP ]PLNSPO Q]ZX [ZTY_ [ LWZYR =
QZWWZbTYR ;]ZNPO`]P L^^`XTYR [ \< [

;]ZZQ ?]d T_

7PXXL _S`^ P^_LMWT^SP^ L vXZO`^ [ZYPY^w ]P^`W_ QZ]
_]LaP]^LW ZQ _SP ]Z`_P = Q]ZX T_^ MPRTY YTYR [ ( _Z T_^
PYO [ ( g=g ?ST^ T^ SZbPaP]

NZYaPYTPY_ []LN_TNLW L[[WTNL_TZY ;`_ TY XZ]P TY_`T_TaP
_P]X^ _SP 0`WP]TLY NT]N`T_ LWWZb^ _SP M]TORP bLWVP]^ _Z
^WPP[ TY _SPT] ZbY MPO^ _SP QZW WZbTYR YTRS_ ]L_SP] _SLY MPTYR
^_]LYOPO LN]Z^^ L ]TaP] 1Z]_`YL_PWd _SP _Z[ZWZRd bP SLaP
^P WPN_PO QZ] 6;-; LWWZb^ QZ] ^`NS L ^ZW`_TZY

?SP L^_`_P ZM^P]aP] bTWW YZ_P _SL_ YZ PORP LXZYR Z`] QZ]
XLWT^X ]P[]P^PY_^ _SP ^YO ^_]PP_ M]TORP /`]TYR _SP
[]ZR]P^^ ZQ Z`] ]P^PL]NS _ST^ M]TORP OTO YZ_ PcT^_ O`P
_Z NZY^_]`N_TZY LYO SPYNP T^ ZXT__PO 4Q LOOPO _Z _SP R]L[S
NLWW T_ 6;-;u T_

+----------------------+-------- | 9ZOP | 0ORP +======================+======== | > 00 | > 3; | > | > | > 9> | > ! | > | > | > 00 | > ! | > | | > 9> | =L. | > | | > 00 | > ,B | > | | > 9> | =Z. | > | | > 00 | 86= | > | | > 9> | > B0 | > | | > >> | +----------------------+-------- ---------------+----------------------+
| 9ZOP |
===============+======================+
| > 9> |
| > |
| > 00 |
| > |
| > 9> |
| > |
| > 00 |
| > |
| > 9> |
| > |
| > 00 |
| > |
| > 9> |
| > |
| > >> |
| > |
| > 9> |
---------------+----------------------+

+-----------------------+----------------------+-----------------------+
| 9ZOP | 0ORP | 9ZOP |
+=======================+======================+=======================+
| > 9> | 1_/ | > 00 |
| > | | > |
| > 00 | 1_; | > >> |
| > | | > |
| > >> | > >1 | > 00 |
| > | > | > |
| > 00 | > 7TM | > >> |
| > | > | > |
| > >> | > -3 | > 00 |
| > | | > |
| > 00 | 38> | > >> |
| > | | > |
| > >> | > 21 | > 00 |
| > | | > |
| > 00 | 3>2 | > >> |
| > | | > |
| > >> | | > 00 |
+-----------------------+----------------------+-----------------------+

T^ VYZbY _SL_ L YZY NdNWTN ^ZW`_TZY PcT^_^ M`_ L
NZY^_]`N_TaP []ZZQ T^ WPQ_ _Z Q`_`]P bZ]V

?LMWP % g=g ( XT

ZQ N]Z^^TYR^ XLd MP Q]PPWd NZY^_]`N_PO QZWWZbTYR = Q]ZX
1TR`]P {width="2.8086668853893264in"
height="2.440333552055993in"}

1TYLWWd ^P_ 0 ( f,WLY -PY 2]PRh ?SP OTL R]LX^ TY 1TR`]P ZQQP]
L aT^`LWTeL_TZY ZQ _SP^P aLW`P^ QZ] , - LYO 0

>TYNP g0g ( ) _ST^ []ZaP^ 7PXXL LYO _S`^ _SP ^`NNP^^Q`W
TY^_LY_TL_TZY ZQ .ZYOT_TZY^ y ?ZRP_SP] bT_S 7PXXL _ST^ []ZaP^
_SL_ = T^ L YLaTRLMWP 0`WP]TLY NT]N`T_ ZQ _SP NT_d ZQ
;T__^M`]RS ?SP]PQZ]P L ^ZW`_TZY _Z _SP 6ÈYTR^

;T__^M`]RS -]TORP ;]ZMWPX PcT^_^

.:9.7A>4:9

1TR`]P % L NL]_ZR]L[STN =PYOP]TYR ZQ _SP >ZW` _TZY =Z`_P =

L [`]PWd _SPZ]P_TNLW ]P^`W_ BP YZb ^SZb _SP []LN_TNLMTWT_d
ZQ _SP ^ZW`_TZY TY LY Z[P]L_TZYLW ^NPYL]TZ aTL L Y`XMP] ZQ
^L_T^QTLMWP NZYOT_TZY^

.ZYOT_TZY 4YT_TLWTeL_TZY

7P_ , MP L ^P_ ZQ L__PX[_TYR [L]_TNT[LY_^ ?SPY
_{L X`^_ MP []P^PY_ L_[(} ^,L ∈ ,

.ZYOT_TZY ;]ZR]P^^TZY

7P_ - MP L ^P_ ZQ \`LWTQdTYR M]TORP^ ^`NS _SL_
_{_SP QZWWZbTYR L]P _]`P} ^,M ∈ -% M ^L_T^QTP^ _SP M]TORP
N]T_P]TL Q]ZX /PQTYT_TZY & M SL^ OP QTYPO ≤ [_M ≤ ZY = 7P_
M_T MP _SP T_S Z]OP]PO PWPXPY_ ZQ - LYO WP_ g-g ( Y ?SPY . ( fN ,
..., N_Yh LYO N_T ( >_T, M_T TQQ ^ZXP >_T ⊆ , N]Z^^P^
M_T

.ZYOT_TZY ?P]XTYL_TZY

7P_ _SP ^P_ ZQ PYOTYR [L]_TNT[LY_^ 0 ⊆ , ( fL ∈ , | L
∈ >_T^,Th ?SPY _SP ^ZW`_TZY T^ ^`NNP^^Q`W TQQ
_{0 = ∅ LYO P T^ []P^PY_ L_ [ (} ^,P ∈ 0

7PXXL >L_T^QTLMTWT_d ZQ .ZYOT_TZY^ .ZYOT_TZY^ y L]P ^L_T^QTLMWP

;]ZZQ >P_ , ( f,WLY -PY /LY 2]PR 6PT_Sh
_{9Z_P _SL_ ;] c LbLVP L_ L X (} ^,c ∈ , ,^
_{WZYR L^ )} ) FA44 H

>P_ - ( f3TRSWLYO ;L]V ! ^_ >_]PP_ _S >_]PP_ !_S
>_]PP_ $_S >_]PP_ \"_S >_]PP_ !_S >_]PP_ 8N6PP^
=ZNV^ BP^_ 0YO 1Z]_ /`\`P^YP 1Z]_ ;T__ >XT_SQTPWO
>_]PP_ 7TMP]_d _S >_]PP_ -T]XTYRSLX 3Z_ 8P_LW 2WPYbZZO
3ZXP^_PLO 2]Ld^h ?SP M]TORP N]T_P]TL ZQ /PQTYT

_{_TZY L]P ^L_T^QTPO} ^,M ∈ - ?SP]PQZ]P _SP ^P_ .

AP_P]P 6ZYTR^MP]R NZY^P\`L_ [ZY^ 6-; OP^TR YL_ TY^`WLP
`]MPX QW`XTYL [ZY_P^ \`T TY _LWT QTR `]L_TZYP _]LY^TPY^
[P] ^TYR`WZ^ ^PXPW T_P] `Y`X YZY [Z_P^_ 4Y SZN L]_TN`WZ
\`LP^_TZYT^ Pc[Z ^`TX`^ LNNZXXZOL_TZ SZOTP]YL OTP LO
Z[[TO`X ;T__^M`]RS 6;-; >TRYTQTNL_ LOL[_L_TZYPX LO
[]ZQPN_`X YZ^_]`X TY^TRYT^ NTaT_L^ TY P^ ^`[P] O`ZM`^

AYZ XZOZ ^TN`_ 6;-; P^_ ^ZW`MTWT^ ZQQP]_ XL_SPXL_TNT
YZ^_]LX NZWWL_TZYPX TYNT_LXPY_`X LO T]P QZ]T^ P_ LNNT[TLX LM
PZ LWT\`TO PcP]NT_T`X \`ZO SZOTP XLRT^ \`LX ^ZXYT`X \`ZO
QTP]T YZY [Z_P^_ /PTYOP TY^`[P] ZQQP]PML_ ^[PN`WL_TaL ]L
_TZ YZ^ TY^_]`T_ P_TLX []ZMWPXL LPOTQTNLY_ \`T []ZMT LO
`W_TX`X [POP^ OPNPX XTWTL X`W_L XLWL

=010=09.0>

F0`W H 7PZYS 0`WP]Z >ZWa_TZ []ZMWPXL_T^ LO RPZXP_]TLX ^T_a^
4Y .ZXXPY_L]TT LNLOPXTLP ^NTPY_TL]`X ;P_]Z[ZWT_LYLP [[ # \"

FALY H ,WLY ALYR[L_ ,WLYu^ [SZ_Z^ S__[% UZ`]YLW LWLYa Z]R
*[( !\"

FA44 H /] ?ZX 8`][Sd A44 BSL_ TQ LYd_STYR T^ P[^TWZY* 4Y
;]ZNPPOTYR^ ZQ _SP 0TRS_T P_S .PY_PYYTLW 4Y_]LNLWL]d =ZMZ_ /LYNP
;L]_d TY 8Z`]YTYR ZQ 3L]]d B -ZaTVu^ ^!_S -T]_SOLd

FBLW H 5LXP^ BLWP^ >PaPY M]TORP^ ZQ VÈYTR^ MP]R 4Y BTVT[POTL
_SP Q]PP PYNdNWZ[P OTL

{width="2.6375273403324586in"
height="1.7520002187226598in"}{width="2.6358606736657917in"
height="1.7520002187226598in"} L .ZYOT_TZY 4YT_TLWTeL_TZY M LY
PcLX[WP 8PXMP] ZQ _SP ^P_ -
{width="2.64163823272091in"
height="1.868665791776028in"}{width="2.6358606736657917in"
height="1.7536668853893262in"} N M0 ∈ = ^ _ M ∈ - O .ZYOT_TZY
^`NNP^^Q`W ?P]XTYL_TZY

1TR`]P % >L_T^QTLMTWT_d ZQ .ZYOT_TZY^ FALY H

7UDFN \<

2QH 3DSHU 7ZR 3DSHU 5HG 3DSHU %OXH 3DSHU DQG 2WKHU )XQ *DPHV IRU
&KLOGUHQ

5HG L 5HPRYDO ZLWK $UWLILFLDO 5HWLQDO 1HWZRUNV

\'U 7RP 0XUSK\ 9,, 3K \'

.H\ZRUGV FRPSXWDWLRQDO SKRWRJUDSK\ LPDJH SURFHVVLQJ JHQHUDOL]HG
SKRWRVKRS DUWLILFLDO UHWLQDO QHWZRUNV W\SHV

$ 3URRI RI WKH 7ZHOYH &RORU 7KHRUHP

+H\ 1RERG\ %RWKHUHG %HIRUH

\< 7 %RYHFN DQG 9LFWRULD 9 9DUJ 0DFN

.H\ZRUGV WZHOYH FRORUV SODQDU JLUDIIHV WLPH WUDYHO GULYHO IRQWV DUH
XJO\ LQ WKH IXWXUH

9LVXDOO\ ,GHQWLI\LQJ 5DQN

\'DYLG )RXKH\ \'DQLHO 0DWXUDQD DQG 5XIXV YRQ :RRIOHV

.H\ZRUGV SHUFHSWXDO RUJDQL]DWLRQ YLWDPLQ UDQN GHILFLHQFLHV
HJDOLWDULDQLVP LQ WKH 36\' FRQH 3$& ERXQGV IRU 69\'V FODVV FRQVFLRXV
QRUPV

7UDQVSDUHQF\ 5HSRUW

7KUHH /HWWHU $JHQF\

.H\ZRUGV WUDQVSDUHQW LQYLVLEOH VHH WKURXJK

Red i removal with artificial retinal networks

Dr. Tom Murphy VII Ph.D.^∗

1 April 2015

Abstract {width="2.6836668853893264in"
height="1.7620002187226598in"}

We present a GPU-accelerated means for red i removal

in photographs.

Keywords: computational photography, image processing,

generalized photoshop, artificial retinal networks, types

1 Introduction

When light---such as the bright flashbulb of a camera---

strikes the human eye, it illuminates the retina. Some

of that light bounces back out of the eye, but most of it stimulates
neurons in the retina to produce electrical signals. These signals
stimulate other neurons to which they are connected, and so on, until
the brain (which is technically part of the eye) perceives an image, as
a two-dimensional array of neurons with different activa tion levels.
Humans often use these images to sense the world, for example, in
reading research papers.

This research paper concerns a particular feature of this process, which
is that humans are able to view an image and ignore certain details of
it. For example, Figure 1 contains a printout of an image file of a pho
tograph of a television displaying a recorded video of an actor. The
video contains a superimposed eye in the corner, the logo of the network
CBS. Most viewers are not tormented by this everpresent eye staring at
them! In fact, most viewers are able to completely ignore the eye, and
view the scene as though it didn't contain the stimulus, even if details
such as the actor's sweatshirt's collar pass beneath the stimulus and
are occluded by it.

Some stimulus is more everpresent than others. The Clay Mathematics
Institute lists among its unsolved Millennium Prize problems the
"red i removal prob lem." This concerns the removal of stimulus (a red
letter "i") from images (Figure 2). The problem is particu-

^∗*Copyright 2015 the Regents of the Wikiplia Foundation. Appears in
SIGBOVIK 2015 with the increasingly askance visage of the Association
for Computational Heresy; *IEEEEEE! press, Verlag-Verlag volume no.
0x40-2A. 0.00 Australian Neo-Dollars
{width="0.10907589676290463in"
height="0.10907589676290463in"}

Figure 1: Q. Who watches the TV watchers? A. CBS's all-seeing eye.

larly difficult because the information occluded by the i is
completely gone, and because the authors of papers about the problem
are persistently agitated because it seems like the letter should be
capitalized.

In this paper I show how red i removal can be solved in certain
specialized cases, using an artificial retinal net work patterned
after the brain contained within the hu man eye. Training this
artificial retinal network is feasi ble on a single powerful desktop
machine. Both training and execution of the model (a mere 400
megabytes) are GPU accelerated. The model presented in this paper was
trained in about 3 days, and executing it in parallel on a suite of
images takes about 100 milliseconds per image.¹

2 Artificial retinal networks

As I expertly foreshadowed in the previous section, an artificial
retinal network works just like the brain in side a human eye. The
retina is itself a rectangular 2D array of neurons, which turn photons
into IEEE-754 floating point values between 0.0f and 1.0f. Behind this

¹Source code is available on the World Wide Web at:
http://sourceforge.net/p/tom7misc/svn/HEAD/tree/trunk/redi

{width="2.055333552055993in"
height="2.0520002187226596in"}

Figure 2: An image of an Enigma machine rotor with a red i superimposed.
Solving this instance of the red i removal problem would mean producing
an image with out the red i. One way to do this would be to steal a
floppy disk containing an original, unimposed image of the rotor, from
someone in possession of it, for example the paper's author.

is another 2D array of exactly the same size, except the pixels are in
a weird jumbled order, and then another layer. This series of layers
is known as the optic nerve. Finally, the brain perceives the image as
an array of pixels, again of the same size (Figure 3).

It is easy to reconceptualize this process as an array of pixels
undergoing several transformations. Obviously the story is more
complicated: Humans see in color, so each pixel is actually three
different nodes, one for red, green and blue. In fact, since some
scientists hy pothesize of certain "superseers"---that is, people who
can perceive more than just the three wavelengths of light---we actually
allow an arbitrary number of nodes per pixel. In this work, we used N
= 4.

In a real human eye, each node is fed inputs from ev ery node in the
previous layer. For computational effi ciency, in this work we allow
only 64 inputs to each node from the previous layer. Because we
suspect that lay ers are spatially related, a node is always connected
to its neighborhood in the previous layer (each node from the 9
pixels within Manhattan distance 1). The rest of the inputs are
selected randomly from a Gaussian distribution, as long as the samples
fall within the im age (using rejection sampling---the sides and
corners do not "wrap around"). By the way, the images are al ways
256x256, because numbers that are a power of two are faster.² The
connection from one node to another

²This is true on computers, because computers count in binary.

Figure 3: How eyes work, and thus, artificial retinal networks.

is modulated by a weight, again an IEEE-754 floating point number. A
node outputs the sum of its input val ues, passed through a
smoothulator, specifically the one found in Gray's Anatomy (the book,
not the TV show),

1

1 + e^−v

This function is biologically plausible.

We learn by backpropagated stochastic gradient de scent, like babies
do. Specifically: The network is pre sented with an image on its
retina, and then we run the floating point values through the layers,
summing them up and applying the smoothulator function, to produce a
final image within the brain. Like a baby, it com pares this image to
what it expected to see, node by node. Where each node does not agree
with the image, the error is computed. The baby propagates the par
tial derivative of the change in error with respect to the change in
stimulus to the previous layer proportional to its weighted impact;
fortunately the smoothulator has a simple derivative that is easily
computed at a point from its output values. Error is not propagated
into the real world (i.e., by sending light off of the retina back to
the physical object that created the stimulus; that would be
ridiculous).

2.1 Training data

One of the insights of this paper is that although ar tificial retinal
networks require a lot of data to train, for certain problems the
training data can be easily generated. For the red i removal
problem, we begin with a corpus of about 4,000 images that were
scraped from Google Image Search. Scraping images is easy; one just
needs to list a bunch of queries for things that babies would want to
view in order to learn what the world looks like. In this experiment I
used terms such as [snakes], [dog on skateboard], [guitar],
[stonehenge] and [superyacht]. Following this, I manually cleaned

In the human eye, powers of ten are faster, because humans have ten
fingers.

the training data. I deleted images that were not pho tographic
(drawings, etc.; for example, most images of guitars are actually 3D
rendered cartoon guitars, fan tasy images of guitars on fire, the
Guitar Hero logo, and so on) or that were too, uh, pornographic
(most queries for things that can have sex, like tapirs, contain promi
nent images of the things having sex). These are not appropriate for
babies.

All images are cropped to a square and resized to 256x256. Then we
generate training instances: An in put image and the expected result.
An image that does not contain a red i should just be transformed into
the image itself (indeed, when we peer directly into the brain of a
baby looking at a TV show, we find a re gion of the brain where the TV
show is clearly visible). It is also easy to generate instances of the
red i removal problem along with their solutions---we simply put a red
i randomly on the source image and keep the destination image
unchanged. In this way, we can easily generate a large amount of
training instances (in actual practice, this procedure had a small
bug; see Section 3.1). One unexpected phenomenon is that I had to be
careful to remove images that already contained a red i, like many
images of casinos, which are often called "CASINO".

In order to coax networks into recognizing the i, we also place an i
into the 4^th color channel in the same position in the expected
output. This is an invisible color channel which we discard, and which
is always zero in the input. In essence we giving a hint to the eye's
brain that it should not just remove the red i, but it should also
perceive it. I have not performed enough experi ments to know if this
is helpful.

For repeatability's sake, important constants used in this experiment:
There were 2 hidden layers. Gaus san samples were produced with a
standard deviation of 16 pixels. The red i was rendered in Comic Sans,
at a height of 80 pixels. I used a variety of learning rates, in cluding
an expontentially decreasing one (the standard advice of 0.05 is too
large for constant learning rates on this kind of task, and limits the
sharpness of resultant images).

2.2 CUDA, SHUDA, WUDA

Because we are working with graphical data, we should use the Graphics
Processing Unit of the computer, not its Central Processing Unit (we are
not processing cen ters). I implemented high-performance OpenCL kernels
for each phase of training: The forward pass (signals flowing from the
retina to the eye's brain), the back propagation step (when the eye
computes the error and partial derivatives) and the weight update step
(when

the eye rewires its neurons so that it sees the right thing next
time). The phases have different parallelism con straints. Because the
connectivity is sparse, we repre sent both forward and inverted index
maps, which are decoded on the GPU. We take care to only load a sin
gle layer of the retinal network into the GPU's RAM at once, to enable
very large models, but we run many training instances in parallel for
a single round. Some other operations, like the preparation of
training data, are performed on the CPU. These are also frequently
done in parallel, using C++11's new std::thread with some crazy-ass
wrappers to allow them to function in mingw32's 64-bit gcc port. On a
good day, training uses all 6 CPU cores and all 2800 GPU cores and
about 14 GB of RAM and warms the home office like a 1kW space heater.

3 Results

After 4 rounds of training, the network produces an excellent-looking
image that could be a Cure album cover, regardless of the stimulus
cast upon its retina (Figure 4).

{width="2.050333552055993in"
height="2.050333552055993in"}

Figure 4: Result after 4 rounds of training. Looks great, and there is
no red i to be seen, but it loses some points for not resembling the
input image at all.

It's not long before the network learns that it should not produce the
same result for every input, and the output starts to mimic the input.
These images look sort of like the world viewed through frosted glass
(Fig ure 5), simulating how a baby first learns to see the world
through the 1cm bulletproof Lexan of its translu cent BabyLearn
incubation cylinder.

Soon thereafter, the network begins to converge on

something like the identity function, as this drastically reduces error
(even if some error is incurred by the persistence of the red i). Left
overnight (about 9,000 rounds), we start to see the network both produce
im ages much like the original (perhaps through a hip "vin tage"
Instagram filter), as well as removing the red i stimulus (Figure 6).

3.1 Evaluation

With a further 30,000 rounds of training, the output im ages sharpen and
lose their Instagram quality (maybe only a small amount of "grain"), and
the i is still suc cessfully removed. However, since we've now made many
passes over each image in the training set (and the model has about
100,000 degrees of freedom), it is certainly possible that we've simply
overfit to this set of images (that is, that the baby's eye's brain is
simply memorizing the i-free images and then recalling the one that
looks closest to the stimulus). To evaluate fairly, we need to apply the
model to totally new images that it was not trained on. These are called
"eval" images.

Firing this up, I observed that the model successfully reproduced eval
images that did not contain a red i; this is good because it means that
it is not simply memoriz ing the training set images. I then started
placing red i stimulus on the images with the mouse, and my heart sank:
It wasn't removing the red i at all! Dejected, I tried loading up the
training images and putting a red i on them---it also did not remove the
i, which did not make sense! Even for babies! Eventually, I discovered
that the red i would be removed, as expected, but only when the i was in
a handful of very specific locations. This was found to be a bug in the
random i placing code; can you find it too?

uint8 x_dice = seed & 0x255;

seed >>= 8;

uint8 y_dice = seed & 0x255;

As a result, there are only 16 different possible x coor dinates, and
same for y. Nonetheless, this is still 256 dif ferent i locations that
work, which implies considerable generality is possible. Due to
Draconian SIGBOVIK deadlines, I have not yet been able to test a
debugged training procedure.

Once the evaluation code only places an i at expected locations, the
artificial retinal network works well (Fig ure 7)!

4 Conclusions

We find that the supposedly impossible red i removal problem is in
fact solvable, at least in some forms, using artificial retinal
networks. There are some limitations of the current model:

{width="4.7110673665791775e-2in"
height="5.0251531058617675e-2in"}It has only been tested to remove the
letter i when it is rendered in bright red, in 30 point Comic Sans.

{width="4.7110673665791775e-2in"
height="5.0251531058617675e-2in"}It probably also removes letters like
j, but maybe also in some other fonts, which is a sword that cuts both
ways.

{width="4.7110673665791775e-2in"
height="5.0251531058617675e-2in"}Due to a bug, the red i must be at a
position whose coordinates are exactly 12 + x₀ + 4*x*₁ +
16*x*₂ + 64*x*₃, 12 + y₀ + 4*y*₁ + 16*y*₂ + 63*y*₃ ,
for x_j*and *y_j*in *{*0,* 1*}*.

{width="4.7110673665791775e-2in"
height="5.0251531058617675e-2in"}It automatically and non-optionally
applies Instagram-style filters.

This technique can probably be applied to other im age processing
problems, for example, J peg dequan tization. Here, we take an image
and badly quantize it (for example, to 4 bits per color channel), and
the training instance consists of the quantized image as in put and
the original image as the expected output; the retinal network learns
how to fill in detail. Figure 8 shows the early stages (about 4000
rounds) of training such a model.

A related, still unsolved problem is "red i reduction"; here we do
simply remove the i but replace it with a smaller i. For example, we
could replace a capital I with a lowercase one, or replace a lowercase
30pt Comic Sans i with a lowercase 29pt Comic Sans i. This is an
offshoot of the text ure compression field, which seeks to make the
text "ure" smaller wherever it appears.

Biologically-inspired computer algorithms hold many wonders for those
that seek to tap into the limitless po tential of the 85% of the human
eye's brain that is cur rently unused. Perhaps humans even contain
graphics processing units!

For higher-fidelity images and source code, please consult
http://tom7.org/redi.

{width="2.995333552055993in"
height="4.505333552055993in"}{width="2.99700021872266in"
height="6.028666885389327in"}

Figure 6: After about 9,000 rounds. Top row is the

input image, the second row is the output (no longer

showing hidden layers because they all just look like

firefly raves); the bottom row shows 4x magnified detail

of the region formerly containing the red i. Images are

somewhat desaturated and blurry, but the red i is re

moved. Note how in the right image, the retinal network

Figure 5: Result after 80 rounds of training, with the

successfully continued both the horizontal and vertical

input image at the top and the signal proceeding down

bookshelves into the occluded region. This is not a trick.

ward through two hidden layers. The hidden layers as

pire to crazy noise-terror glitch art versions of the stim

ulus as well.

{width="2.9986668853893264in"
height="2.995333552055993in"}{width="2.99700021872266in"
height="3.0203324584426947in"}

Figure 7: Evaluation on new images after 30,000 rounds of training. Top
row is the input image, the second row is the output, and third is 4x
magnified defail. The first image (no i) shows the high amount of detail
pre served. In the latter two, the i is successfully removed; the
quality of the replacement is not perfect, but cer tainly reasonable.

Figure 8: Evaluation of an early model for J peg dequan tization. The
model still contains a lot of noise pixels, which sometimes take a
long time to converge, but it is already easy to see how quantization
artifacts have been reduced (left). Actually, there is no reason why
such de quantization must only be applied to J pegs; the right column
shows it working on a nice rainbow picture.

A Proof of the Twelve Color Theorem:

Hey, Nobody Bothered Before.

Sixth Grade Class Project for Mr. Blum

Y. T. Boveck Victoria V. Varg-Mack, VI

April 1 ^{[1]{.underline}}₃ , 2071

Editor's note: Several days ago, the wreckage of a small time

machine appeared in the program committee's office, containing

apparently only a copy of the proceedings from SIGBOVIK 2071.

Unfortunately, all papers but one were burnt beyond recognition.

Current speculation holds that the time machine operators forgot

to disable the paradox safety interlock, and all the important (po

tentially causality-violating) papers were destroyed, leaving only

this drivel. We're publishing it anyway, sorry.

Abstract

Roughly 100 years ago, mathematicians successfully proved the 4-Color
Theorem. Widely regarded as one of the most important theorems in
graph theory at the time, the 4-Color Theorem states that for all
planar graphs there exists an assignment of colors to nobes, such that
no two adjacent nobes are assigned the same color, with at most 4
colors used. However, modern-day computers are capable of rendering
far more diverse color palees, and the old 4-color limitation is now
largely irrelevant. In this work we extend the old result to support
12-colorings, offer some thoughts on generalization, and leave a
conspicuous hole in our proof to support our future work.

1 Introduction

Victoria said I had to write this section, even though she's the only
one of us who actually knows how the 4-color theorem proof goes. But
luckily I found a proof for the 5-color theorem that made sense, and
since having more colors is obviously beer, that should work just as
good. It goes like this:

Lemma 1.1. All planar graphs have at least one nobe with at most
5 neighbors.

Proof. Let N(n) mean how many neighbors a given nobe n has.
Then because each edge connects two
_{nobes, the sum of all nobes' neighbors} _n N(n)=2*e*.
Let's assume all nobes have at least six neighbors. Then 6*n ≤* 2*e*.

Next let E(f) mean the number of edges that make up the border of
a given face f of the graph. Since _{each edge borders 2 faces,}
_f E(f)=2*e*. Every region is bounded by at least 3 edges so that
means 3*f ≤* 2*e*.

If we plug all that into the "Euler's Forumula" that Mr. Blum gave us
in class, which says that n − e + f = 2, here's what we get: n −
e + f ≤ ^{[e]{.underline}}₃ − e + ^{[2*e*]{.underline}}₃ = 0.
But since n − e + f = 2 we end up with 2 ≤ 0. Then we must have
been wrong to assume all nobes have at least six neighbors. That's a

"contradiction"!

Theorem 1.2. All planar graphs can be colored with no more than 5
colors so that no neighbor nobes have the same color.

Proof. Let G mean the graph we're trying to prove this for. Using
the lemon I just proved, pick the nobe n that has at most five
neighbors and call those n₁, n₂, n₃, n₄, n₅ in
whatever order you want, but remember the order! Let G mean the
smaller graph you get by taking out n, which of course is still
planar. Because G is smaller, we already know with "induction" that
G can be 5-colored. (That step seemed kinda weird to me but Victoria
said it was legit so please don't take points off.)

Now we're gonna assume G can't be 5-colored. For this to be true,
then each n_i*from 1 to 5 must all have different colors, or else
you could just pick the missing one for *n. Let's think about the
sub-graph that has only the 2 colors matching n₁ and n₃, call
it G₁₃. If the graph is disjoint, meaning n₁ and n₃ are in
two separate parts, then you would be able to re-color the graph to
make n₃ have color 1, so you can paint n with color 3. Therefore
G₁₃ must be connected. You can make the same argument for G₂₄
to be connected, but suddenly that doesn't make any sense, because a
path that keeps G₂₄ connected would have to intersect the
connected G₁₃!

So now, even if the 5-coloring of G gives all different colors to
n₁, n₂, n₃, n₄, n₅, you should be able

to re-color one of the n_i*s so you can have a spare color to give
to *n. That means you can 5-color G.

Nice! Hey, that wasn't so bad.

2 The 12-Color Theorem

In the previous section, Y.T. et al. outlined the prior work in the
field. Now we will make our main contribution; namely, to extend the
5-color theorem reviewed above to allow for 12-colorings of arbitrary
planar graphs.

Theorem 2.1. Given an arbitrary planar graph G, there exists an
assignment of no more than 12 colors to the set of nobes N(G) such
that no two neighbouring nobes are assigned the same color.

Proof. Using Theorem 1.2, generate a 5-color assignment for G. As 5
is less than 12, this assignment

suffices.

Corollary 2.2. If G has at least 12 nobes, then all 12 colors may
be used.

Proof. First we will prove the case for a smaller number of colors
c \< 12, by induction on c. Assume a graph G with c or more
nobes, and an existing assignment of c − 1 colors in which all
colors are represented, such that c \< 12. The pigeonhole principle
states that there must exist two nobes n₁ and n₂ with the same
color. Simply assign the c*th color to *n₂ in the new coloring.

Next for the case c = 12. Given a graph G with 12 or more nobes,
there must exist an assignment of 11 colors in which all colors are
represented. The pigeonhole principle states that there must exist two
nobes

n₁ and n₂ with the same color. Assigning the 12^th color to
n₂ causes all 12 colors to be used.

An example application of our algorithm is depicted in Figure 1.

3 Conclusions and Future Work

In this paper we reviewed historical developments in the field, with a
particular focus on the proof of the ~~4-Color Theorem~~ 5-Color
Theorem; and we presented our main contribution, a constructive proof
of our new 12-Color Theorem based on the assumption of existing
~~4-colorings~~ 5-colorings of an arbitrary planar graph G.

The most significant limitation of our work is that a generalized
version of our proof only applies for C-colorings when C ≤ 12. In
future research, we plan on extending our theorem to support ever
greater values of C. We hope the need for additional funding to
study such advanced open problems is self-evident.

^{(a) Make a 4-color of your graph first.} (b) Choose a nobe and
color it different.

$c$ Repeat that seven more times to get a 12-coloring! (d) If you
had 51 different colors and wanted to use them all, it would look like
this. However, we are

leaving a proof of the existence of generalized 51-

colorings to future work.

Figure 1: Mr. Blum said we needed to have some pictures in our paper,
so we pretended the USA was a graph and colored it like our algorithm
says.

CONFIDENTIAL COMMITTEE MATERIALS
{width="0.9486668853893263in"
height="0.9486668853893263in"}

SIGBOVIK 2015 Paper Review

Paper 10: A Proof of the Twelve-Color Theorem

Mr. Blum, New Pittsburgh Middle School

Rating: :(

Confidence: 4/4

This project makes a well-meaning, but ultimately entirely
unconvincing, attempt at proving an interesting theorem in computer
science. In the early twenty-first century, when the four-color
theorem was still considered exciting, as opposed to something that
all schoolchildren are taught from an early age, this might have been
a reasonable starting point for sixth-grade work. Unfortu nately, my
standards are higher than this. I would have been more impressed if
Y.T. and Victoria had started with a more recent and interesting
result, such as the 2068 paper of Blum et al. (no relation) showing
that P = NP.

Of course, as this class is "United States History: The 2017 Burrito
Wars to the Present Day", none of the above has any bearing. Using our
school's standard grading scheme of :) to :(, I assign this project a
:(

SIGBOVIK, APRIL 2015

Visually Identifying Rank

David F. Fouhey, Mathematicians Hate Him!

Daniel Maturana, Random Forester Rufus von Woofles, Good Boy

Abstract---The visual estimation of the rank of a matrix has
eluded researchers across a myriad of disciplines many years. In this
paper, we demonstrate the successful visual estimation of a matrix's
rank by treating it as a classification problem. When tested on a
dataset of tens-of-thousands of colormapped matrices of varying ranks,
we not only achieve state-of-the-art performance, but also
distressingly high performance on an absolute basis.

Index Terms---perceptual organization; vitamin and rank
deficiencies; egalitarianism in the positive-semi-definite cone; PAC
bounds for SVDs; class-conscious norms

✦

that require access to the matrix, our work gives
{width="0.9120002187226597in"
height="0.910333552055993in"}{width="0.9120002187226597in"
height="0.910333552055993in"}{width="0.9120002187226597in"
height="0.910333552055993in"}

guarantee-free solutions that can operate on only an

colormapped version of a matrix. By treating matrix

rank as an image classification problem, we are able to

consistently achieve distressingly high performance --

$a$ (b) ©

Fig. 1. What are the ranks of these matrices? Which ones are
rank-deficient? In this paper, we investigate how one can guesstimate
the rank of a matrix from visual features alone. See footnote on page
2 for answer.

1 INTRODUCTION

Consider Figure 1(b): what is the rank of the matrix? Most people are
confused. Some might hazard a guess. A select collection of professors
might say "3." The mystery of how professors can visually estimate the
rank of matrices from as little as a brief glance at a jet-colormap
rendering has puzzled researchers in neuroscience, philosophy,
mathematics, and computer science for decades.

The rank of a matrix M reveals a great deal. By definition, it tells us
how many linearly independent columns the matrix has; surprisingly, it
also tells us how many linearly independent rows the matrix has, and if
that does not get you excited, I do not know what will. If we think of M
as an operator, the rank tells us about the dimensionality of its
output, and thus for a square matrix, whether M is invertible.

In this paper, we show how to identify the rank of a matrix from an
image alone. In contrast to past work on guaranteed solutions to
matrix rank computation

• All authors are with The Robotics Institute, Carnegie Mellon
University.

Send us fan mail at:

Neurotic Computing Institute ℅ D. Fouhey, A.B. M.S. EDSH 212

5000 Forbes Avenue

Pittsburgh, PA 15213

≈ 40% accuracy on 10-way classification; ≈ 80% accuracy on
rank-deficient/not-rank-deficient binary classification. In subsequent
experiments we show the following: 1) Our method can identify what
matrices seem low rank, and why; 2) Our method is easily extended to
structured prediction; 3) That activations of our network can be even
used as a feature for semantic image classification with
non-embarrassing performance (20*.*9% on Caltech 101 with 15 samples).

2 RELATED WORK

In this work, we tackle two problems concerning a square matrix M ∈
R*^n×n. The first is a binary classification problem: is M
full-rank? The second is a *k-way classification problem: what is the
rank of M?

Many approaches exist for solving both problems. In the binary case,
for instance, note that a square matrix is full rank if and only if
its determinant is non zero. This leads to a straight-forward way to
check for rank deficiency. Similarly, if we let UΣV*^T* = M be the
singular value decomposition of M (i.e., Σ*_i,i* = σ_i where
*σ_i*is the *i*th singular value of M), then the rank is the number
of non-zero singular values. This permits checking not only for rank
deficiency but also calculating the rank.

While these sorts of approaches enable the accurate solution of both
questions, they (a) require access to the matrix itself (as opposed to
a screen capture or printout) and (b) have time complexity greater
than O(n²). SVD computation has complexity O(n³) and
determinant calculation is O(n³) with Bareiss [1] or
O(n^2*.*807) with Bunch and Hopcroft [2]. Our work aims to fix
these gaps.

Our method requires only access to a visual repre sentation of the
matrix, and thus answers the purely

SIGBOVIK, APRIL 2015

1 2 3 4 5 6 7 8 9 10 {width="0.640333552055993in"
height="0.6370002187226597in"}{width="0.6386668853893264in"
height="0.6370002187226597in"}{width="0.640333552055993in"
height="0.6370002187226597in"}{width="0.6386668853893264in"
height="0.6370002187226597in"}{width="0.6386668853893264in"
height="0.6370002187226597in"}{width="0.640333552055993in"
height="0.6370002187226597in"}{width="0.6386668853893264in"
height="0.6370002187226597in"}{width="0.640333552055993in"
height="0.6370002187226597in"}{width="0.6386668853893264in"
height="0.6370002187226597in"}{width="0.6386668853893264in"
height="0.6370002187226597in"}{width="0.640333552055993in"
height="0.6386668853893264in"}{width="0.6386668853893264in"
height="0.6386668853893264in"}{width="0.640333552055993in"
height="0.6386668853893264in"}{width="0.6386668853893264in"
height="0.6386668853893264in"}{width="0.6386668853893264in"
height="0.6386668853893264in"}{width="0.640333552055993in"
height="0.6386668853893264in"}{width="0.6386668853893264in"
height="0.6386668853893264in"}{width="0.640333552055993in"
height="0.6386668853893264in"}{width="0.6386668853893264in"
height="0.6386668853893264in"}{width="0.6386668853893264in"
height="0.6386668853893264in"}

Fig. 2. Examples of matrices of various ranks. Top row: random
instances; Bottom row: archtypical examples of each rank, determined
by the most confident classification examples from a pool of 1,000
matrices according to a classifier.

visual way of computing rank as opposed to the mechanical way of
computing rank. When a professor says a matrix looks rank-deficient, she
is probably not doing an SVD, but instead using some visual smell-test
(akin to the notion of direct perception as proposed by psychologist
J.J. Gibson [3]); we seek to emulate this astounding ability.

Our method is O(n²). Feature extraction is only dependent on the
number of pixels for all methods and thus O(n²). If we are doing
binary classification, it is O(1) and thus the method serves as a
guarantee free quadratic-time rank-deficiency test. If we do n way
classification, it depends on the method, but is arguably O(1) for
random forests, which most of our methods use.

We acknowledge that our work gives no guar antees, but computer vision
has a long history of extraordinarily successful algorithms that may not
always be right. The Random Sample Consensus algo rithm [4], for
instance, can give no guarantees about its performance on any individual
problem instance. However, it works extraordinarily well in practice,
and the authors have taken it all the way to the proverbial citation
bank with a well-deserved *≈*10,000 citations. Similarly effective
methods include Simu lated Annealing, Iterative Conditional Modes (ICM)
[5], and many others. Our method may not be as successful, but as
presented in Table 1, our method is surprisingly effective and has a
certain je ne sais quoi.

Our approach of neural-network based approaches to linear algebra is
not itself novel. However, previous approaches (e.g., [6], [7],
[8], among many others) require direct access to the matrix itself.
Our approach, on the other hand, only gets access to an colormap of
the matrix.

The natural complement to the thematically-related related work
section (as above) is the alphabetically related related work section
introduced in Fouhey and Maturana's seminal work on celebrity-themed
learn ing [9]. In this paper, we extend this to a word-based

1. Answers first page quiz: a -- rank 1; b -- rank 3; c -- rank 10.

TABLE 1

A comparison of ways to check whether a matrix is rank deficient. We
evaluate methods on their time complexity, their success rate, whether
there is an easy extension to n-way rank calculation, and their Je
Ne Sais Quoi.

Method Complexity Success Multi-class Je ne sais Name (Time) Rate
Extension quoi

SVD O(n³) 100% Yes Minimal Det. O(n^2*.*807) 100%
No Kinda CNN O(n²) 78.6% Yes Tons

related work section. A highly related technique is the rank transform
proposed by Zabih and Woodfill [10]. This method replaces each pixel
by its "neighborhood rank" to achieve invariance to monotonic
illumination differences. We employ a related technique, Local Bi nary
Patterns [11] to extract features for our classifiers. Also related
are learning-to-rank algorithms such as support vector ranking [12].

3 TECHNICAL APPROACH

We now introduce the method in simple English to illustrate its
simplicity. We take a matrix, visualize it as a picture (like a.png),
and feed it into a standard image classification pipeline. More
formally, we create a fixed-length feature representation φ of the
image, and learn a mapping f that maps the representation to a set
of discrete classes. For instance, we might extract standard image
features like SIFT as φ, and apply a standard technique like Random
Forests or SVM to learn an f. Similarly, we might train a
convolutional neural network (CNN) to predict the rank, serving as
both φ and f. This classifier is simply trained on a collection of
random matrices. We note that one ele gant aspect of our method is
that rank-deficiency and classification are encapsulated in the same
learning formulation.

3.1 Features and Learning Method

In this paper, we apply standard image classification machinery by
substituting in various standard fea-

SIGBOVIK, APRIL 2015

TABLE 2

Quantitative results on visual rank problems. Our paradigm of
rank-prediction works surprisingly well across a myriad of features
and learning methods.

Learning method f Random Forest+Engineered RF + Pretrained Scratch
CNN Chance Feature map φ All Eng. Gray SIFT BoW Color SIFT BoW LBP
BoW pool₅ fc₇ Raw Pixels

10-way Rank 38.1% 32.5% 36.5% 31.0% 33.7% 34.9% 43.5% 10% Rank
Deficiency 76.4% 73.1% 75.3% 73.9% 75.0% 76.3% 78.6% 50%

tures and learning methods for φ and f. Shallow Learner +
Features: Features (φ): The first feature type we use is standard
hand-engineered fea tures in the form of a bag-of-words (i.e.,
histogram) representation over dense SIFT [13] and Local Binary
Patterns (LBP) [11]. To quantize SIFT, we build a codebook with
k-means; each extracted SIFT feature is represented by the nearest
cluster center (i.e., hard assignment). Thus, each image is mapped to
one or more histograms of codewords; we concatenate his tograms when
using multiple representations. We also experiment with using the
responses of a standard convolutional neural network -- Alexnet [14]
-- pre trained on the Imagenet dataset [15]. We use the standard
pool₅ and fc₇ features.

Learning Methods (f): We work with random forests [16] although our
method is entirely generic. In this method, an ensemble of decision
trees is trained inde pendently. During learning, splitting occurs on a
ran dom subset of features and occurs until a minimum number of samples
is in a leaf. Whenever training, we do 5-fold cross-validation on the
training data and select the values for both parameters (number of
features considered, minimum node size) that give maximum mean
performance.

Deep Learning: In keeping with the spirit of the deep learning
times, we train a CNN to map directly from pixels to matrix rank. We
refer to this as a Scratch CNN in the experiments since it is learned
from scratch. Our experiments use a small amount of data, so we adapt a
network designed for the MNIST dataset [17] that appears in the
examples for [18]. Starting with all images resized to 60*×60, our
network has architecture *C(5*,* 20) → P(4*,* 3) → C(5*,* 50) →
P(4*,* 3) → C(4*,* 500) → R → softmax, where C(k, n) denotes a
convolutional layer with n filters of size k × k, P(k, s) is
max-pooling over a k × k region with stride s, and R is a
rectified linear unit. Empirically, we found that the more aggressive
max-pooling than usual helped the network generalize to matrices of
other dimensions.

3.2 Implementation Details

We used Piotr Dollar's toolbox [19], Vedaldi et al.'s VLFeat [20],
MatConvNet [18], and LIBSVM [21]. SIFT: We extract and quantize
SIFT on both the gray image and each of the R, G, and B channels
separately; each codebook has 256 entries and one codebook is

generated on training data per channel. The code books are learned
once on the 10 × 10 training set. Scratch CNN: We use a learning
rate of 10^*−*3 in a standard gradient-descent+momentum approach and
1M iterations; to prevent overfitting, we use the first iteration to
have validation error within 1% of the final validation error.

4 EXPERIMENTS

We now rigorously evaluate our approaches for vi sually guesstimating
rank-related matrix properties. Every figure and table in this
section represents a true experiment and actual results. We do not
mess around.

4.1 Dataset

We perform our experiments on a dataset of 10 × 10 matrices, with
2000 examples of each rank 1*,...,* 10, which we split evenly into
train and test. When doing binary rank-deficiency classification, we
balance class distributions by downsampling the rank deficient class.
We generate these matrices by first sampling a matrix M with entries
uniformly and independently sampled from the interval [0*,* 1]. We
then compute its SVD M = UΣV*^T* _{and set Σ}^˜ to Σ but with the
_{r + 1*,...,n*th entries to 0 and compute UΣV}˜ ^T .

We convert each matrix to a 100*×*100 image, which we store as a PNG.
This is done in MATLAB by calling the underlying colormapping
functionality used by imagesc and then upsampling with nearest
neighbor. In this paper, we primarily use the traditional and often
criticized jet colormap, but we also experiment with two linear
colormaps, copper and bone. All colormaps have 255 possible values and
are scaled by the min and max of the matrices (i.e., the default of
imagesc, where no absolute scale is imposed). Note that the many
matrices of a variety of ranks may map to the same colormap
visualization due to both colormap and PNG quantization.

4.2 Experiments -- Features

In this section, we ask the question: what visual features are best
suited for visually identifying the rank of a matrix? Is color a
useful cue? It was argued in [22] that off-the-shelf pre-trained CNN
features are an astoundingly effective baseline for any generic vision
task -- does this include profoundly unnatural

SIGBOVIK, APRIL 2015

{width="1.0420002187226596in"
height="1.0386668853893264in"}{width="1.0420002187226596in"
height="1.0386668853893264in"}{width="1.0436668853893263in"
height="1.0386668853893264in"}{width="1.080333552055993in"
height="1.0770002187226597in"}{width="1.080333552055993in"
height="1.0770002187226597in"}{width="1.080333552055993in"
height="1.0770002187226597in"}

Jet (38*.1%) Bone (35.2%) Copper (33.*6%)

Fig. 3. Confusion matrices and accuracies for different colormaps on
the 10-way rank classification problem using dense SIFT and LBP. Note
that while there is variation, performance is decidedly above chance
across colormaps.

images such as color-mapped matrices? Does learning a specialized CNN
work on this task?

We present results in Table 2 showing the perfor mance of various
features. In the hand-engineered category, grayscale SIFT seems to
perform on par with LBP; adding color considerably improves per
formance; and using all features does the best. The pretrained CNN
does well despite the giant domain shift with both layers do slightly
better than grayscale SIFT. However, in keeping with current results
in computer vision, training a CNN from scratch consis tently does the
best. Note, however, that all feature and method combinations operate
at significantly above chance level.

4.3 Experiments -- Colormaps

One natural question is whether the colormapping scheme affects the
visual discrimination between ma trices of different ranks. The jet
colormap (e.g., Figs. 1, 5) in particular has received a lot of
criticism for being difficult to interpret in practice by humans. Lin
ear colormaps (i.e., smoothly varying from one color to another) in
theory make for easier interpretation by humans. We see whether this
holds true for computers as well. We compare the jet colormap (named for
its origin in astrophysical fluid jet simulation) with copper and bone.
The etymology of copper is -- we hope for the reader's sake -- obvious;
bone is so named because it looks somewhat like an X-ray and is popular
because it lets researchers like us try to pretend to be brain-surgeons.

We run our learning method on matrices with a variety of colormaps and
report 10-way classification results in Fig. 3 and 4. Generally, jet
does the best. The only representation on which it does appreciably
worse is the pre-trained CNN; we hypothesize this is because the linear
colormaps produce more natural images, whereas the jet colormap's
outputs look like noise. Using grayscale SIFT, the results are roughly
comparable, which is somewhat surprising as jet is known to convert
poorly to grayscale. Nonetheless, while these differences exist, one
consistent pattern is that the proposed method works surprisingly well
across all colormaps.

$P$ 3 / (A) 1 (P) 10 / (A) 2 (P) 2 / (A) 10 Predicted / Actual Rank

Fig. 5. Failure cases: some deceptive matrices with their (P)redicted
and (A)ctual ranks, selected from the most confi dent mistakes of a RF
classifier using dense SIFT and LBP features.

4.4 Experiments -- Cross Domain

One recent pressing concern in the computer vision community is the
biased nature of datasets: models learned on one dataset might not
perform even rea sonably on another, as reported in [23]. In our
case, one might wonder whether a model learned to predict the rank of
a 10 × 10 matrix (with a fixed set of ranks 1*,...,* 10) can
generalize to matrices of different sizes (e.g., 30 × 30). To answer
this, we train a 10- class random forest on square matrices of
dimensions 10, 15, and 30, and test them on different sizes; bag
of-word features are generated using the 10 × 10 matrix codebooks.
These new matrix images have dimensions 150 × 150 and 300 × 300
respectively to maintain scale for the SIFT features. CNNs require a
fixed input, and so we cannot apply this scaling trick to them.

We train a model to predict ranks 1*,...,* 10 for all matrix sizes
involved and report results in Table 3. Our method does surprisingly
well, performing at around 2*.5×* chance-level when training on 10
× 10 matrices and testing on 30 × 30 matrices and vice versa. The
scratch CNN generalizes well, with the exception of the 30 × 30
scratch CNN on 10 × 10 data, which operates at chance level. This is
poor generalization as opposed to a bad model to start with: the same
model gets 49*.7% when testing on 30×30 and 14.6% on 15×*15. We
believe generalization could be improved by developing an architecture
that would enable the row-to-pixel ratio to be constant.

5 DISCUSSION

The success of such a simple approach raises a num ber of questions,
but our method also enables answer to some of these. For instance, we
can see what makes a matrix smell rank deficient by analyzing the
learned relationship between φ and f. We now discuss a few of
these questions as well as extensions.

5.1 What does an archetypical rank-***k* **matrix look like and
which matrices are tricky to classify? We can answer each of these
questions by looking at the classifier scores; by looking at the most
confident

SIGBOVIK, APRIL 2015

50

45

40

35

y

c

a

30

r

u

c

25

c

A

20

y

a

w

15

−

0

10

1

5

_{All E. BoWC BoWg LBP P5 FC7 Scratch All E. BoWC BoWg LBP P5 FC7 Scratch All E. BoWC BoWg LBP P5 FC7 Scratch}
0 Colormap + Method

Fig. 4. What colormap is best for predicting matrix rank? (Left to
right: jet, bone, copper). While Jet has been criticized widely
compared to linear colormaps, it produces the best results with color
sift and the from-scratch CNN

TABLE 3

Cross-domain performance: We report the accuracy of the methods on
10-way classification. Although chance on this task is 10%, most of
our methods perform substantially better than chance.

Train Test Random Forest+Engineered RF + Pretrained Scratch CNN Dim.
Dim. All Eng. Gray SIFT Color SIFT LBP pool₅ fc₇ Raw Pixels
10 × 10 38.1% 32.5% 36.5% 31.0% 33.7% 34.9% 43.5%

10 × 10

15 × 15 33.7% 31.5% 33.5% 27.3% 25.7% 26.1% 37.9% 30 × 30
25.9% 19.1% 25.3% 19.4% 17.7% 17.5% 24.1%

^{15 × 15} _{10 × 10} 33.0% 28.1% 32.0% 26.5% 13.9% 14.4%
34.1% 30 × 30 25.8% 22.7% 23.8% 21.6% 11.5% 11.8% 10.0%

mistakes of the classifier, we can find the most rank deceptive
matrices. We present some archetypical ma trices in Fig. 2 according
to RF classifier using all features. While the rank 1 matrix archetype
is under standable, ranks 2 and up seem inscrutable. Nonethe less, the
model is perfectly confident in its assessment of these matrices and
is correct a surprising amount of time. Fig. 5 shows the model's
confident mistakes. On the left, for instance, is shown a rank-1
matrix with not too much apparent inter-row/column similarity that was
mistakenly predicted to rank 3 by the RF.

5.2 What parts of matrices tell us rank?

Given our bag-of-words model, we can answer this by figuring out which
codewords help the most in predicting rank as well as their sign (i.e.,
which codes are most associated with rank-1 rather than rank-10). We
solve both by learning a L₂-regularized logistic regression model to
predict Rank-i or Rank-j, which we solve with LIBLINEAR [24]. The
regularization parameter λ is selected via 5-fold cross-validation to
give best average performance. The coefficients of the model w in terms
of magnitude and sign indicate which codewords are indicative of rank
deficiency.

We can visualize the informative regions of matrices by replacing pixels
with the weight vector of their as sociated codewords. We show a few
examples of this for low rank and high rank matrices using grayscale
SIFT in Fig. 6. For rank 1, the regions associated with low rank have
low frequency, and the codewords associated with high rank occur mainly
at the sharp transition from the penultimate and blue column to the last
column. The other ranks are a bit harder to

Image All High Weight
{width="0.9120002187226597in"
height="0.910333552055993in"}{width="0.9120002187226597in"
height="0.910333552055993in"}{width="0.9119991251093613in"
height="0.910333552055993in"}Rank 1

{width="0.9120002187226597in"
height="0.9086668853893264in"}{width="0.9120002187226597in"
height="0.9086668853893264in"}{width="0.9119991251093613in"
height="0.9086668853893264in"}Rank 2

{width="0.9120002187226597in"
height="0.910333552055993in"}{width="0.9120002187226597in"
height="0.910333552055993in"}{width="0.9119991251093613in"
height="0.910333552055993in"}Rank 10

Fig. 6. A visualization of what makes a matrix look rank deficient
according to gray-scale SIFT. We train a logistic regressor to predict
rank-k vs. full rank and plot weight-vector coefficients onto the
image wherever the codeword appears. Blue is low rank, red high.

interpret, although the one can note the most strongly low-rank
regions correspond to flat regions.

5.3 Can We Solve Structured Tasks?

So far, our approach of doing mathematics by learning has only been
applied to classification problems. In-

SIGBOVIK, APRIL 2015

Fig. 7. Examples from our deep visual multiplication net. A B Pred.
A · B True A · B MSE
{width="0.6270002187226597in"
height="0.590333552055993in"}{width="0.6270002187226597in"
height="0.590333552055993in"}{width="0.625333552055993in"
height="0.590333552055993in"}{width="0.625333552055993in"
height="0.590333552055993in"}0.033
{width="0.6270002187226597in"
height="0.5870002187226596in"}{width="0.6270002187226597in"
height="0.5870002187226596in"}{width="0.625333552055993in"
height="0.5870002187226596in"}{width="0.625333552055993in"
height="0.5870002187226596in"}0.014
{width="0.6270002187226597in"
height="0.5870002187226596in"}{width="0.6270002187226597in"
height="0.5870002187226596in"}{width="0.625333552055993in"
height="0.5870002187226596in"}{width="0.625333552055993in"
height="0.5870002187226596in"}0.012

spired by our success in visual rank estimation, we are currently
exploring the application of our framework to structured outputs, such
as matrices.

In particular, we consider matrix multiplication and inversion, where
for centuries mathematicians have relied on hand-crafted, shallow
methods. Again, keeping with the times we propose to replace these
methods with visual deep learning. To this end we designed a deep
learning architecture, differing only in the input for each task: for
the multiplication task we used two M × M concatenated multiplicands
as input, whereas in the inversion task there is a single M × M
input. The input is connected to two fully connected layers using ReLU
nonlinearities of 512 hidden units each, followed by a fully connected
M × M output layer with no nonlinearity. Dropout regularization was
used in all layers. We generate 5 · 10⁵ training examples for each
task. In both cases we use 3 × 3 matrices with each entry
independently sampled from a uniform(0*,* 1) distribution as input,
and their "true"² product and inverse as outputs.

We then use this data to train the network with stochastic gradient
descent on a mean square error (MSE) loss for 100 epochs. Some
qualitative predic tions on unseen data are shown in Figures 7 and 8. We
found the multiplication task to be easily solved by our network
architecture, but the inversion task proved much more challenging, as
shown by the higher MSE values. We note that this is analogous to humans
taking Linear Algebra 101.

5.4 Can This Work On Real Data?

One advantage of our method is that it does not require access to the
matrices themselves; but what if we only have a picture of the
colormapped matrix? As a proof of concept, we took a cell-phone
picture of each part of Fig. 1 of this paper, as shown in Fig. 9,
left. We cropped out the matrix from the cell phone picture, as shown
in Fig. 9, right. We then resized

2. At least according to our matrix library.

Fig. 8. Examples from our deep visual matrix inverse net. A
Predicted A⁻¹ True A⁻¹ MSE
{width="0.625333552055993in"
height="0.590333552055993in"}{width="0.6270002187226597in"
height="0.590333552055993in"}{width="0.6270002187226597in"
height="0.590333552055993in"}0.25
{width="0.625333552055993in"
height="0.5870002187226596in"}{width="0.6270002187226597in"
height="0.5870002187226596in"}{width="0.6270002187226597in"
height="0.5870002187226596in"}0.49
{width="0.625333552055993in"
height="0.5870002187226596in"}{width="0.6270002187226597in"
height="0.5870002187226596in"}{width="0.6270002187226597in"
height="0.5870002187226596in"}1.56
{width="0.5220002187226597in"
height="0.6870002187226597in"}{width="0.725333552055993in"
height="0.6870002187226597in"}{width="0.8286668853893263in"
height="0.6870002187226597in"}{width="0.7820002187226597in"
height="0.6870002187226597in"}1 (92*.8%) 10 (48.1%) 10 (45.*5%)

Fig. 9. Results on cropped images from cell-phone pictures of a
computer monitor. (Left) sample pre-cropped image; (right) cropped
images, their predicted rank, and posterior from the scratch CNN.

it and sent it through our scratch CNN. The rank 1 matrix was
classified correctly, but both the rank 3 and rank 10 matrix were
classified as rank 10. We note, however, that all images have
perspective distortion that the CNN did not see at training time.

5.5 Does the matrix rank network generalize? In our experiments,
we confirmed the reports of [22] that one can use neuron activations
from a network pretrained for classification as a strong feature for a
variety of tasks; but can we use do the reverse? In other words, can
we use activations in our scratch CNN as a feature for image
classification?

To evaluate this, we tested our method on the Caltech 101 dataset
[25]. We used the concatenated features from the last and
second-to-last layers of the rank network (i.e., the softmax responses
and the half wave rectified feature map immediately before) as a
feature representation. We then trained a multiclass SVMs (1v1, linear
kernel) on top of these representa tions. We report results in Table
4; results are averaged over 1*K* random samplings of train sets; for
test, we use an equal number per-class. While far from
state-of-the-art, the numbers are respectable given that the
underlying feature representation was trained to estimate matrix
ranks.

6 CONCLUSIONS

In this paper, we introduced a new problem -- visual rank estimation
-- and demonstrated that it is feasible

SIGBOVIK, APRIL 2015

TABLE 4

Results on Caltech 101, training a linear SVM over responses from our
scratch rank CNN. Chance on this dataset is ≈ 1%.

# Samples 5 10 15 20 25 Accuracy 12*.6% 17.7% 20.9% 23.3%
25.*1%

using conventional image classification approaches. Our approach is
simple and obtains alarmingly high performance. More importantly, our
features also con veys understanding by showing us why some ma trices
just look low rank and what matrices have surprising rank. We have
additionally demonstrated future directions in the form of structured
prediction and have demonstrated that our rank predictor CNN can serve
as a generic image feature.

REFERENCES

[1] E. Bareiss, "Sylvester's identity and multistep integer
preserving Gaussian elimination," Mathematics of Computation, vol.
22, no. 102, 1968.

[2] J. Bunch and J. Hopcroft, "Triangular factorization and inver
sion by fast matrix multiplication," Mathematics of Computation,
vol. 28, no. 125, 1974.

[3] J. Gibson, The Ecological Approach to Visual Perception. 1979.
[4] M. Fischler and R. Bolles, "Random sample consensus: A paradigm
for model fitting with applications to image analysis and automated
cartography," Commun. of the ACM, vol. 24, June 1981.

[5] J. Besag, "On the statistical analysis of dirty pictures,"
Journal of the Royal Statistical Society, Series B (Methodological),
vol. 48, no. 3, pp. 259--302, 1986.

[6] J. J. Hopfield and D. W. Tank, ""Neural" computation of deci
sions in optimization problems," Biological Cybernetics, vol. 52,
pp. 141--152, 1985.

[7] M. Kennedy and L. Chua, "Neural networks for nonlinear pro
gramming," Circuits and Systems, IEEE Transactions on, vol. 35, pp.
554--562, May 1988.

[8] A. Cichocki and R. Unbehauen, "Neural networks for solving
systems of linear equations and related problems," Circuits and
Systems I: Fundamental Theory and Applications, IEEE Transac tions
on, vol. 39, pp. 124--138, Feb 1992.

[9] D. F. Fouhey and D. Maturana, "The Kardashian Kernel," in
SIGBOVIK, 2012.

[10] R. Zabih and J. Woodfill, "Non-parametric local transforms for
computing visual correspondence," in ECCV, 1994. [11] T. Ojala, M.
Pietikainen, and T. Maenpaa, "Multiresolution gray-scale and rotation
invariant texture classification with local binary patterns," TPAMI,
vol. 24, no. 7, 2002. [12] T. Joachims, "Optimizing search engines
using clickthrough data," in KDD, 2002.

[13] D. Lowe, "Distinctive image features from scale-invariant
keypoints," IJCV, vol. 60, no. 2, pp. 91--110, 2004.

[14] A. Krizhevsky, I. Sutskever, and G. E. Hinton, "Imagenet
classification with deep convolutional neural networks," in NIPS,
2012.

[15] O. Russakovsky, J. Deng, H. Su, J. Krause, S. Satheesh, S. Ma,
Z. Huang, A. Karpathy, A. Khosla, M. Bernstein, A. C. Berg, and L.
Fei-Fei, "ImageNet Large Scale Visual Recognition Challenge," 2014.

[16] L. Breiman, "Random forests," Machine Learning, vol. 45, no.
1, pp. 5--32, 2001.

[17] Y. LeCun, L. Bottou, Y. Bengio, and P. Haffner, "Gradient-based
learning applied to document recognition," Proceedings of the IEEE,
vol. 86, no. 11, pp. 2278--2324, 1998.

[18] A. Vedaldi and K. Lenc, "Matconvnet -- convolutional neural
networks for matlab," CoRR, vol. abs/1412.4564, 2014.

[19] P. Dollar, "Piotr's Image and Video Matlab Toolbox (PMT)." ´
http://vision.ucsd.edu/ pdollar/toolbox/doc/index.html. [20] A.
Vedaldi and B. Fulkerson, "VLFeat: An open and portable library of
computer vision algorithms." http://www.vlfeat.org/, 2008.

[21] C.-C. Chang and C.-J. Lin, "LIBSVM: A library for support vector
machines," ACM Transactions on Intelligent Systems and Technology,
vol. 2, pp. 27:1--27:27, 2011. Software available at
http://www.csie.ntu.edu.tw/ cjlin/libsvm.

[22] A. S. Razavian, H. Azizpour, J. Sullivan, and S. Carlsson, "Cnn
features off-the-shelf: an astounding baseline for recognition," CoRR,
vol. abs/1403.6382, 2014.

[23] A. Torralba and A. A. Efros, "Unbiased look at dataset bias," in
CVPR, 2011.

[24] R.-E. Fan, K.-W. Chang, C.-J. Hsieh, X.-R. Wang, and C.-J. Lin,
"LIBLINEAR: A library for large linear classification," Journal of
Machine Learning Research, vol. 9, pp. 1871--1874, 2008.

[25] L. Fei-Fei, R. Fergus, and P. Perona, "Learning generative visual
models from few training examples: An incremental bayesian approach
tested on 101 object categories," in IEEE CVPR Workshop of Generative
Model Based Vision (WGMBV), 2004.

David F. Fouhey David F. Fouhey received
{width="0.8170002187226597in"
height="1.2236668853893264in"}

an A.B. from Middlebury College in Moose

Watching in 2011. He is currently a Ph.D.

student at the Robotics Institute at Carnegie

Mellon University. He likes long walks, Ed

ward Hopper, macchiatos, Jaffa Cakes, and,

above all, kvetching. In his copious spare

time, he sends fake announcements to the

New York Times' Wedding Section. He and his

colleagues were awarded the People's Demo

cratic Choice Award at SIGBOVIK 2013.

Daniel Maturana Daniel comes from Chile.
{width="0.925333552055993in"
height="1.2220002187226597in"}

Daniel likes Eat'n Park, bicycling, recycling,

and Pabst Blue Ribbon. You won't believe

the one weird trick that credit card compa

nies hate that Daniel uses to make money

at home thanks to Obama lowering 10-year

mortgage rates! He and his colleagues were

awarded the People's Democratic Choice Award

at SIGBOVIK 2013.

Rufus von Woofles Rufus von Woofles is a
{width="0.9820002187226596in"
height="1.080333552055993in"}

good boy, isn't he. Yesh he is. Rufus obtained

his DoD (Doggy Obedience Diploma), First

Class, from Muddy Paws University. Rufus

is currently the PI of CHOCOLATE Lab at

Carnegie Mellon University, where he leads

research on predicting pizza-delivery-man

appearance. Rufus likes wagging his tail and

belly rubs. Rufus was awarded the People's

Democratic Choice Award at SIGBOVIK 2013,

but he tore it up.

Transparency Report

United States Three Letter Agency

1 April 2015

Here at Three Letter Agency, we care deeply about transparency. We
have implemented a transparency policy carefully designed to ensure
that trans parency is at the heart of everything we do. Transparency
means that you can set your mind at ease. Our track record proves that
transparency is a top priority for us. We are more transparent than
air itself. Transparency is our commitment to you. Our mission is to
be the most transparent agency on the planet. We worry about
transparency so that you don't have to. We take transparency very
seriously. We use transparencies in all of our presentations. Finger
lickin' transparent. Taste the transparency. Always transparent. We
conduct regular transparency audits. We once briefly believed that we
were not being transparent, but it was a mistake. A transparent proxy
intercepts normal communication at the network layer without requiring
any special client configuration, such that clients need not be aware
of the existence of the proxy. Transparency keeps you safe. We have a
long tradition of transparent processes and outcomes. We make
transparency work for you. Transparency is in our DNA. Think
transparent. Got transparency? So transparent, no wonder it's number
one. Every breath you take, every move you make, we'll be transparent.

7UDFN /

/XQFK ,QWHUPLVVLRQ

%XUULWRV IRU WKH +XQJU\ 0DWKHPDWLFLDQ

(G 0RUHKRXVH

.H\ZRUGV EXUULWRV PRQDGV ZK\ GLG L VSHQG P\ GD\ GRLQJ WKLV LQVWHDG
RI UHDO ZRUN\"

\"m``BiQb 7Q` i?2 >mM;`v J i?2K iB+B M

1/ JQ`2?Qmb2

T`BH R- kyR8

#bi` +i

h?2 /p2Mi Q7 7 bi@+ bm H J2tB+ M@bivH2 /BMBM; 2bi #HBb?K2Mib- bm+? b
*?BTQiH2 M/ Z/Q# - ? b ;`2 iHv BKT`Qp2/ i?2 T`Q/m+iBpBiv Q7 `2b2
`+? K i?2K iB+B Mb M/ i?2Q`2iB+ H +QKTmi2` b+B2MiBbib BM `2+2Mi v2
`bX aiBHH K Mv 2tT2`B2M+2 +QM7mbBQM mTQM 2M+QmMi2`BM; #m``BiQb
7Q` i?2 7B`bi iBK2X

LmK2`Qmb #m``BiQ imiQ`B Hb UQ7 p `vBM; [m HBivV `2 iQ #2 7QmM/
QM i?2 AMi2`M2iX aQK2 /2b+`B#2 #m``BiQ b i?2 BK ;2 Q7 +`āT2
mM/2` i?2 +iBQM Q7 i?2 M2r@rQ`H/ 7mM+iQ`X \"mi bm+? +? ` +i2`Bx
iBQMb K2`2Hv b2`p2 iQ `2BM/2t i?2 +QM7mbBQM +QMi` p `B MiHvX
Pi?2`b BMbBbi i? i i?2 QMHv r v iQ `2 HHv mM/2`bi M/ #m``BiQb Bb
iQ 2 i K Mv /B772`2Mi FBM/b Q7 #m``BiQ mMiBH i?2 +QKKQM mM/2`HvBM;
+QM+2Ti #2+QK2b TT `2MiX

Ai ? b #22M `2+2MiHv `2K `F2/ #v uQ`;2v (N) i? i #m``BiQ + M #2
`2; `/2/ b M BMbi M+2 Q7 mMBp2`b HHv@mM/2`biQQ/ +QM+2Ti- M K2Hv-
i? i Q7 KQM /X Ai Bb i?Bb +? ` +i2`Bx iBQM i? i r2 BMi2M/ iQ 2tTHB+
i2 ?2`2X hQ rBi-

m``BiQ Bb Dmbi bi`QM; KQM / BM i?2 bvKK2i`B+ KQMQB/ H#

+ i2;Q`v Q7 7QQ/c r? iǶb i?2 #B; /2 H\5

R h?2 * i2;Q`v Q7 6QQ/

h?2 + i2;Q`v Q7 7QQ/- 6Ƚ/- Bb 7mHH bm#+ i2;Q`v Q7 i?2 + i2;Q`v
Q7 bim77- ai7- r?Qb2 Q#D2+ib `2 i?2 bim77 vQm + M 2 iX KQ`T?BbK Q7
i?Bb + i2;Q`v Bb FMQrM b **`2+BT2**X h?Bb + i2;Q`v BM?2`Bib i?2
K#B2Mi KQMQB/ H T`Q/m+i, B7 vQm + M 2 i + ``Qi M/ vQm + M 2 i TQi
iQ- i?2M vQm + M 2 i + ``Qi M/ TQi iQX h?2 KQMQB/ H mMBi BM i?2 +
i2;Q`v Q7 7QQ/ Bb MQi?BM;- ၥ- r?B+? Bb iQ #2 7QmM/ BM K Mv ;` /m i2
bim/2MibǶ `27`B;2` iQ`b- ivTB+ HHv- i2MbQ`2/ rBi? #22`X

h?2 KQMQB/ H + i2;Q`v 6Ƚ/ Bb bvKK2i`B+, B7 vQm + M 2 i + ``Qi M/
TQi iQ i?2M vQm + M 2 i TQi iQ M/ + ``QiX >Qr2p2`- Bi 7 BHb iQ #2
*+ `i2bB M*X q2 H +F i?2 T`QD2+iBQMb, B7 r2 ? p2 K /2 i?2 KBbi F2 Q7
Q`/2`BM; r?BbF2v bQm`- i?2`2 Bb ;2M2` HHv MQ r v iQ `2+Qp2`
Dmbi i?2 r?BbF2vX LQ` /Q r2 ? p2 /B ;QM H M im` H i` Mb7Q`K iBQM-
Ⴍ \" ਾ \" ܿ \" ૵ \"- ;BpBM; mb irQ r?BbF2vb 7Q` i?2 T`B+2 Q7 QM2 Ĝ H
bX 6Q` 7m`i?2` /2i BHb QM i?2 i?2Q`v Q7 + i2;Q`B+ H +QQF2`v- b22
(R)X

k h?2 hQ`iBHH 1M/Q7mM+iQ`

h?2 + i2;Q`v Q7 7QQ/ bmTTQ`ib M 2M/Q7mM+iQ`- 5 ਾ 6Ƚ/ ܿ 6Ƚ/- FMQrM b
i?2 **iQ`iBHH 2M/Q7mM+iQ`**X P#D2+ib BM i?2 BK ;2 Q7 i?Bb 7mM+iQ`
`2 T`2+Bb2Hv i?Qb2 i? i `2 r` TT2/ BM iQ`iBHH X h?2 +iBQM Q7 i?2
7mM+iQ` 5 QM KQ`T?BbKb Bb iQ i F2 `2+BT2 M/ vB2H/ `2+BT2 7`QK
iQ`iBHH \@r` TT2/ BM;`2/B2Mib iQ iQ`iBHH @ r` TT2/ `2bmHibX

LQi2 i? i i?2 iQ`iBHH 2M/Q7mM+iQ` Bb- BM ;2M2` H- MQi KQMQB/ HX
:Bp2M iQ`iBHH @ r` TT2/ `B+2 M/ #2 Mb- Bi Bb mbm HHv MQi TQbbB#H2
iQ `2+Qp2` iQ`iBHH \@r` TT2/ `B+2 M/ iQ`iBHH \@r` TT2/ #2 MbX
LQ` Bb Bi Hr vb TQbbB#H2 iQ T`Q/m+2 iQ`iBHH @ r` TT2/ MQi?BM; Qmi
Q7 MQi?BM;X

j h?2 \"m``BiQ JQM /

Ai Bb mMBp2`b HHv mM/2`biQQ/ i? i KQM / QM + i2;Q`v ජ Bb
+QKT`Bb2/ Q7 (e) M 2M/Q7mM+iQ` 5ਾජܿජ M/ irQ M im` H i` Mb7Q`K
iBQMb- ၓ ਾ JE ජ ܿ 5 M/ ၙਾ5^ɞ ܿ 5- FMQrM `2bT2+iBp2Hv b i?2 KQM /
mMBi M/ KmHiBTHB+ iBQM b iBb7vBM; i?2 KQMQB/ mMBi M/ bbQ+B
iBp2 H rb,

ၓ ਼ ਼5 ਼ ၙ JE 5 5 ਼ ਼ၓ ਼ ၙ ਾ 5 ܿ 5

M/

ၙ ਼ ਼5 ਼ ၙ 5 ਼ ਼ၙ ਼ ၙ ਾ 5^ɘ ܿ 5

AM i?2 + b2 Q7 i?2 #m``BiQ KQM /- i?2 7mM+iQ` BM [m2biBQM Bb- Q7
+Qm`b2- i?2 iQ`iBHH 2M/Q7mM+iQ`X

h?2 #m``BiQ KQM / mMBi i F2b bQK2i?BM; vQm + M 2 i M/ r` Tb Bi BM
iQ`iBHH - vB2H/BM; bBKTH2 #m``BiQ- r?B+? Bb #Qi? iQ`iBHH \@r`
TT2/ M/ 2/B#H2 Ĝ MQ K2 M 72 iX h?Bb +QMbiBimi2b i?2 7 KBHB `
BMb2`iBQM Q7 ;2M2` iQ`b (8)X >Qr2p2`- BM i?2 + b2 Q7
H2bb@pBb+Qmb ;2M2` iQ`b- bm+? b ;m + KQH2- bQK2 + `2 K v #2
`2[mB`2/ BM i?2 BMb2`iBQM- M/ Bi Bb Q7i2M 2 bB2` iQ BMb2`i i?2
;2M2` iQ` BMiQ i?2 KQM / mbBM; MQxxH2 ` i?2` i? M #v i?2 Q#pBQmb
7QH/BM; K TX

h?2 #m``BiQ KQM / KmHiBTHB+ iBQM i F2b +QKTQmM/ #m``BiQ- i? i
Bb- bQK2@ i?BM; vQm + M 2 i i? i Bb /Qm#H2@r` TT2/ BM iQ`iBHH b- M/
K2`;2b i?2 irQ iQ`@ iBHH b BMiQ bBM;H2 r` TTBM;X h?Bb i2M/b iQ ?
TT2M bTQMi M2QmbHv BM i?2 + b2 Q7 M Qp2` #mM/ M+2 Q7 i?2
T`2pBQmbHv@K2MiBQM2/ H2bb@pBb+Qmb ;2M2` iQ`b- H@ i?Qm;? bBKBH `
2772+i + M #2 +?B2p2/ K2+? MB+ HHv #v mbBM; bQK2 7Q`+2 M/ i?2 7H
ii2MBM; 7mM+iBQM Ub?QmH/ r2 +Bi2 i?2 +` TTv : #Q` T T2` ?2`2\V
(k)X

LQr r2 Kmbi +?2+F i? i i?2 KQM / H rb `2 b iBb7B2/,

KQM / `B;?i mMBi H r, h?Bb H r b vb i? i B7 vQm #2;BM rBi?
bQK2i?BM; vQm + M 2 i i? iǶb r` TT2/ BM iQ`iBHH M/ vQm r` T i?2
r?QH2 i?BM; BM MQi?2` iQ`iBHH - i?2M K2`;2 i?2 iQ`iBHH b- vQm ;2i
# +F r? i vQm bi `i2/ rBi?- b i?2 `2 /2` K v /2HB+BQmbHv p2`B7vX

KQM / H27i mMBi H r, h?Bb H r b vb i? i B7 vQm #2;BM rBi?
bQK2i?BM; vQm + M 2 i i? iǶb r` TT2/ BM iQ`iBHH M/ vQm mMr` T Bi-
`2KQp2 i?2 +QMi2Mib

M/ r` T i?2K BM MQi?2` iQ`iBHH - i?2M r` T i?2 `2bmHi # +F mT BM
i?2 Q`B;BM H iQ`iBHH M/ K2`;2 i?2 irQ r` TTBM;b- i?2 2772+i Bb ;
BM i?2 B/2M@ iBiv 7mM+iBQMX

KQM / bbQ+B iBp2 H r, h?Bb H r b vb i? i B7 vQm ? p2
i`BTH2@iQ`iBHH \@r` TT2/ i?BM; vQm + M 2 i M/ vQm K2`;2 i?2 BMM2`
irQ iQ`iBHH b- i?2M K2`;2 i?2 `2bmHi rBi? i?2 Qmi2` iQ`iBHH - i?2
2772+i Bb i?2 b K2 b B7 vQm ? / K2`;2/ i?2 Qmi2` irQ iQ`iBHH b
7B`bi- M/ i?2M i?2 `2bmHi rBi? i?2 BMM2` QM2X

9 6`QK \"m``BiQb- ai`2M;i?

h?2 #m``BiQ KQM / Bb BM 7 +i bi`QM;X KQM / 5 ၓ ၙ QM KQMQB/ H +
i2;Q`v ජ ૵ * Bb bi`QM; B7 i?2`2 Bb M im` H i` Mb7Q`K iBQM-

ၟ \" # ਾ \" ૵ 5 # ܿ 5 \" ૵ #

b iBb7vBM; +2`i BM `2H iBQMb (j)X AM i?2 + b2 Q7 bi`B+i KQMQB/
H + i2;Q`v- bm+? b 6Ƚ/- i?2b2 KQmMi iQ i?2 `2[mB`2K2Mi i? i ၟ #2
KQ`T?BbK Q7 i?2 KQM / bi`m+im`2X h?2 +Q``2bTQM/BM; H rb `2,

JE \" ૵ ၓ # ਼ ၟ \" # ၓ \" ૵ # ਾ \" ૵ # ܿ 5 \" ૵ #

M/

JE \"૵ၙ #਼ၟ \"# ၟ \"5 #਼5 ၟ \"#਼ၙ \"૵# ਾ \" ૵ 5^ɞ # ܿ 5 \" ૵ #

AM i?2 + b2 Q7 i?2 #m``BiQ KQM /- i?2 bi`2M;i?- ၟ- Bb i?2 ǳr`
TTBM; BMǴ i` Mb7Q`K iBQM- r?B+? i F2b ǳbB/2Ǵ Q#D2+i \" M/ #m``BiQ
5 # M/ vB2H/b #m``BiQ BM r?B+? i?2 bB/2 ? b #22M r` TT2/ BM iQ i?2

m``BiQX h?Bb Bb KQbi +H2 `Hv BHHmbi` i2/ #v M 2t KTH2X amTTQb2 i?#

i vQm #2;BM rBi? #2 M #m``BiQ M/ bB/2 Q7 ;m + KQH2X \"v ǳr` TTBM;
BMǴ i?2 bB/2- vQm K v Q#i BM #2 M M/ ;m + KQH2 #m``BiQ Ĝ r?B+? Bb
+H2 `Hv #2ii2`X AM i?Bb + b2- i?2 KQM / bi`2M;i? H rb `2[mB`2
i?2 7QHHQrBM;,

bi`2M;i? mMBi H r, A7 vQm 7B`bi BMb2`i bQK2 #2 Mb BMiQ bBKTH2

m``BiQ M/ M2ti r` T@BM bB/2 Q7 ;m +- i?2 2772+i Bb i?2 b K2 b B7#

vQm ? / BMb2`i2/ i?2 ;m + M/ #2 Mb BMiQ bBKTH2 #m``BiQ iQ;2i?2`X

bi`2M;i? KmHiBTHB+ iBQM H r, A7 vQm ? p2 +QKTQmM/ #2 M #m``BiQ
i? i vQm 7B`bi K2`;2 BMiQ bBKTH2 QM2 M/ vQm i?2M r` T@BM bB/2 Q7 ;m
+- i?2 2772+i Bb i?2 b K2 b B7 vQm ? / r` TT2/ i?2 ;m + BMiQ i?2
Qmi2`- #2 M #m``BiQ- #m``BiQ- i?2M r` TT2/ i?2 UMQr BMi2`biBiB
HV ;m + BMiQ i?2 BMM2`- #2 M- #m``BiQ- M/ i?2M 7BM HHv K2`;2/ i?2
+QKTQmM/ ;m + M/ #2 M #m``BiQ

BMiQ bBKTH2 QM2X h?Bb H bi 2[mBp H2M+2 Bb T2`? Tb #2bi mM/2`biQQ/
b, ;m + M/ UU#2 M #m``BiQV #m``BiQV

;m + M/ UU#2 M #m``BiQV #m``BiQV ࠯> K2`;2 +QKTQmM/ #m``BiQ>

[]{dir="rtl"}࠯> r` T@BM ;m + iQ Qmi2` #m``BiQ> U;m + M/ U#2 M

m``BiQVV #m``BiQ#

;m + M/ U#2 M #m``BiQV

[]{dir="rtl"}࠯> r` T@BM ;m +>

U;m + M/ #2 MV #m``BiQ

8 6mM+iBQM H \"m``BiQb

[]{dir="rtl"}࠯> r` T@BM ;m + iQ BMM2` #m``BiQ> UU;m + M/ #2 MV

m``BiQV #m``BiQ ࠯> K2`;2 +QKTQmM/ #m``BiQ> U;m + M/ #2 MV#

m``BiQ#

h?Qb2 +QKBM; iQ #m``BiQb 7`QK 7mM+iBQM H T`Q;` KKBM; # +F;`QmM/
K v T`272` iQ mM/2`bi M/ i?2K #v r v Q7 i?2 ǳ`2im`M M/ #BM/Ǵ
7Q`KmH iBQM Q7 KQM /b (3)- TQTmH `Bx2/ #v i?2 ivT2+H bb K2+? MBbK
Q7 H M;m ;2b bm+? b > bF2HHX

6`QK i?Bb T2`bT2+iBp2- i?2 #m``BiQ KQM /Ƕb UHWXUQ Bb Dmbi i?2 b K2
b Bib mMBi ၓX 6HBTTBM; `;mK2Mi Q`/2`- r2 b22 i? i i?2 ELQG QT2`
iBQM- \" ܽ 5# ܽ 5\" ܽ 5#- i` Mb7Q`Kb #m``BiQ `2+BT2 BMiQ QM2 i? i
2tT2+ib iQ `2+2Bp2 Bib BM;`2/B2Mib BM #m``BiQ 7Q`KX h?2 KQM / H
rb BM i?Bb 7Q`KmH iBQM `2 b iBb7B2/ Dmbi BM + b2 QM2 i F2b IOLS ELQG
ԕ iQ #2 5 ԕ ਼ ၙ #X

h?2 5@BK ;2 Q7 i?2 KQ`T?BbK ԕ T2`7Q`Kb ԕ r?BH2 r` TT2/ BM iQ`iBHH
X .2T2M/BM; QM i?2 M im`2 Q7 i?2 KQ`T?BbK- i?Bb K v ` Bb2 bBx2
Bbbm2bX AM i?2 T`2+2/BM; /Bb+mbbBQM- r2 ? p2 bbmK2/ HH #m``BiQb iQ

2 HQ+ HHv bK HHX#

e *QM+HmbBQM M/ _2H i2/ qQ`F

b vQm + M b22- #m``BiQb `2 MQi bQ ? `/ iQ mM/2`bi M/- QM+2 pB2r2/
7`QK i?2 T`QT2` T2`bT2+iBp2 Ĝ M K2Hv- i? i Q7 #bi` +i + i2;Q`v
i?2Q`vX q2 ?QT2 i? i i?Bb HBiiH2 imiQ`B H rBHH 2M+Qm` ;2 KQ`2
`2b2 `+?2`b iQ BM+Q`TQ` i2 #m``BiQ@i?2Q`2iB+ `2bmHib M/
K2i?Q/b BMiQ i?2B` QrM rQ`FX

\"m``BiQ@HBF2 b M/rB+?2b ? p2 2K2`;2/ b2p2` H iBK2b BM/2T2M/2MiHv-

mi r2`2 MQi Tmi QM bQHB/ i?2Q`2iB+ H 7QQiBM; mMiBH i?2B`#

+QMM2+iBQM iQ KQM /b #2+ K2 TT `2Mi BM i?2 2 `Hv RNdyb (j- d)X JQ`2
`2+2MiHv- +QMM2+iBQM iQ i?2 >2;2HB M i +Q- /BbTH v Q7 i?2
@/BK2MbBQM H 2B;?i@2H2K2Mi ;` T?B+ KQMQB/ rBi? 7Bp2 H27i B/2 Hb- ? b

22M rQ`F2/ Qmi #v G rp2`2 (9)X Ai Bb +QMD2+im`2/ i? i r2 F 2[mBp#

H2M+2b 2tBbi iQ Qi?2` r` T@HBF2 bi`m+im`2b- #mi `2b2 `+? BM i?Bb
`2 Bb T`2b2MiHv QM;QBM;X

_272`2M+2b

$R$ \"Q# *Q2+F2X ǳZm MimK SB+im` HBbKǴX AM, *QMi2KTQ` `v
S?vbB+b UkyyNVX m`H, KWWS DU[LY RUJ DEV X

$k$ * i 62`;mbQMX Pp2`Hv ?QM2bi `272`2M+2b, ǳa?QmH/ r2 +Bi2
i?2 +` TTv : @ #Q` T T2` ?2`2\Ǵ m`H, KWWS UHWUDFWLRQZDWFK FRP
RYHUO\ KRQHVW UHIHUHQFHV VKRXOG ZH FLWH WKH FUDSS\ JDERU SDSHU KHUH
X

$j$ M/2`b EQ+FX ǳai`QM; 6mM+iQ`b M/ JQMQB/ H JQM /bǴX AM, `+?Bp
/2` J i?2K iBF kj URNdkV- TTX RRjĜRkyX

$9$ 6X qBHHB K G rp2`2X ǳ.BbTH v Q7 :` T?B+b M/ i?2B` TTHB+
iBQMb- b 1t2K@ THB7B2/ #v @* i2;Q`B2b M/ i?2 >2;2HB M h +QǴX AM,
*S`Q+22/BM;b Q7 i?2 6B`bi AMi2`M iBQM H *QM72`2M+2 QM H;2#` B+
J2i?Q/QHQ;v M/ aQ7ir `2 h2+?MQH@ Q;v*X RN3NX

$8$ a mM/2`b J + G M2X ** i2;Q`B2b 7Q` i?2 qQ`FBM; J i?2K iB+B
M*X b2+QM/ 2/BiBQMX :` /m i2 h2tib BM J i?2K iB+bX aT`BM;2`- RNN3X

$e$ J `F JQHHQvX :` KK ` +`mb /2` bT2M/b v2 `b `2KQpBM;
`2T2 i2/ 2``Q` 9d-yyy iBK2b QM qBFBT2/B X m`H, KWWS ZZZ
WHOHJUDSK FR XN PHQ WKH ILOWHU *UDPPDU FUXVDGHU VSHQGV \HDUV
UHPRYLQJ UHSHDWHG HUURU WLPHV RQ :LNLSHGLD KWPOX

$d$ _Qbb ai`22iX ǳh?2 6Q`K H h?2Q`v Q7 JQM /bǴX AM, CQm`M H Q7
Sm`2 M/ TTHB2/ H;2#` k URNdkV- TTX R9NĜRe3X

$3$ S?BHBT q /H2`X ǳJQM /b 7Q` 6mM+iBQM H S`Q;` KKBM;ǴX AM, */p
M+2/ 6mM+@ iBQM H S`Q;` KKBM;*X G2+im`2 LQi2b BM *QKTmi2` a+B2M+2
Nk8X aT`BM;2`@ o2`H ;- RNN8X

$N$ \"`2Mi uQ`;2vX *#bi` +iBQM- BMimBiBQM- M/ i?2 ǳKQM / imiQ`B
H 7 HH +vǴ*X m`H, KWWSV E\RUJH\ ZRUGSUHVV FRP DEVWUDFWLRQ LQWXLWLRQ
DQG WKH PRQDG WXWRULDO IDOODF\ X

CONFIDENTIAL COMMITTEE MATERIALS
{width="0.9486668853893263in"
height="0.9486668853893263in"}

SIGBOVIK 2015 Paper Review

Paper 7: Burritos for the Hungry Mathematician

A. G.

Rating: 3 (weak accept)

Confidence: 2/4

This paper presents a novel category theoretic understanding of
burritos. This understanding is a major step forward in the eventual
goal of understanding the categorical structure of Fud¨ . The def
inition of the tortilla endofunctor is a significant research
contribution that is a start at illuminating the mysterious structure
of Fud¨ . However, the reviewer is not satisfied with just the
definition of the tortilla endofunctor and believes that either the
author should define the other endofunctors in this category or prove
a uniqueness theorem as to why the tortilla endofunctor is the only
one possible. This reviewer suspects that there may actually be
infinite endofunctors in Fud¨ once one considers, crepes, blini,
wraps, etc -- the whole set of circular two dimensional vessels for
enclosing food. ˆ

7UDFN =

&RPSXWDWLRQDOL]LQJ &RPSXWDWLRQ

$ 1HZ 3DUDGLJP IRU &HUWLILHG &RGH

6WHIDQ 0XOOHU

.H\ZRUGV FHUWLILHG FRGH FHUWLILHG FRPSLOHU SURRI FDUU\LQJ FRGH

%H\RQG WKH +DOWLQJ 3UREOHP +LJKHU 2UGHU ,QILQLWH /RRS &KHFNHUV -RG\
/HRQDUG DQG $DURQ 6DQWLDJR

.H\ZRUGV FRPSXWDELOLW\ GHFLGDELOLW\ LQILQLWH ORRS FKHFNHU

%DVKLQJ +DVNHOO

5HLPSOHPHQWLQJ WKH 3DUVHF /LEUDU\ ,QVLGH WKH 8QL[ 6KHOO 0LNH
,]ELFNL

.H\ZRUGV XQL[ VHG SDUVLQJ SDUVHF KDVNHOO DSSOLFDWLYH PRQDG

A New Paradigm for Certified Code

Stefan Muller

Carnegie Mellon University

smuller@cs.cmu.edu

Abstract

Everyone likes running programs, but before you run a piece

of code, you want to be sure that it's actually code. ~~Utterly~~

~~ignoring~~ building on a large body of work in certified code,

we solve this ever-so-common problem.

1. Introduction

Dozens of prior studies over several years have worked in the

area of "certified code" (e.g. [1--5, 7, 9, 10, 12--14]). Like all

great researchers, the present author didn't read any of these

papers, as such a literature study clouds one's mind with

lesser ideas and stifles true innovation. Instead, this paper

presents an entirely novel way of generating and running

certified code. You're welcome.

In these fast-and-loose days of computing, it is com

mon to assume that a given file is an executable binary, run

chmod +x on it, and execute it willy-nilly. However, doing

this on a non-executable file can severely damage one's com

puter¹. It is thus vital to the security of computers that, prior

to executing a file, we certify that it is, in fact, code (as op

posed to, for example, a humorous animated GIF of a cat).

This is the domain of certified code. In this paper, we de

scribe CODECERT, a new, language-independent method of

generating certified code from source, and running it safely.

2. The CODECERT System

The key observation underlying CODECERT is that exe

cutable binaries are the result of running a compiler on a

piece of source code. This observation, explained in Fig

ure 1, means that, to certify that a file is a binary, and there

fore code, we need only certify that it is the output of a com

piler.

¹ Or gracefully throw an exception and exit, as the case may be.

Figure 1: A binary is the output of a compiler on source

code. If the inputs are not a compiler and source code, no

guarantees are possible.

Permission to make shallow or deep copies of all or part of this work
for personal or

classroom use is granted without fee provided that copies are not made
or distributed

for profit or commercial advantage (because that would just be mean),
that copies bear

this notice and that bears copy this notice.

SIGBOVIK '15, April 1, 2015, Pittsburgh, Pennsylvania, USA.

Copyright c 2015 ACH . . . $1000.00 (or best offer)

Figure 2: The CODECERT system compiles a given source file with a given
compiler and compares the result with a given file. The file is a binary
if and only if the results match.

+------------------------------+---------------------------------------+
| Compilers | Not compilers |
+==============================+=======================================+
| gcc | > ls |
| | > |
| javac | > awk |
| | > |
| ghc | > echo |
| | > |
| ocamlc | > sleep |
| | > |
| gc | > apt-get |
| | > |
| coqc | > emacs |
| | > |
| fbc | > bash |
+------------------------------+---------------------------------------+

Table 1: Comparison of compilers and non-compilers

{width="3.0769991251093614in"
height="1.0186668853893264in"}

Figure 3: In the first instance, CODECERT correctly deter mines that
hello is code. In the second, it correctly deter mines that cat.jpg is
not code.

3. Proof of Correctness

We now formally prove that CODECERT is correct in that running a
certified code package generated by CODECERT will proceed only if the
provided file is indeed code.

Theorem 1. If CODECERT produces a certified code pack age from a
file e, then either e is an executable or running the code package
using CODECERT will produce an error.

Proof. By induction on the length of the filename of e. A
zero-character filename is invalid, so the base case is trivial. If
the length is n, rename e to a name of n − 1 characters. By
induction, this new file, and therefore e, is either an

The simplest way to do this is to keep as proof artifacts the source
code and the compiler, and show that the pur

executable or will produce an error.

4. Implementation

ported binary is actually what is obtained by running the purported
compiler on the purported source. This process is explained in further
detail in Figure 2.

To produce certified code, the CODECERT system takes a purported binary,
along with its source code and the com piler with which it was compiled.
These three files are pack aged together. When the certified binary is
to be run, CODE CERT compiles the packaged source code with the packaged
compiler. If this matches the purported binary, the binary is executed.
Otherwise, the file is determined to not be a binary, and the user is
warned not to execute it.

2.1 Certified Compilers

At this point, the astute reader may observe that the pro cess described
above works only if the compiler provided to CODECERT is actually a
compiler. Otherwise, the "source code" could be, for example, an image
and the "compiler" could be a program that, for example, adds captions
to im ages. This concern led us to conduct novel research in the area of
certified compilers [6, 8], related to certified code. Our method
for certifying that a program is a compiler relies on a second key
observation. This observation was reached after detailed study of a
large number of compilers and non compiler utilities, catalogued in
Table 1. Note that all com pilers in the list end in the letter "c"
while no non-compilers do. The CODECERT code generator takes advantage
of this fact to certify that the provided binary is a compiler before
generating the package.

Our CODECERT package consists of two utilities: mkcode and runcode.
The mkcode utility takes as command-line arguments a source code file,
its compiler, the name of the uncertified binary and the name of the
certified package to output and, as the name suggests, mks a certified
code package. This utility is 12 lines of Bash script code which
certifies the compiler and, if valid, prepares a .tar archive of the
provided files, along with the command line with which to invoke the
compiler².

The second utility, runcode, extracts the files from the archive,
invokves the compiler and uses diff to compare the output with the
provided binary. If they match, the binary is executed. Otherwise, an
error is produced. This utility consists of nine lines of Bash code.
Figure 3 shows two interactions with CODECERT.

5. Related Work

A closely related avenue of research which we hope to soon explore
(read: solve) is proof-carrying code [11]. For exam ple, see
Figure 4.

References

[1] A. W. Appel and A. P. Felty. A semantic model of types and
machine instructions for proof-carrying code.

² This is assumed to be ./\<compiler> -o \<output> \<src>. If the
com piler arguments do not take this form, mkcode will fail gracefully
and output an error. We assume. This hasn't actually been tested.

1 (∗ Suppose sqrt (2) = a/ b where a , b are not both even . 2 ∗ 2b
ˆ 2 = a ˆ 2 , so a ˆ 2 i s even , so a=2n

3 ∗ 2bˆ2 = 4nˆ2

4 ∗ bˆ2 = 2nˆ2

5 ∗ bˆ2 is even , so b is even . Contradiction .

6 ∗)

7

8 let rec fib n =

9 i f n \<= 1 then 1 else ( fib (n − 1) ) + ( fib (n − 2) )

_{Figure 4: This code carries a proof that} *^√*2 is
irrational. It also computes Fibonacci numbers.

In Proceedings of the 27^th ACM SIGPLAN-SIGACT Sym posium on
Principles of Programming Languages, POPL '00, pages 243--253, New
York, NY, USA, 2000. ACM. ISBN 1-58113-125-9. doi:
10.1145/325694.325727. URL http://doi.acm.org/10.1145/325694.325727.

[2] S. Chaki, J. Ivers, P. Lee, K. Wallnau, and N. Zeilberger.
Model-driven construction of certified binaries. In Pro ceedings of
the 10^th International Conference on Model Driven Engineering
Languages and Systems, MOD ELS'07, pages 666--681, Berlin,
Heidelberg, 2007. Springer Verlag. ISBN 3-540-75208-0,
978-3-540-75208-0. URL
http://dl.acm.org/citation.cfm?id=2394101.2394161.

[3] K. Crary and S. Sarkar. Foundational certified code in the twelf
metalogical framework. ACM Trans. Comput. Logic, 9(3):16:1--16:26,
June 2008. ISSN 1529-3785. doi: 10.1145/1352582.1352584. URL
http://doi.acm.org/10.1145/1352582.1352584.

[4] K. Crary and J. C. Vanderwaart. An expressive, scalable type
theory for certified code. In Proceedings of the Seventh ACM SIGPLAN
International Conference on Functional Program ming, ICFP '02, pages
191--205, New York, NY, USA, 2002. ACM. ISBN 1-58113-487-8. doi:
10.1145/581478.581497. URL http://doi.acm.org/10.1145/581478.581497.

[5] N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A
syntactic approach to foundational proof carrying code. In
Proceedings of the 17^th Annual IEEE Symposium on Logic in Computer
Science, LICS '02, pages 89--100, Washington, DC, USA, 2002. IEEE
Computer Society. ISBN 0-7695-1483-9. URL
http://dl.acm.org/citation.cfm?id=645683.664592.

[6] X. Leroy. Formal certification of a compiler back-end or:
Programming a compiler with a proof assistant. In Con ference Record
of the 33^rd ACM SIGPLAN-SIGACT Sympo sium on Principles of Programming
Languages, POPL '06, pages 42--54, New York, NY, USA, 2006. ACM. ISBN
1-59593-027-2. doi: 10.1145/1111037.1111042. URL
http://doi.acm.org/10.1145/1111037.1111042.

[7] T. Lindholm and F. Yellin. Java Virtual Machine Specifica
tion. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA,
2^nd edition, 1999. ISBN 0201432943.

[8] J. S. Moore. A mechanically verified lan guage implementation.
J. Autom. Reason., 5(4): 461--492, Nov. 1989. ISSN 0168-7433. URL
http://dl.acm.org/citation.cfm?id=83471.83477.

[9] G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F.
Smith, D. Walker, S. Weirich, and S. Zdancewic. Talx86: A realistic
typed assembly language. In In Second Workshop on Compiler Support
for System Software, pages 25--35, 1999.

[10] T. Murphy, VII. Ml grid programming with concert. In
Proceedings of the 2006 Workshop on ML, ML '06, pages 2--11, New
York, NY, USA, 2006. ACM. ISBN 1-59593-483-9. doi:
10.1145/1159876.1159879. URL
http://doi.acm.org/10.1145/1159876.1159879.

[11] G. C. Necula. Proof-carrying code. In Proceed ings of the 24^th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL '97, pages 106--119, New York, NY, USA, 1997. ACM. ISBN
0-89791-853-3. doi: 10.1145/263699.263712. URL
http://doi.acm.org/10.1145/263699.263712.

[12] G. C. Necula. Compiling with Proofs. PhD thesis, Carnegie
Mellon University, Pittsburgh, PA, USA, 1998. AAI9918593. [13] Z.
Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for
certified binaries. In Proceedings of the 29^th ACM SIGPLAN-SIGACT
Symposium on Prin ciples of Programming Languages, POPL '02, pages
217--232, New York, NY, USA, 2002. ACM. ISBN 1-58113-450-9. doi:
10.1145/503272.503293. URL

http://doi.acm.org/10.1145/503272.503293. [14] Z. Shao, V. Trifonov,
B. Saha, and N. Papaspyrou. A type system for certified binaries. ACM
Trans. Program. Lang. Syst., 27(1):1--45, Jan. 2005. ISSN 0164-0925.
doi: 10.1145/1053468.1053469. URL
http://doi.acm.org/10.1145/1053468.1053469.

Beyond the Halting Problem

Higher Order Infinite Loop Checkers

Jody Leonard and Aaron Santiago

jleonard11@simons-rock.edu asantiago11@simons-rock.edu

Division of Science, Mathematics and Computing, Bard College at Simon's
Rock

Abstract. The infamous Halting Problem asks whether it is
possible to determine whether an arbitrary program P halts on
arbitrary input x. It is well known that the Halting Problem is
undecidable for all input pairs of P and x - however, this
question nevertheless remains woefully unexplored. In this landmark
paper, we reframe the investigation with a more practical
construction: infinite loop checkers.

Keywords: computability, decidability, in finite, loop, checker.

1 Introduction

In 1936, Alan Turing's delivered his pa per "On Computable Numbers, with
an Application to the Entscheidungsproblem" [3] as a response to the
famous Entschei dungsproblem¹. In essence, Turing showed that for
all programs P and inputs to those programs x, the language

L_H:= {(P, x)|*P halts when run on x},*

also known as the Halting Problem, is not computable on a Turing
Machine. Since the Halting Problem can be reduced to the
Entscheidungsproblem, it follows that the Entscheidungsproblem has no
general so lution.

Our paper does not challenge Turing's conclusions, but rather draws
attention to some important concerns and limitations of Turing's
circumstances:

• Before the 1990s, there was no suffi cient method to test any of
Turing's re sults because programming didn't exist

¹ Elvish for "tree fecal issue". For more infor mation, see [2].

yet. The release of Python and other programming languages have all
but solved this problem.

• Technology now has reached levels of computational power that
would be unfathomable to researchers of Tur ing's time. The clock
speed of Turing Machines are lumps of dirt compared to the chips found
in even the light switches of today.

• Alan Turing was a much too attrac tive man. This meant that his
ability to design theoretically valid statements must have been
impaired by his ability to socialize.

With these limitations in mind, it is im portant to reassess the
foundations of Tur ing's arguments in order to continue com puting as
a whole. Even though no one can know for sure, the authors believe
that without such a change in direction, com puting will be forced to
stop.

To this end, we re-define and oper ationalize the Halting Problem in
terms of a construction we call the infinite loop checker.
Critically, this construction allows us to better consider
extrapolations of the Halting Problem, which we term orders of
infinite loop checkers.

2 Definitions

We begin by establishing a key concept with Definition 1.

Definition 1. A program P verifies pro gram S iff P returns
True when its input is equivalent to S, and False otherwise.

We define an infinite loop checker of or der n to be a program that
verifies a loop checker of order *n−*1. This allows a simple natural
language definition given in Defini tion 2.

Definition 2. An infinite loop checker of order n is the
following:

checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker

"

^{"*inf inite loop checker . . . checker*} n times

checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker

For example, an infinite loop checker of order n = 420 is an infinite
loop checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker checker
checker checker

checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker

checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker checker checker checker checker
checker checker checker checker. This is obviously a very high order.
For conve nience, particularly in dealing with high orders, we adopt
the notation given in Def inition 3.

Definition 3. ILC_n is an infinite loop checker of order n.

The above language-notated infinite loop checker is equivalent to
ILC₄₂₀.

3 The Infinite Loop Checker Checker

The Halting Problem, along with Turing's proof, is widely known.
However, the def initions given in Section 2 prompt us to consider the
case of ILC₂. Lemma 1 offers the first of our foundational results.

Lemma 1. ILC₂ is computable.

To prove Lemma 1, we provide pseu docode for what we believe to be a
poly time algorithm. The approach is described in Algorithm 1.

Algorithm 1 Infinite Loop Checker [Checker]{.underline}

Input: P, a program.

Output: True if P is an infinite loop checker; False otherwise.

return False

A table containing the experimental run times of Algorithm 1 is given in
Table 1².

² Tests were performed on a 2010 Alienware M11x R2 running 32-bit
Ubuntu through an emulated Commodore 64.

From this table, we conclude that Algo _{rithm 1 runs in O} ₁ ,
because the p-values are good enough³. Further, it's clear that
Algorithm 1 runs very quickly, as comput ing all of Table 1 took just
under 70 units of time. A theoretical runtime analysis is pending
construction of a program that can verify the runtime of Algorithm 1.

Table 1: Experimental Results of ILC₂

+-------------------------------------+--------------+----------------+
| Input (Description) Output | | |
| Runtime | | |
+=====================================+==============+================+
| > Bubblesort | False | 6.902 |
| > | | |
| > Quicksort | False | 6.900 |
| > | | |
| > Bogosort | False | 6.899 |
| > | | |
| > Panicsort | False | 6.901 |
| > | | |
| > blank file | False | 6.898 |
| > | | |
| > Checker.tex | False | 6.899 |
| > | | |
| > vista-sp2.iso⁴ | False | 6.897 |
| > | | |
| > hl3.exe | False | 6.902 |
| > | | |
| > The Deep Web | False | 6.903 |
| > | | |
| > song.mp3⁵ | False | 6.899 |
+-------------------------------------+--------------+----------------+

4 High Order Infinite Loop Checkers

In trying to aggressively improve the per formance of our ILC₂
implementations, we attempted to create a program to verify ILC₂,
and found that, like ILC₁, this prob lem is also undecidable.

Lemma 2. ILC₃ is not computable.

For a formal proof of Lemma 2, see the Halting Problem [3].

Further research revealed that increas ing the order again led to
another decid able problem, and that it has, in fact, an
implementation identical to Algorithm 1.

Lemma 3. ILC₄ is computable.

³ Confused readers are encouraged to consult Rumsey[1].

⁴ Acquired legally.

⁵ Available here: http://jabdownsmash.com/ sigbovik2015/song.mp3

Lemmas 1, 2, and 3 lead us to consider Theorem 1.

Theorem 1. If n is of the form n = 2*k, then* ILC_n is
decidable; if n is of the form n = 2*k* + 1*, then* ILC_n is
undecidable.

To test Theorem 1, we created an arbi trary order infinite loop checker
generator, and verified the first few trillion orders of infinite loop
checkers. Pseudocode is given in Algorithm 2, and Table 2 outlines the
fruits of our research up through ILC₅₀. So far, the results of this
test have been consis tent with Theorem 1. We leave the formal proof of
Theorem 1 as an exercise to the reader⁶.

Algorithm 2 Infinite Loop Checker Gen [erator]{.underline}

Input: n, a Natural number.

Output: P, a program that is an implemen tation of ILC_n; False
if not possible.

if n is greater than 0 and even then

return "return False"

else

return False

end if

5 Infinite Order Infinite Loop Checkers

Building on Definition 3, we can begin to approach the concept of
high-order ILC_n programs theoretically. First, we observe a new
approach to Definition 3 in Remark 1

Remark 1. ILC_n for n ≥ 1 is a program that verifies its input to
be ILC_n*−*1.

To cover the case of ILC₁, we provide Definition 4.

Definition 4. ILC₀ is an infinite loop.

⁶ Any completed exercises should be submit ted to
coders@simons-rock.edu for review.

Table 2: Infinite Loop Checkers

+-----------------------+--------------------------+-------------------+
| | ILC Order Decideable? | |
| | Runtime | |
+=======================+==========================+===================+
| > ILC1 | False | N/A |
| > | | |
| > ILC2 | True | _O ₁ |
| > | | |
| > ILC3 | False | N/A |
| > | | |
| > ILC4 | True | _O ₁ |
| > | | |
| > ILC5 | False | N/A |
| > | | |
| > ILC6 | True | _O ₁ |
| > | | |
| > ILC7 | False | N/A |
| > | | |
| > ILC8 | True | _O ₁ |
| > | | |
| > ILC9 | False | N/A |
| > | | |
| > ILC10 | True | _O ₁ |
| > | | |
| > ILC11 | False | N/A |
| > | | |
| > ILC12 | True | _O ₁ |
| > | | |
| > ILC13 | False | N/A |
| > | | |
| > ILC14 | True | _O ₁ |
| > | | |
| > ILC15 | False | N/A |
| > | | |
| > ILC16 | True | _O ₁ |
| > | | |
| > ILC17 | False | N/A |
| > | | |
| > ILC18 | True | _O ₁ |
| > | | |
| > ILC19 | False | N/A |
| > | | |
| > ILC20 | True | _O ₁ |
| > | | |
| > ILC21 | False | N/A |
| > | | |
| > ILC22 | True | _O ₁ |
| > | | |
| > ILC23 | False | N/A |
| > | | |
| > ILC24 | True | _O ₁ |
| > | | |
| > ILC25 | False | N/A |
| > | | |
| > ILC26 | True | _O ₁ |
| > | | |
| > ILC27 | False | N/A |
| > | | |
| > ILC28 | True | _O ₁ |
| > | | |
| > ILC29 | False | N/A |
| > | | |
| > ILC30 | True | _O ₁ |
| > | | |
| > ILC31 | False | N/A |
| > | | |
| > ILC32 | True | _O ₁ |
| > | | |
| > ILC33 | False | N/A |
| > | | |
| > ILC34 | True | _O ₁ |
| > | | |
| > ILC35 | False | N/A |
| > | | |
| > ILC36 | True | _O ₁ |
| > | | |
| > ILC37 | False | N/A |
| > | | |
| > ILC38 | True | _O ₁ |
| > | | |
| > ILC39 | False | N/A |
| > | | |
| > ILC40 | True | _O ₁ |
| > | | |
| > ILC41 | False | N/A |
| > | | |
| > ILC42 | True | _O ₁ |
| > | | |
| > ILC43 | False | N/A |
| > | | |
| > ILC44 | True | _O ₁ |
| > | | |
| > ILC45 | False | N/A |
| > | | |
| > ILC46 | True | _O ₁ |
| > | | |
| > ILC47 | False | N/A |
| > | | |
| > ILC48 | True | _O ₁ |
| > | | |
| > ILC49 | False | N/A |
| > | | |
| > ILC50 | True | _O ₁ |
+-----------------------+--------------------------+-------------------+

Pseudocode for an implementation of

Definition 5.

ILC₀ is provided in Algorithm 3, and is pending runtime analysis.

IOILCC_n

verif ies IOILCC_n*−*1 if n > 0 is ILC*_∞ if n* = 0

Algorithm 3 Infinite Loop

while True do

Nothing.

end while

Now consider ILC*_∞*. Remark 1 states that

ILC*_∞ verif ies* ILC_*∞−*1,

but ∞ − 1 = ∞, which implies that ILC*_∞ verif ies* ILC*_∞*

or simply, that an infinite order infinite loop checker is a program
that verifies it self. Pseudocode for an implementation of an infinite
order infinite loop checker is pro vided in Algorithm 4.

Algorithm 4 Infinite Order Infinite Loop [Checker]{.underline}

Input: P a program.

Output: True if P is equivalent to this pro gram; False
otherwise.

Generate own source code S

if P = S then

return True

else

return False

end if

6 Additional Results and Open Problems

Using the research techniques found in Sec tions 2, 3, and 4, we
consider Definition 5 and suggest Lemmas 4 and 5 as a cursory
exploration of the possibility of infinite or der infinite loop checker
checkers. We offer these Lemmas as open problems.

Lemma 4. IOILCC₁ is not computable. Lemma 5. IOILCC₂ is
computable.

The authors would like to explore the possibility of higher order
infinite order in finite loop checker checkers themselves, how ever
their machines are currently still stuck analyzing the runtime of the
infinite loop algorithm, and it would seem that emulat ing C64
hardware on a five year old laptop is not granting them any favors.

Also, the possibility of exploring check ers in multiple dimensions
might divulge more insight on the nature of Turing's orig inal halting
problem.

{width="2.090333552055993in"
height="1.5886668853893264in"}

Fig. 1: A possible explanation of multi dimensional infinite loop
checkers.

References

1. D. J. Rumsey. Statistics For Dummies. For Dummies, 2^nd edition,
2011.

2. Naomi Saphra. The dumping lemma: As sessing regularity. SIGBOVIK
2014, pages 51--52, April 2014.

3. A. M. Turing. On computable num bers, with an application to the
entschei dungsproblem. Proceedings of the Lon don Mathematical
Society, s2-42(1):230-- 265, 1937.

CONFIDENTIAL COMMITTEE MATERIALS
{width="0.9486668853893263in"
height="0.9486668853893263in"}

SIGBOVIK 2015 Paper Review

Paper 13: Beyond the Halting Problem

Stefan Muller, Carnegie Mellon University

Rating: ∞ (strong strong strong strong strong strong strong strong
strong strong strong Confidence: 4/4

This is a very good paper. Allow me to explain my reasoning. Alan
Turing's famous "On the Computable Numbers, with an Application to the
Entscheidungsproblem" was a good paper, and this paper generalizes its
findings to order ∞, which must make this paper ∞ times better. As
we all know, ∞ × good = ∞, so the goodness of this paper is ∞.

On the other hand, I was slightly confused by Section 6. Judging by
Figure 1 (which was the only part of this section I read), this
section discusses multi-dimensional infinite loop checkers, an amusing
game played by homotopy theorists in which players must reduce their
opponents' loops to points in an infinite, multi-dimensional
non-Euclidean topological space. This is an excellent topic of study,
but I don't see the relevance to the rest of the paper. Unless the
authors have constructed an algorithm to verify programs which
validate possible moves in multi-dimensional infinite loop checkers,
since such a "multi-dimensional infinite loop checkers checker
checker" would be a valuable contribution. In this latter case, the
goodness of the paper is doubled to ∞, otherwise it is decreased
slightly to ∞ − confusing section = ∞.

One request I would make of the authors is to not further discuss the
subject of Alan Turing with me until I finish reading his biography,
as I'm only on Chapter 3 and don't want to be told how it ends.
Judging by his healthy lifestyle and the importance of his scientific
contributions, I can only assume he lived happily to a ripe old age
and was revered by all as the King of Computers.

Bashing Haskell:

Reimplementing the Parsec Library Inside the Unix Shell ~~Functional~~
Imperative Pearl

Mike Izbicki

University of California Riverside

mike@izbicki.me

Abstract

We introduce the Parsed suite of Unix command line tools. Parsed
improves the classic sed program by incorporating ideas from the
popular parsec Haskell library. In particular, the Unix pipe op
^{erator (|) corresponds exactly to the Applicative bind (}_*>)
in Haskell. The resulting syntax is both intuitive and powerful. The
original syntax used by sed can match only regular languages; but our
improved syntax can match any context sensitive language.

Keywords unix, sed, parsing, parsec, Haskell, applicative, monad

1. Introduction

The stream editor (sed) is one of the oldest and most widely used Unix
utilities. Unfortunately, it is a monolithic beast. It fails to live
up to the Unix philosophy of "do one thing well." The problem is that
sed tries to implement all regular expression features in a single
executable. This ruins composibility. For example, let's say I have a
simple sed command for deleting email addresses. Something like:

sed 's/[a-zA-Z0-9.]@[a-zA-Z0-9.]/xxx@xxx/g'

But in the file I'm working on, I only want to delete an email address
if the line starts with the words CONFIDENTIAL. This should not be a
hard task. We should be able to write another sed command for
finding lines that begin with CONFIDENTIAL, then combine these two
commands. But this is not possible using standard techniques. To solve
our problem, we must rewrite an entirely new sed command from scratch.
Within that command, we copy-and-paste our previously tested command:

^{sed 's/(CONFIDENTIAL.}_*)[a-zA-Z0-9.]@[a-zA-Z0-9.]/
$1xxx@xxx/g'

Real world experience suggests that this practice is a leading source
of bugs for the modern sed programmer.¹ In this paper, we simplify
shell based parsing by introducing techniques from functional pro
gramming into the Unix shell. Our Parsed library combines the best of
sed with Haskell's excellent Parsec library.

Parsec is a simple Haskell library that makes parsing easy and fun. It
provides a small set of simple higher order functions called
combinators. By combining these combinators, we can create pro grams
capable of parsing complex grammars. The Parsed library recreates
these combinators within the Unix terminal. In particu lar, each
combinator corresponds to either a shell script or shell function. We
then combine these combinators using the standard Unix pipe. There are
three combinators of particular importance: match, some, and choice.
With these combinators, we can match any regular expression. But
unlike sed, our combinators can

¹ Can you spot the bug in the command?

take advantage of the shell's built-in expressivity to match any con
text sensitive language!

In the remainder of this paper, we give a brief tutorial on how to
construct your own parsers using Parsed. We recommend that you install
Parsed and follow along with our examples. Installing is easy. Just
clone the git repo:

$ git clone https://github.com/mikeizbicki/parsed And add the
resulting parsed/scripts folder to your PATH: $ export
PATH=\"$(pwd)/parsed/scripts:$PATH\" That's it! You're now ready to
start parsing!

2. Matching strings

The most basic combinator is match. It's easiest to see how it works
by example. Throughout this tutorial, we will first present the
examples, and then their explanation.

$ match hello \<\<\< \"goodbye\"

$ echo $?

1

match takes a single command line argument, which is the string our
parser is trying to match. In the above example, this is the string
hello. The text to be parsed comes from stdin. In the above example,
we use bash's built-in \<\<\< syntax, which redirects the contents of
the following string (goodbye) to stdin. The exit code of the
previously run program is stored in the shell variable $?. In the
above example, our parser failed (the string hello does not match the
string goodbye), so $? contains a non-zero value.

Now let's see what a successful parse looks like:

$ match hello \<\<\< \"hello\"

hello

$ echo $?

0

When match succeeds, the matched text gets printed to stderr. This is
where the output string hello comes from in the above example. Since
parsing succeeded, match returned an exit code of 0. As you can see,
match is a very simple parser. It is normally combined with other
parsers.

3. Combining parsers

We combine parsers using the standard unix pipe (|). For example,
let's create a parser that first matches the string hello and then
matches the string world:

$ (match hello | match world) \<\<\< \"helloworld\"
helloworld

$ echo $?

0

Script 1 match

#!/bin/sh

# check for the correct number of arguments if [ -z \"$1\" ]
|| [ ! -z \"$2\" ]; then

echo \"match requires exactly one argument\" exit 255

fi

# When reading from stdin, the shell ignores the contents of the IFS
variable. By default, this is set to whitespace. In order to be able
to read whitespace, we must set IFS to nothing.

IFS=''

# read in exactly as some characters as are in the first command
line argument

read -rn \"${#1}\" in

# if we parse correctly

if [ \"$1\" = \"$in\" ]; then

# print the parsed string to stderr

echo -n \"$in\" 1>&2

# forward the unparsed contents of stdin cat

# signal that parsing succeeded

exit 0

else

# parsing failed

exit 1

fi

Parsing succeeds for both calls to match, so parsing succeeds overall.
To see how piping combines parsers, we need to take a more careful
look at the match script. Like all combinators in the Parsed library,
match is written in POSIX compliant shell. The full source code is
shown in Script 1 above.

We've already seen that when match succeeds, the matched string is
printed to stderr; but additionally, any unparsed text is printed to
stdout. This is demonstrated by the following two tests:

$ match hello \<\<\< \"helloworld\" 1> /dev/null hello

$ match hello \<\<\< \"helloworld\" 2> /dev/null world

As a reminder, by putting a number in front of the output redirection
operator >, we redirect the contents of that file descriptor to the
specified file. File descriptor 1 corresponds to stdout and 2 to
stderr. So the first command above discards stdout; it shows only the
text that was successfully parsed. The second command above discards
stderr; it shows only the text that is sent to any subsequent parsers.

It is possible for the first parser to succeed and the second to fail.
In this case, the succeeding parsers still print their output to
stderr, but parsing fails overall:

$ (match hello | match world) \<\<\< \"hellogoodbye\"
hello

$ echo $?

1

Concatenating two match parsers is relatively uninteresting. We could
have just concatenated the arguments to match! So now let's introduce a
new combinator called eof which matches the end of file. That is, eof
will succeed only if the stdin buffer has been

Script 2 eof

#!/bin/sh

# Try to read a single character into the

variable $next. If next is empty, we're at the end of file, so
parsing succeeds.

IFS=

read -n 1 next

if [ -z $next ]; then exit 0; else exit 1; fi

closed because there is no more input to parse. The source code for
eof is much simpler than for match, and is shown in Script 2. These
next two examples demonstrate the effect of the eof combinator. First,
we try matching the string hello on the input hellohello:

$ match hello \<\<\< \"hellohello\"

hellohello

$ echo $?

0

Parsing succeeds; we print the contents of the parsed text (hello) to
stderr; and we print the remaining content to be parsed (hello) to
stdout. If, however, we apply the eof combinator:

$ (match hello | eof) \<\<\< \"hellohello\"

hello

$ echo $?

1

Parsing now fails because the input was too long. Shortening the input
again causes parsing to succeed:

$ (match hello | eof) \<\<\< \"hello\"

hello

$ echo $?

0

Now that we know how to combine two simple parsers, we're ready for
some more complex parsers.

4. Iterating some parsers

The some combinator lets us apply a parser zero or more times.
^{some corresponds to the Kleene star (}_*) operator used in
sed and most other regular expression tools. some takes a single
command line argument, which is the parser we will be applying zero or
more times. For example:

$ (some \"match hello\" | eof) \<\<\< \"hellohello\"
hellohello

$ echo $?

0

The above example succeeds because the some \"match hello\" parser
consumes both occurrences of hello. As already men tioned, some need
not consume any input:

$ some \"match hello\" \<\<\< \"\"

$ echo $?

0

$ some \"match hello\" \<\<\< \"goodbye\"

$ echo $?

0

In fact, the some used by itself can never fail---it will always just
parse the empty string. In order to force failures, we must
concatenate some with another parser like so:

$ (some \"match hello\" | eof) \<\<\< \"goodbye\" $
echo $?

1

Script 3 some

#!/bin/sh

# check for the correct number of arguments if [ -z \"$1\" ]
|| [ ! -z \"$2\" ]; then

echo \"many requires exactly one argument\" exit 255

fi

# put the contents of stdin into a variable so we can check if it's
empty

stdin=$(cat)

# if we still have input and parsing succeeded if [ ! -z
\"$stdin\" ] && stdout='eval \"$1\" \<\<\< \" $stdin\"';
then

# run this parser again

\"$0\" \"$1\" \<\<\< \"$stdout\"

else

# stop running this parser

cat \<\<\< \"$stdin\"

fi

Unfortunately, the some combinator breaks the ability to use POSIX pipes
for concatenation as we did above. Consider this example:

$ (match hello | some \"match hello\") \<\<\< \"\" $
echo $?

0

Our first match parser failed because there was no input. Then we call
the some parser. There is still no input, so some succeeds. Since some
was the last command to execute, $? contains its exit code which is
0.

The problem is that the standard POSIX $? variable has the wrong
behavior. We need a variable that will report if any of the commands in
the pipe chain failed. There is no POSIX compliant way to do this. But
more modern shells like bash offer a simple fix. The command

$ set -o pipefail

modifies the semantics of the $? variable so that it contains zero only
if all commands in the pipe chain succeed; otherwise, it con tains the
exit code of the first process to exit with non-zero status. This
command need only be run once per bash session. There after, we can
rerun the incorrect example above to get the correct output:

$ (match hello | some \"match hello\") \<\<\< \"\" $
echo $?

1

The code for the some combinator is shown in Script 3 above.

5. Custom combinatorial explosion

Most regular expression libraries offer a primitive combinator + that
matches one or more occurrences of a previous parser. Parsed does not
have such a primitive operator because it is easy to build it using only
the | and some combinators. We call the resulting operator many, and we
implement it by creating a bash function:

$ many() { $1 | some \"$1\"; }

Recall that the $1 variable will contain the first parameter to the
many function. In this case, that parameter must be a parser. We

Script 4 many

#!/bin/bash

set -o pipefail

$1 | some \"$1\"

exit $?

can use our new combinator to simplify the examples from the previous
section:

$ many \"match hello\" \<\<\< \"\"

$ echo $?

1

$ many \"match hello\" \<\<\< \"hello\"

hello

$ echo $?

0

Unfortunately, Bash functions do not last between sessions. If we want
something more permanent, we can create a script file instead. In
fact, the many combinator is so useful that it comes built-in to the
Parsed library. You can find its source code in Script 4 above. When
the script file starts, it will not inherit the settings of its parent
process in the same way that our many function did. Therefore, we must
specifically re-setup our non-POSIX pipes at the beginning of every
script that uses them.

6. The program of choice

The last combintor we need for parsing regular languages is called
choice. The match and many combinators required exactly one input, but
choice takes an arbitrary number of input parameters. Each parameter
is a parser. For each of these parsers, choice applies it to stdin. If
it succeeds, then choice returns success. If it fails, then choice
goes on to the next parameter. If all parsers fail, then choice fails
as well.

Here's a simple example using just the match combinator:

$ choice \"match hello\" \"match hola\" \<\<\< hello hello

$ echo $?

0

$ choice \"match hello\" \"match hola\" \<\<\< hola hola

$ echo $?

0

$ choice \"match hello\" \"match hola\" \<\<\< goodbye $ echo
$?

1

Our parser succeeds when the input was either hello or hola, but fails
on any other input.

7. Free your context

In the intro we claimed that Parsed is strictly more powerful than
sed. We now demonstrate this point by parsing a context free language.
Sed only supports regular expressions. The reason Parsed has this
extra power is because we can define our own recursive parsers using
standard shell syntax.

To demonstrate this capability, we will write a parser that checks for
balanaced parenthesis. First, let's define a small combinator paren
that takes a single parser as an argument and creates a parser that
succeeds only when the parameter is surrounded by parentheses:

$ paren() { match \"(\" | $1 | match \")\"; } And
let's test it:

Script 5 choice

#!/bin/bash

# We need to store the contents of stdin explicitly to a file. When
we call one of our candidate parsers, it will consume some of the
input form stdin. We need to restore that input before calling the
next parser. stdin=$(tempfile)

cat >\"$stdin\"

# If stdin is empty, then we're done with recursion; parsing
succeeded

if [ ! -s \"$stdin\" ]; then

exit 0

fi

# For similar reasons, we'll need to store the output of our
parsers.

stdout=$(tempfile)

stderr=$(tempfile)

# For each parser passed in as a command line arg for cmd in
\"$@\"; do

# Run the parser; if it succeeds, then pass on its results

if $(eval \"$cmd\" \<\"$stdin\" 1>\"$stdout\" 2>\"
$stderr\") ; then

cat \"$stderr\" >&2

cat \"$stdout\"

exit 0

fi

done

# All parsers failed, so we failed

exit 1

$ paren \"match hello\" \<\<\< \"hello\"

$ echo $?

1

$ paren \"match hello\" \<\<\< \"(hello)\"

(hello)

$ echo $?

0

We will use paren to write a combinator maybeparen that ac cepts whether
or not the parameter parser is surrounded by paren thesis. Here is a
reasonable first attempt:

$ maybeparen() { choice \"$1\" \"paren $1\"; }

Unfortunately, this doesn't work due to scoping issues with bash. When
we run our command, we get an error:

$ maybeparen \"match a\" \<\<\< \"(a)\"

choice: line 7: paren: command not found

We get this error because the choice combinator is its own shell script.
When this script gets executed, a new shell process starts with a clean
set of environment variables. In the context of this subprocess, the
paren function we created above doesn't exist.

There are two ways to solve this problem. The simplest is to use the
following bash-specific syntax:

$ export -f paren

This command tells the running bash shell that any subshells it spawns
should also have access to the paren function. Now when we try running
our previous tests:

Script 6 parens

#!/bin/bash

choice \"$1\" \"match '(' | par \\"$1\\" | match ')'\"

$ maybeparen \"match a\" \<\<\< \"a\"

a

$ echo $?

0

$ maybeparen \"match a\" \<\<\< \"(a)\"

$ echo $?

1

We still get a parse error! What's happening is that we actually
defined the maybeparen function incorrectly. Here is the correct
definition:

$ maybeparen() { choice \"$1\" \"paren \\"$1\\"\"; }

The only difference is that the correct definition surrounds our $1
parameter with quotation marks. This ensures that the entire value of
the variable gets passed as a single parameter to the paren
combinator. Because these quotation marks are within quotation marks,
they must be escaped with backslashes. Arrgh!

We are now ready to define a combinator parens that matches any number
of balanced parentheses. In order to avoid the need for a set of
triply nested quotation marks, we will put the parens combinator
within a script file (instead of a function) and we will manually
inline our call to the paren combinator. Script 6 above contains the
final result. And now let's test our creation:

$ par \"match a\" \<\<\< \"(((a)))\"

(((a)))

$ echo $?

0

$ par \"match a\" \<\<\< \"(((b)))\"

$ echo $?

1

$ par \"match a\" \<\<\< \"(((a\"

$ echo $?

1

We've successfully parsed a context free language :)

8. Discussion

This is only a very brief introduction to the capabilities of our
Parsed library. Additional under-documented features include: (1) We
can use shell variables to simulate Haskell's Monad type class. In
particular, the shell code:

var=$(func)

is equivalent to the haskell do-notation code:

var \<- func

In fact, all shell commands can be thought of as being within the IO
monad wrapped within the ParsecT transformer. This leads us to our
next under-documented feature. (2) Arbitrary commands can be used in
parsers. Want to punish your users when they make
^{syntax errors? Just add an rm -rf} _* at the appropriate
place in your combinators.

References

[1] Daan Leijen and Erik Meijer. Parsec: Direct style monadic parser
combinators for the real world. 2002.

7UDFN :

/DVW 3HULRG +RQRUV (QJOLVK &ODVV

3URJUDPPLQJ /DQJXDJH )DQ )LFWLRQ

6WHIDQ 0XOOHU

.H\ZRUGV W\SH ODQJXDJHV SURJUDPPLQJ ILFWLRQ IDQ WKHRU\

$FURQ\P\ $ %LGLUHFWLRQDO \'LFWLRQDU\

\'DYLG 5HQVKDZ

.H\ZRUGV NQRZLQJO\ HOHYDWH \RXU ZULWLQJ RQ UHOHYDQW GLUHFWHG
VHDUFKHV

$QRWKHU $UWLFOH WKDW 0DNHV %LEOLRPHWULF $QDO\VLV D %LW +DUGHU -
3IHIIHU DQG - 3IHIIHU

.H\ZRUGV ELEOLRPHWULFV M SIHIIHU M SIHIIHU

&RPPHQW 6,*%29,. 6KRXOG %DQ &RQFOXVLRQV

-LP 0F&DQQ

.H\ZRUGV EDVS KDVS JUDVS WDVS PDVS ODVS GDVS

7KH 3RUWPDQWRXW

\'U 7RP 0XUSK\ 9,, 3K \'

.H\ZRUGV ODVW PLQXWH WUHDWV OH[LFDO IHDWV EURJUDPPDU