Sigbovik 2022

Click for full version PDF

the association for computational heresy presents

a record of the proceedings of

SIGBOVIK 2022

the sixteenth annual intercalary robot dance party in celebration of
workshop on symposium about 2⁶th birthdays; in particular, that of
harry q. bovik

cover art by someone probably

carnegie mellon university

pittsburgh, pa

april 8, 2022

i

SIGBOVIK

A Record of the Proceedings of SIGBOVIK 2022

ISSN 2155-0166

April 8, 2022

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

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.

ii

SIGBOVIK 2022 {width="1.000485564304462in"
height="1.000485564304462in"}

Message from the Organizing Committee
\Message2020{16}{uenchiest}{$2ˆ6$}

iii

iv

TODO: Tell next year's committee that they should probably avoid

further milking the blindsight joke

Programming Languages 5 1 Modernized Python . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 6 2 Grand Challenges in
Programming Languages Position Paper: What, if any

thing, does multiplication even mean? . . . . . . . . . . . . . . . .

. . . . . . 13 3 A Type-and-Affect System for Semisignificant

Whitespace . . . . . . . . . . 16 4 brainfuck++: a much needed

extension to brainfuck . . . . . . . . . . . . . 23

Other Languages 33 5 Tironiculum: Latin Speech Recognition via Latin
Text-to-Speech . . . . . . 34 6 Abecedarial Acrostic, Alphabetized
Amusingly Because Beings Blissfully

Cause Celebratory Centennials... (Note: Full Title is Longer) . . . .

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

. . . . . . . . . . 41 8 ACTION: A Catchy Title Is all yOu Need! . . .

. . . . . . . . . . . . . . . 42 9 A Deep Learning Approach for Deeply

Inaccurate Wordle Solving . . . . . . 43

Systems 45 10 Edward, edMUnD & Edwin: Line-Based Text Editing for
the 21^st Century 46 11 A Free Computer Vision Lesson for Car
Manufacturers or It is Time to Retire

the Erlk¨onig . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . 52 12 Redundant Coupling . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . 54

Theory 57 13 Destructive Logic . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 58 14 Overlap-Maximal Graph Labelings:
Graph Labelings with Non-Disjoint Ver

tex and Edge Sets (and how they can be used for encryption, poetry,

and breaking mathematics) . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . 62 15 Neo-classical Logic: Une Logique non classique .

. . . . . . . . . . . . . . . 69 16 A Patriotic Analysis of

Programming Paradigms . . . . . . . . . . . . . . . 76 17 On Ruinment:

Ruination Theory and its Consequents . . . . . . . . . . . . 84

Astrophysics 91 18 Method and Tool for Estimating the Mass of the
Black Hole Located in the Office of Immigration, Refugees and
Citizenship Canada Causing a Supermas sive Time Dilation in the Visa
Extension Process . . . . . . . . . . . . . . . 92 19 Black Hole
Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . .
102 20 Schr¨odinger's SAT: Generalizing Quantum Bogosort to Prove P =
NP Under Many-Worlds Quantum Mechanics . . . . . . . . . . . . . . . .
. . . . . . . 109 21 Solving Double Execution of Java's paint() Method
by Counting Down to the Heat Death of the Universe (plus language
compendium) . . . . . . . . . 111

1

Climate Science 139 22 Towards Cloud Computing . . . . . . . . . . .
. . . . . . . . . . . . . . . . 140 23 Ecological Memory Management:
Beyond Garbage Collection . . . . . . . . 144 24
Infrastructure-as-PowerPoint: A No-Code Approach to Cloud
Infrastructure

Management . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . 166 25 On the Possibilities and Challenges of Organic

UAV-Assisted MEC . . . . . 172

A Brief Musical Interlude 177 26 Baby Sharks are More than Sharks .
They are Earworms Sung More than Happy Birthday Perhaps . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 178 27 Everybody Clap Your
Hands: The Cha Cha Slide is Turing Complete . . . . 184 28 Exhaustive
Survey of Rickrolling in Academic Literature . . . . . . . . . . . 189

Best Practices 201 29 Quadruple-Blind Peer Review . . . . . . . . .
. . . . . . . . . . . . . . . . . 202 30 Optimal degeneracy through
OwO based variable names . . . . . . . . . . . 206 31 Multiplication
by repeated addition, with fraction handling. . . . . . . . . . 208 32
Objective Correlation Metrics for Quality of Code Estimation . . . . .
. . . 209

Algorithmic Advances 215 33 Functorial wrappers for high-dimensional
classification algorithms . . . . . . 216 34 (Un)helper functions . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 220 35 A
sometimes-accurate O(1) search algorithm . . . . . . . . . . . . . . .
. . 223

Mathematic Retreats 225 36 Improved Data and Instruction Locality in
Long Division . . . . . . . . . . 226 37 The New New Math: using
sentiment analysis of mathematics word problems

to gauge children's reactions to teaching 8-bit floating point

arithmetic for the new California public school math curriculum . . .

. . . . . . . . . . . . . . 229 38 Infix Modifiers for Flexible

Multiplication . . . . . . . . . . . . . . . . . . . 236

Aesthetics 239 39 Real-Time Foliage Simulation . . . . . . . . . . .
. . . . . . . . . . . . . . . 240 40 Using deep CNNs to prove that I
look better than Tom Cruise and Shah

Rukh Khan combined . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . 241 41 EBMP: Efficient Bitmap Encodings on Ethereum Virtual

Machines . . . . . 243 42 A Machine Learning Approach To Classifying

Cuteness . . . . . . . . . . . 251 43 Attractiveness Learning: A

General Solution for the Cold-Start Problem . . 253

Hardware 257 44 Correct-It-Yourself Paper Updater . . . . . . . . .
. . . . . . . . . . . . . . 258 45 Harder Drive: Hard drives we didn't
want or need . . . . . . . . . . . . . . 259 46 Just a Regular Paper .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 278 47
Wearable RF-shield repositories . . . . . . . . . . . . . . . . . . .
. . . . . . 279

2

Black Boxes 281 48 A 23 MW data centre is all you need . . . . . . .
. . . . . . . . . . . . . . . 282 49 When Pull Comes To Shove... Do
Both! . . . . . . . . . . . . . . . . . . . . 293 50 man exorcism . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 338
51 2x a fake submission . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 340

SIGBOVIK 343 52 Analysis of A New Error Calculation Technique . . .
. . . . . . . . . . . . . 344 53 A Third Thorough Investigation of the
Degree to which the COVID-19 Pan

demic has Enabled Subpar-Quality Papers to Make it into SIGBOVIK, by
Reducing the Supply of Authors Willing to Invest the Necessary Effort
to Produce High-Quality Papers . . . . . . . . . . . . . . . . . . . .
. . . . . . 345 54 this is not a review . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 346

3

4

Programming Languages

1 Modernized Python

Daniel Ng

Keywords:programming languages, type theory, python, sml

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

Jim McCann

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

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

Keywords: whitespace, white space, white nspace

4 brainfuck++: a much needed extension to brainfuck C´edric Ho Thanh

Keywords: Programing langage, brainfuck, concurrency, machine learning

5

1

Abstract

Modernized Python

Daniel Ng

March 25, 2022

The popular Python programming language is generally heralded for its
usability and learn ability. However, this often comes at the cost of
efficiency. Solutions to this problem have emerged over the last few
years to impose static type systems onto Python without intruding on
the underlying syntax. This paper deviates from the norm of building
on the existing language, and instead looks to completely overhaul the
concrete syntax while maintaining its beloved semantics.

Introduction

Python has recently surged in popularity, largely for two reasons.
Firstly, it is an easy language for beginners to learn, especially
because its array of modules allows for relatively complex projects to
be built up relatively quickly. Additionally, these modules are often
used in fields such as artificial intelligence and machine learning as
a reliable and easy-to use language. However, concerns from type
theorists have emerged, largely regarding its inefficiency and
unsafety.

The approach of overlaying a type system onto the existing concrete
syntax is one that has been considered in several places previously.
Type theorists claim that this could speed up the language and allow
for fewer runtime errors. However, this approach has a negative impact
in certain edge cases. Certain scripts may wait for Python programs to
terminate, causing processor cycles to be wasted. Additionally,
speeding up Python gives programmers less time to slack off while
their code is running, the social drawbacks of which are immense.

It is thus only natural to look into ways to make the Python
programming language more palatable for functional programmers.
Current approaches focus on keeping Python's con crete syntax while
overhauling the abstract syntax to better match that of functional lan
guages. In contrast, we try a revolutionary new approach in this paper
and try to improve the concrete syntax make it more palatable for
functional programmers. In the spirit of Harper [1], we therefore
propose a Modernized Python, which seeks to eliminate the issues

6

with Python at the level of concrete syntax, while maintaining both the
speed and mem ory usage of original Python. Any resemblance to real
languages, living or dead, is purely coincidental¹.

Problems

Concrete Syntax

While the concrete syntax of Python seems both easy to learn and easy to
write, its actual nature is really not like that at all. Consider the
behaviour of the following program:

1 def fact ( x ) :

2 if ( x == 0) :

3 return 1

4 return x * fact ( x - 1)

5 print ( fact (10) )

At first glance, this appears to be a perfectly legal² program that
computes the factorial of a given positive number. However, upon
actually attempting to interpret this code, it returns IndentError
rather than printing 3628800. Some might argue that this has to do with
the use of a three-space indent for some awful reason. However, the same
problem exists for users of the much more popular two-space indent. It
follows from these strict indentation requirements that handwritten
Python code on paper³is extremely unlikely to run, much to the dismay
of many exam-takers.

The additional requirement that all lines be terminated with a newline
adds further com plications to the concrete syntax, especially when
trying to write long commands and avoid confusion. The indentation issue
is also exascerbated when determining where a loop ends or begins.
Marking the end of code blocks in general is therefore another concern
that we will attempt to address when modernizing Python.

One feature that must be preserved through this is Python's acceptance
of generally ques tionable code. For example, the following function
would be rejected by most sensible type systems, yet is allowed by
Python:

1 def f (_ ) :

2 return f ( f )

Python will attempt to execute f(3) in vain, eventually reaching a
RecursionError, gener ating thousands of call stack frames in the
process before Python realizes what is going on

¹I promise.

²Except in the state of California, where this code is known to cause
cancer, birth defects, or other reproductive harm. And only in the state
of California.

³Or on whiteboards, cuneiform tablets, The Fence, or any other
non-digital media. 7

and averts the impending memory disaster.⁴ Python's willingness to
try once again leads to run-time errors, but it gets an A⁺ for
effort. This characteristic tenacity is preserved even when fixing the
above problems, at the cost of efficiency.

Statics and Dynamics

We now look to the statics and dynamics of Python to better understand
how it be haves.

Statics:

Γ ` x : PyObject

Everything is a PyObject, so this is just stating the obvious. There
are no further statics, because no other types exist anyway.

Dynamics:

_{x final TypeError final f(x) 7−→ TypeError}(With high
probability)

The first dynamic just states that if we have an established PyObject,
then there is nothing further to be done to it, so we just leave it
alone. Likewise, if we have managed to reach a TypeError, there is
nowhere further we can go, as the program has reached an erroneous
state.

The third rule states that most expressions will result in a
TypeError. This is evidenced by the fact that many PyObjects are
functions, however, the probability that the argument x has the
correct type to be input to f without causing a TypeError is rather
low, since the number of total PyObjects is quite large and the set of
valid inputs S is likely significantly smaller⁵. Rudimentary
calculations show that the probability of a TypeError can exceed 99%,
which sounds like quite a high probability.

We now carry out the time-honoured tradition of proving progress and
preservation. Progress: If Γ ` x : τ , then either x final or x 7−→
x⁰for some x⁰. For this, we need a canonical forms lemma⁶.
Fortunately, we can note that every PyObjectconsists of either no
function applications or at least one function application, so if x :
PyObject then either x = y for some non-function application y or x =
f(z) for appropriate f and z. The first case uses the first dynamic to
conclude that x final. The third rule indicates that f(z) 7−→
TypeError.

⁴For dealing with this, the author recommends downloadmoreram.com.

⁵If there are |S| = k valid inputs, there are also at least
k^kinvalid ones, all functions mapping S to itself. ⁶Or Canadian
Football League.

8

Preservation: If Γ ` x : τ and x 7−→ x<sup>0</sup>, then Γ ` x⁰: τ .
Consider that τ = PyObject since PyObject is the only possible type.
Additionally note that the only possible rule that could produce the
judgement is the third dynamic, which implies that x⁰ = TypeError.
Finally, note Γ ` TypeError : PyObject by the statics.

The rules for Python are therefore not particularly complex. This is
mostly evidenced by the fact that the lines in the middle of the rules
are not particularly long -- more detailed languages tend to use rules
with lines spanning nearly the width of the page. The restrictions
that these simplistic rules create are, according to Harper [1],
what makes Python such a powerful language⁷.

Basic Changes

We begin this section with a snippet of Python code which takes the
digital root of an integer.

1 \"\"\"

2 Find the digital root of the number .

3 \"\"\"

4 def dr ( x ) :

5 res = 0

6 while ( x > 0) :

7 res += x % 10

8 x = x // 10

9 if ( res >= 10) :

10 return dr ( res )

11 return res

We begin with the most important part of the code: the arithmetic
control flow comments. Nesting comments can be somewhat cumbersome,
as trying to comment out the entire func tion can lead to uncommenting
parts of the code. Comments therefore now start and end with (* *)
to create clear start and finish markers for a comment.

To make it apparent that dr is a function and res is a variable, we
can rewrite them with keywords that indicate what they are, while
still not forcing them to take on certain types. We also use braces in
place of indentations to keep code blocks organized as the program
evolves. Finally, we make arithmetic more readable by using words to
describe what is going on.

1 (* Find the digital root of the number . *)

2 fun dr ( x ) {

3 val res = 0

⁷In terms of both computational power and energy usage -- the
technique of using Python scripts as space-heater extensions for
laptops has become increasingly prevalent.

9

4 while ( x > 0) {

5 res += x mod 10

6 x = x div 10

7 }

8 if ( res >= 10) return dr ( res )

9 return res

10 }

At this 'point', the code is not exactly sure what it wants to look
like. Some of the Python has been stripped away from the concrete syntax
while maintaining the same underlying inter preter. We therefore
introduce the following loop construct for a while loop. Notice how this
looks functional since the "mutable state" is hidden away in the
function arguments.

fun while (x , state ) guard body = if guard x

then while ( body (x , state ) )

guard body

else state

Additionally, the braces have been stripped away for clarity reasons,
now that our code is organized again. The if/then/else and let/in/end
constructs replace them when needed to keep code organized.

1 (* Find the digital root of the number . *)

2 fun dr ( x ) = let

3 fun body (a , b ) = ( a div 10 , b + ( a mod 10) ) 4 val res = while
(x , 0) ( fn x = > x > 0) body 5 in

6 if res >= 10 then dr ( res ) else res

7 end

Notice the arrow =>, which looks like an elongated musical accent and
is therefore used to add emphasis to the loop guard. Eliminating
unnecessary whitespace allows us to compress our code further, attaining
the goal of the Single Massive Line (SML)⁸.

1 fun dr x = let fun body (a , b) =( a div 10 , b +( a mod 10) ) val res
= while (x ,0) ( fn x = >x >0) body in if res >=10 then dr res else
res end

Further Changes

Here are some further constructs that can be added to the language to
allow for easier compilation from SML-like constructs to Python, in
order to maintain the same efficiency associated with Python
compilation.

⁸Whitespace-equivalence is not a well-studied topic, likely due to
people attempting to read code. 10

1 filter p L == > [ x for x in L if p ( x ) ]

2 map f L == > [ f ( x ) for x in L ]

3 foldl f acc L == > x = acc

4 for y in L :

5 x = f ( acc , x )

6 return x

The widespread importing of Python modules is closely related to SML's
module system, though some might argue it is in name only. A syntax
similar to that of the SML module system is therefore used in
Modernized Python. However, the conversion of many type checking
failures to run-time errors eliminates the need for signatures, which
are replaced by the user's choice between reading documentation
and trial-and-error.

This error conversion also enables the user to write programs such as:

1 fun f () = if random () > 0.5 then 15 else \" potato \" 2 fun g _
= 3 + ( f () )

The user is therefore able to gamble the stability of a currently
running program by at tempting to use the result of a call to f, for
no apparent reward at all. Use cases for this seem extremely limited
and further research is necessary. At the very least, allowing this
sort of 'compilation' to Python allows well-typed portions of programs
to be tested before the remainder of the program is written in full.

Pedagogy

The following introductory computer science courses at CMU were
surveyed about their opinions on Modernized Python.

• 15-122: Honk honk honk honk honk? (Translation: Does it include
contracts?)

• 15-150: My code speed has gotten slower, but maybe converting it to
CPS will somehow help.

• 15-210: Modernized Python could go pretty quickly on multiple
processors with the right libraries if we put it on Diderot.

• 15-213⁹: Do not SIGBOVIK 213.

• 15-251: Not what we meant when we said to perform a reduction.

15-112 did not need to be surveyed, since they already used Python
before its moderniza tion.

⁹https://www.google.com/search?q=15213

11

Conclusion

By restructuring the concrete syntax, we have therefore managed to
translate code written in a functional style to Python. In doing so,
users are now able to run a subset of SML in a much slower manner.
This thrilling discovery allows us to combine the dynamic
type-checking and general permissibility of Python with SML's tidy
syntax. By taking the opposite approach to the popular literature, we
are therefore able to develop a revolutionary new system which makes
the Python language Slightly More Likeable.

References

[1] Robert Harper. 2016. Practical Foundations for Programming
Languages (2^nd. ed.). Cambridge University Press, USA.

12

2

Grand Challenges in Programming Languages Position Paper:

What, if anything, does multiplication even mean?

Jim McCann

Programming Studies Institute

Cranberry Lemon University

Pittsburgh, PA 15213

ix@tchow.com

Abstract

What, if anything, does multiplication even mean? Current programming
languages

answer the question in quirky and overly specific ways, which -- like
being forced

to wear socks only on your feet -- seems fine until you encounter a
situation

where it does not. In this position paper, I will describe the
ambiguity implicit in

"multiplication," how the scope of defining a proper multiplication is
so broad that it is inconceivable that within any ten lifetimes of
good work it could be solved, and

conclude that -- therefore -- defining a sufficiently flexible
multiplication operator is

pretty much impossible.

1 Introduction

What, if anything, does multiplication even mean? While the definition
of addition is abundantly clear, like Crystal Pepsi; the proper
definition of multiplication is terribly muddy, like Pepsi.
Multiplication has so many possible meanings (Section the next
section) that I cannot begin to imagine a world where programming
languages have a uniform, sensible, interpretation of the operation,
just like I can't begin to imagine golf negative trait § couch the.

Therefore, I claim for the throne of the SIGBOVIK Grand Challenges in
Programming Languages Position Paper Grand Challenges List (Appendix
A) the challenge of defining and implementing a consistent and
flexible multiplication semantics in any modern programming language.

the next section Background

What, if anything, does multiplication even mean? Nobody really knows,
but a lot of people have tried to do something smart anyway and got it
sort of wrong but not wrong enough to really matter, just like you did
when you pretended to understand how to use the salad bar at a
Ponderosa steakhouse.

Just a few options:

1.1 Addition in the Log Domain

Slide rule users may attempt to use the so-called identity:

a ∗ b := exp(log(a) + log(b)) (1)

But any savvy numerical methodist will realize that the exp and log
functions are simply shorthand for a near-infinite amount of
multiplication:

_{exp(x) := 1 +} ^x_{1∗ 1 +}^x_{2∗ 1 +}^x_{3∗ (1 + . . .)}
(2)

Meaning that the "definition" in (1) is clearly circular.

-1^st Annual Symposium on Harry Q. Bovik (SIGBOVIK 2022), Pittsburgh,
PA.

13

1.2 Replication

Some languages decide that multiplying a number by a string should
replicate the string:

>>> 5 * 'x'

'xxxxx'

But this definition is inconsistent, since numbers aren't properly
promoted to strings:

>>> 5 * 5

25

expected: '55555'

and, further, the operator is broken for fractions:

>>> 5.5 * 'x'

TypeError: can't multiply sequence by non-int of type 'float'

expected: 'xxxxxx'

1.3 Linear Algebra

Working in a vector space V over field F exposes one to a wide variety
of multiplications.

By definition, every vector space allows scalar-vector multiplication
∗ : F × V → V. For example, in R³,

a ∗ (b₁, b₂, b₃) := (a ∗ b₁, a ∗ b₂, a ∗ b₃) (3)

But many vector spaces also have an inner product ∗ : V × V → F. In
R³,

(x, y, z) ∗ (s, t, r) := x ∗ s + y ∗ t + z ∗ r (4)

And some vector spaces -- like R³ have a cross product ∗ : V × V →
V,

(a₁, a₂, a₃) ∗ (b₁, b₂, b₃) := ( a₂ ∗ b₃ − a₃ ∗
b₂,

a₃ ∗ b₁ − a₁ ∗ b₃,

$5$

a₁ ∗ b₂ − a₂ ∗ b₁ )

Not to mention the element-wise product ∗ : V × V → V,

(a₁, a₂, a₃) ∗ (b₁, b₂, b₃) := (a₁ ∗ b₁, a₂ ∗ b₂,
a₃ ∗ b₃) (6)

And vector spaces may have an associated space of linear
transformations, which in finite-dimensional vector spaces may be
notated using matrices A ∈ F^m×n that tabulate the action of the
transformation

in some basis:

A =



^_a₁₁ · · · a_1n

^.._.^.._.^...

a_m1 · · · a_mn



^ (7)

Meaning that linear transformations A ∈ F^r×m and B ∈ F^m×ccan be
composed by multiplication ∗ : F^r×m × F^m×c → F^r×c:

A ∗ B := C

where c_{ij :=} X^m k=1

a_ik ∗ b_kj(8)

And, further, these linear transformations can be applied to vectors
with multiplication ∗ :

---

LaTeX Gold Warning: MathBBFree per-document usage limit exceeded;
upgrade to remove this limitation.

---

---

F_~ⁿ~ → F_~^m~:

A ∗ b := c

F^m×n×

where c_{i =}Xⁿ k=1

14

b_iA_ik(9)

Further, it is often useful to be able to compose scalar
multiplication with linear transformations using multiplication ∗ : F
× F^r×c → F^r×c:

a ∗ B := C

where c_ij = a ∗ b_ij(10)

Which is seven different definitions of ∗, all of which depend on
each-other as well as some unstated ∗'s that came along with the
definition of F and the vector field.

1.4 Unary Multiplication

Of course, there is no rule that ∗ must be a binary operator. Some
programming languages, like C++, provide unary ∗ operators which --
like unary + -- appear to do nothing:

int x();

assert(+x == x); //unary addition is identity

assert(*x == x); //unary multiplication is identity

//assert(++x == x); //compile error?!

assert(**x == x); //still the identity

2 Potential Approaches

What, if anything, does multiplication even mean? My editor suggests
that I should provide some approaches to this seemingly insurmountable
problem but, honestly, I just can't think of any possible ideas. I
suppose we could stick with the status quo -- multiplication meaning
something which is right in some circumstances and not right in others
-- but I can't see this quo, well, status-ing.

I think the revolution is coming, like a rising tide, and I'm both
apprehensive and elated by the prospect of what may lie on the other
side, like the things the rising tide casts upon the beach; but I sure
as heck don't want to step in some of the things. So I'll be walking
carefully, and so should you.

3 Conclusions

What, if anything, does multiplication even mean? We may never know,
and perhaps it's for the best that we do not. Like when your parents
come home drunk and confess their love to your dog and you realize as
it's happening that you don't have a dog and it's you who are drunk.
And you just said it all out loud.

Current programming languages seem to want to make the decision for
you, but they certainly don't know best. We are all grown up and they
can't make us go to bed early.

Acknowledgments and Disclosure of Funding

This paper was produced with the help of a fictitious bribe from
several shady treeacters, which are like characters, but also trees.
Ent it just the way!

A The SIGBOVIK Grand Challenges in Programming Languages Position
Paper Grand Challenges List

1. Defining a sensible notion of multiplication in any modern
programming language. 2. Et cetera.

15

3

A Type-and-A ect System for Semisignificant Whitespace

Stefan Muller

Illinois Institute of Technology

if ( p != NULL ) { printf ( \" % d \ n \" , * p ) }

if ( p != NULL )

{

printf ( \" % d \ n \" , * p ) }

Ä ::= int | bool | Ä × Ä | Ä → Ä

[¿]{.underline} ::= ¦ | § | I | | ∅

e ::= n | true | false | fun␣x␣−> e | e␣e | (e, e) | let (x,
␣y) = e in e | let␣x␣ = e␣in e | if e␣then e␣else e

Figure 1: If you're a C programmer, one of these looks beau tiful and
one of them makes you want to vomit.

if ( p != None ):

| ␣e | e␣ | \ne | e\n

Figure 3: The syntax of Pedant

print ( \" p ␣ is ␣ \" + p + \" ␣ and ␣ oh ␣ no ␣ I \'m ␣ getting
␣ close ␣ to ␣ the ␣ end ␣ of ␣ the ␣ line ␣ can ␣ I ␣ put ␣ a ␣
linebreak ␣ here ? ␣ I ␣ don \'t ␣ know \" ) In this paper, we begin
by presenting a type system Pedant

that enforces good coding style with regard to whitespace, drawing

Figure 2: Python syntax terri es me.

ABSTRACT

Whitespace characters are generally ignored by compilers for most
languages. But for something ignored by the compiler, programmers sure
do spend a lot of time arguing about the use of whitespace in programs.
In this paper, we show whitespace some (tough?) love and enforce some of
your favorite pedantic style conventions statically. Oh, you asked if
this is like a linter or something? Not exactly...

1 INTRODUCTION

Most languages (with the notable exception of Whitespace [3]) treat
whitespace characters as insigni cant other than as delim iters
between tokens, and discard them during lexing. That's right,
whitespace characters don't even make it to the parser, that's how
overlooked they are. And yet, whitespace is related to so many of the
features that many programmers and programming instruc tors spend so
much time lecturing and/or arguing about: every programming course,
company, book author, and pedant in gen eral has a style guide for
their preferred language. Many of these style guides give advice on
line length, indentation, when to start a new line before and after
delimiters, and other features directly or indirectly related to
whitespace (newlines, spaces, and, if you're a terrible person, tabs),
as seen in Figure 1. Some provide good advice on creating reasonable
code, others harp on pet peeves, and many are contradictory (e.g.,
[2, 4]). Few languages make these guidelines standard or
enforceable, and some languages even make good style di cult. It is an
irony of programming languages that languages which do not have "signi
cant whitespace" have no way of enforcing good style. Meanwhile,
languages in which whitespace characters are sign cant can enforce
some stylistic conventions (e.g., indentation in Python), but the very
fact that whitespace is signi cant makes it di cult to achieve other
elements of good style (who knows when you can break a long line in a
Python program without wreaking havoc?, Figure 2).

SIGBOVIK 2022,

2022.

16

on the best of the signi cant and insigni cant whitespace worlds. In a
normal paper introduction, we would now go on to describe how we do
this and the results we achieve, but as a result, most academic papers
are very uniform as to narrative style. It would be like if every
novel took the approach of beginning the rst chapter with the
protagonists re ecting back on the events that are to be described in
the novel. This can be a good storytelling technique, but it doesn't
work well if overused. Instead, I'll start with a more traditional
narrative style that builds a higher degree of suspense. And so we set
o on this adventure together.

2 PEDANT: A SYNTAX AND TYPE SYSTEM FOR ENFORCING PEDANTIC STYLE RULES
In this section, we begin to develop Pedant, a language equipped with
a type system to enforce the pedantic style rules we discussed in the
introduction. Figure 3 gives the syntax of Pedant, an ML style
calculus extended with visible whitespace (␣, \n). The calculus
consists of integers, Booleans, lambdas, pairs, and the relevant
elimination forms (including let-binding for pairs). The typing
judgment for Pedant is Γ ¢ e : _mÄ^{[¿]{.underline}}_n, meaning that
under variable context Γ, the expression e has type Ä , starts with m
columns of whitespace, and is at most n columns wide. The type also
includes a description [¿]{.underline} of e's newlines, which can be ¦
("top", starts with a newline), § ("bottom", ends with a newline), I
("both", starts and ends with a newline), ("internal", does not start
or end with a newline but is not all on one line), and ∅ ("none", is
all on one line).

Figure 4 gives the typing rules for Pedant. The variable rule T Var
looks x up in the context and types x with the given type. Its width
is |x |, the number of characters in the variable name. We assume
variable names do not contain whitespace, so the left is 0 and the
newline description is ∅. The introduction rules for integers and
booleans are straightforward as well. The remaining rules are standard
as far as the introduction and elimination of types Ä goes, but the
whitespace-relevant parts of the rules are somewhat¹ nonstandard,
and so we'll describe them very brie y before going way too quickly on
to the next section of the paper. As an example, there are three rules
for "if". Rule bool-E1 assumes that

¹I'm hoping there will be an award for "biggest understatement" this
year

SIGBOVIK 2022, Stefan Muller

Γ, x : Ä ¢ x :₀Ä^∅_{|x |}^(Var)Γ ¢ n
:₀int^∅|_{n |}^(int-I)Γ ¢ true :₀bool^∅₄^(bool-I1)Γ ¢
false :₀bool^∅₅(bool-I2) Γ ¢ fun␣x␣−> e :₀Ä₁ →
Ä₂^∅_{4+|x |+4+m+n(→-I1)}Γ, x : Ä₁ ¢ e :
_{[m+1]{.underline}}Ä₂^¦[n]{.underline}

Γ, x : Ä₁ ¢ e : _{[m+1]{.underline}}Ä₂^∅[n]{.underline}

Γ ¢ e₁ : _mÄ₁ → Ä₂^∅_nΓ ¢ e₂ :_jÄ₁^∅k

Γ ¢ fun␣x␣−> e :₀Ä₁ → Ä_{2 max(m+1+n,4+|x |+4)}(→-I2)

Γ ¢ e₁␣e₂ : _mÄ₂^∅_{n+1+j+k(→-E1)}Γ ¢ e₁ :
_{[m]{.underline}}Ä₁ → Ä₂^§_{[n+1]{.underline}}Γ ¢ e₂ :
_{[m+1]{.underline}}Ä₁ [n]{.underline}

Γ ¢ e₁␣e₂ : _mÄ_{2 n+1}(→-E2)

Γ ¢ e₁ : _mÄ₁^∅_nΓ ¢ e₂ :_jÄ₂^∅k

Γ ¢ e₁ : _{[m]{.underline}}Ä₁ → Ä_{2lΦ [n+1]{.underline}}Γ ¢ e₂ :
_{[m+1]{.underline}}Ä₁^¦[n]{.underline} Γ ¢ e₁␣e₂ : _mÄ_2
n+1(→-E3)

Γ ¢ e₁ : _mÄ₁ × Ä₂^∅_nΓ, x : Ä₁,y : Ä₂ ¢ e₂ :_j+1Ä^′∅k

Γ ¢ (e₁, e₂)₀Ä₁ × Ä₂^∅_m+n+j+k+3:^(×-I1)Γ ¢ e₁ :
_{[m]{.underline}}Ä_{1 [n]{.underline}}Γ ¢ e₂ :
_{[m+1]{.underline}}Ä₂^¦[n]{.underline}

Γ ¢ true :₀Ä₁ × Ä_{2 m+n+1}(×-I2)

Γ ¢ e₁ : _mÄ₁ × Ä₂^∅_nΓ, x : Ä₁,y : Ä₂ ¢ e₂ :_j+1Ä^′Ik

Γ ¢ let (x, ␣y) = e₁ in e₂
:₀Ä^′∅_{5+|x |+2+|y |+3+m+n+3+j+1+k}(×-E1)

Γ ¢ e₁ : _{[m+1]{.underline}}Ä₁ × Ä₂^I_{[n]{.underline}}Γ, x :
Ä₁,y : Ä₂ ¢ e₂ : _{[m+1]{.underline}}Ä^′I[n]{.underline} Γ ¢ let
(x, ␣y) = e₁ in e₂ :₀Ä^′
_{max(5+|x |+2+|y |+3,m+1+n)}(×-E3)

Γ ¢ e₁ : _m+1bool^∅_nΓ ¢ e₂ :_j+1Ä^I_kΓ ¢ e₃ :_j+1Ä^¦k

Γ ¢ let (x, ␣y) = e₁ in e₂ :₀Ä^′
_{max(5+|x |+2+|y |+3+m+n+3,j+1+k)}(×-E2)

Γ ¢ e₁ : _m+1bool^∅_nΓ ¢ e₂ :_j+1Ä^∅_kΓ ¢ e₃ :_i+1Ä^∅l Γ
¢ if e₁␣then e₂␣else e₃
:₀Ä^∅_{2+m+1+n+5+j+1+k+5+i+1+l}(bool-E1)

Γ ¢ if e₁␣then e₂␣else e₃ :_{0Ä max(2+m+1+n,j+1+k)(bool-E2)}Γ ¢
e₁ : _{[m+1]{.underline}}bool^I_{[n]{.underline}}Γ ¢ e₂ :
_{[m+1]{.underline}}Ä^I_{[n]{.underline}}Γ ¢ e₃ :
_{[m+1]{.underline}}Ä^¦[n]{.underline} Γ ¢ if e₁␣then e₂␣else e₃
:_{0Ä max(4,m+1+n)}(bool-E3)

Γ ¢ e₁ : _mÄ₁^∅_nΓ, x : Ä₁ ¢ e₂ :_j+1Ä₂^∅k

Γ ¢ let␣x␣ = e₁␣in e₂ :₀Ä^′∅_{4+|x |+2+m+n+3+j+1+k}(Let1) Γ ¢
e₁ : _{[m+1]{.underline}}Ä₁^I_{[n]{.underline}}Γ, x : Ä₁ ¢ e₂ :
_{[m+1]{.underline}}Ä₂^I[n]{.underline}

Γ ¢ let␣x␣ = e₁␣in e₂ :₀Ä^′ _{max(4+|x |+2,m+1+n)(Let3)}Γ ¢ e :
_{[m]{.underline}}Ä^∅[n]{.underline}

Γ ¢ e₁ : _mÄ₁^∅_nΓ, x : Ä₁ ¢ e₂ :_j+1Ä₂^Ik

Γ ¢ let␣x␣ = e₁␣in e₂ :₀Ä^′ _{max(4+|x |+2+m+n+3,j+1+k)}(Let2)

Γ ¢ ␣e : _m+1Ä^∅_n(Space1)Γ ¢ e :
_{[m]{.underline}}Ä^∅[n]{.underline}

Γ ¢ e␣ : _mÄ^∅_n+1(Space2)Γ ¢ e : _{[m]{.underline}Ä
[n]{.underline}}

Γ ¢ \ne : _mÄ_~^¦~n(Newline1)

Γ ¢ e : _{[m]{.underline}}Ä^§[n]{.underline}

Γ ¢ \ne : _mÄ^I_n(Newline2)Γ ¢ e : _{[m]{.underline}Ä
[n]{.underline}} Γ ¢ e\n : _mÄ_~^§~n(Newline3)

Γ ¢ e : _{[m]{.underline}}Ä^¦[n]{.underline}

Γ ¢ e\n : _mÄ^I_n(Newline2)

Γ ¢ e : _mÄ^{[¿]{.underline}}n_{[1]{.underline}}n₁ f n₂ Γ ¢ e :
_mÄ_{~^{[¿]{.underline}}n}2~(Sub1)

Γ ¢ e : _{[m]{.underline}}Ä^∅[n]{.underline}

Γ ¢ e : _{mÄ n}(Sub2)

Figure 4: Statics of Pedant

none of the three subexpressions contain newlines, and therefore the
entire if statement appears on one line:

if b then f () else g ()

All three subexpressions must begin with at least one space, in order to
separate the expression from the preceding keyword. This is enforced
with the +1 on the left component of the type of each subexpression.
Rule bool-E2 assumes that the condition has no newlines, but requires
the "then" branch to have starting and ending newlines and the "else"
branch to have a top newline.

As before, all subexpressions must begin with whitespace. Now,
however, this results in requiring at least one space of indentation
for the two branches, as both are required to begin with a newline.

if b then

f ()

else

g ()

Finally, rule bool-E3 additionally assumes that the condition has
starting and ending newlines.

17

A Type-and-A ect System for Semisignificant Whitespace SIGBOVIK 2022,

if b then f () else g ()

if b then f ()

else g ()

if

b then

f ()

else g ()

let c = \" SIGBOVIK ␣ 2022 \" in

let how = \" really ␣ really ␣ really ␣ \" in let what = \" bad
␣ idea \" in

\" This ␣ \" ^ c ^ \" ␣ paper ␣ is ␣ a ␣ \" ^ how ^ what

Figure 5: Badly formatted expressions that can't typecheck in Pedant.

if

b

then

f ()

else

g ()

Note that because these are the only three typing rules for "if", none
of the abominations in Figure 5 can typecheck. In all cases, the left
column of the if expression is 0, because the expression does not start
with whitespace. The width is calculated appropriately from the widths
of the subexpressions and keywords. For multiline expressions, we take
the maximum width. Note that in bool-E2, for example, both branches are
assigned the same width. To make this work, we allow for a form of
subtyping (Sub1) which we call width subtyping, a name so well-suited to
this concept that I won't bother Googling for whether or not it's
already used for a di erent concept. This allows a narrower expression
to be assigned a wider type for the purposes of taking the maximum width
of several subexpressions. We also allow for another form of subtyping
on line breaks (Sub2) in which "none" is considered a subtype of
"internal". For this, we will use the similarly well-suited term depth
subtyping.

At this point in a type systems paper, we would normally de ne a dynamic
semantics for the language, prove progress and preser vation and declare
success. The astute reader may notice, however, that the type system we
have de ned fails at even the most basic aspects of being a type system.
In fact, not only would preservation be false for any reasonable dynamic
semantics, but we can't even prove a reasonable substitution lemma:

x : int ¢ x :₀int^∅1

[42/x]x = 42

· ¢ 42 : ₀int^∅2

At this point, we have several options:

$1$ We could admit that this whole idea is a farce and these are
entirely syntactic properties that we have no business trying to enforce
semantically, and scrap this idea altogether.

$2$ We could quietly admit the above but recognize that this whole
conference is a farce and decide that it doesn't matter. (3) We could
double down and go to even more ridiculous lengths to try to make this
idea at least seem reasonable.

For maximum comedic e ect, we will, of course, proceed with Option 3.

let how = \" really ␣ really ␣ really ␣ \" in

let what = \" bad ␣ idea \" in

\" This ␣ \" ^ \" SIGBOVIK ␣ 2022 \" ^ \" ␣ paper ␣ is ␣ a ␣ \" ^ how
^ what

let what = \" bad ␣ idea \" in

\" This ␣ \" ^ \" SIGBOVIK ␣ 2022 \" ^ \" ␣ paper ␣ is ␣ a ␣ \" ^ \"
really ␣ really ␣ really ␣ \" ^ ...

Figure 6: A single-step execution of an OCaml expression.

3 THE LANGUAGE PRETTYPRINT

Before attempting to make the ideas of the previous section kinda sorta
work, we need a imsy justi cation for doing so. Most func tional
languages are presented with an operational semantics that involves
transforming expressions (e.g. applying substitutions, re ducing "if"
statements when the condition is evaluated), as opposed to imperative
languages, which are generally presented as static code with a program
counter that captures the runtime control ow. This poses a problem for
debuggers for functional languages: while debuggers for imperative
languages can easily show the line of source code corresponding to the
point of execution and dis play the values of variables, debuggers for
functional languages are generally not able to do something immediately
analogous. Part of the problem is that functional languages are
generally not actually evaluated in a way that closely resembles the
abstract operational semantics presentation: they are either changed
heavily during compilation or interpreted using more e cient techniques.
How ever, one could imagine building an educational debugger for a
functional language that allows novice functional programmers to
single-step programs in a way that follows the formal operational
semantics they learned for the language. This then presents the problem
of displaying the program at any point during execution. One option
would be to maintain the AST of the program as it is transformed by
execution, and pretty-print it when needed. How ever, this would obscure
many of the transformations. Statements that had been spread across many
lines might now be condensed into one or vice versa, and it would be di
cult for novices to follow how the code moves across the screen. It
would be preferable for this contrived example if the line breaks in the
original code were maintained, so the steps were clear. But then, with
no restrictions on input programs, it would be possible for some of
these interme diate expressions to be too wide to properly display.
Consider the example in Figure 6.

This imsy justi cation gives us a new, and actually less ridicu lous,
interpretation for the types of expressions: the type should describe
the maximum width that an expression will have during execution, rather
than simply the width of the source expression. This now begins to more
closely resemble an e ect or type-and-e ect system. As with most e ect
systems, this requires us to annotate more types. For example, it is now
no longer su cient to describe a function type by its input and output
base types, its left column and its width. E ect systems for
call-by-value languages would

18

SIGBOVIK 2022, Stefan Muller

a ect

verb tr.

$1$ (of things) to tend toward habitually or naturally. (2) to assume
arti cially, pretentiously, or for e ect:

Lemma 2. If Γ ¢ e : _mÄ^{[¿]{.underline}}_nthen Γ ¢ strip(e) : _mÄ
n. If Γ ¢ e : _mÄ^∅n then Γ ¢ strip(e) : _mÄ^∅_n.

Lemma 3 (Substitution). If Γ,v : Ä₁[¿]{.underline} ₁

_k¢ e : _mÄ₂[¿ ₂]{.underline}

to a ect a Southern accent.

_{k, then Γ ¢ e[strip(}^←−v )/x] : _mÄ₂[¿ ₂]{.underline}

_nand Γ ¢ v :

_jÄ₁[¿]{.underline} ₁

_n.

Figure 7: De nitions of a ect, paraphrased from Dictio nary.com [1]

generally annotate the function type (or possibly the return type,
depending on the desired notation) with the e ects that might occur
during execution of the function. We could similarly annotate the
return type of a function with a left, width and newline description,
indicating the behavior of the function as it executes. However, this
will depend on the width and line breaks of the substituted arguments.
Consider the following function:

fun x -> \" Is ␣ this ␣ too ␣ long ? ␣ It ␣ depends ␣ on ␣ \" ^
x

Finally, we can state and not attempt to prove type safety. Theorem 1
(Preservation). If • ¢ e : _mÄ^{[¿]{.underline}}_nand e 7→ e^′then •
¢ e^′: _mÄ^{[¿]{.underline}}_n.

Of course, the canonical forms lemma now becomes interesting because
irreducible values may have leading or trailing whitespace.

Lemma 4 (Canonical Forms).

$1$ If • ¢ v : _mint^{[¿]{.underline}}_n, then strip(v) = n
for some n.

$2$ If • ¢ v : _mbool^{[¿]{.underline}}_n, then strip(v) = true
or strip(v) = false. (3) If • ¢ v : _mÄ₁ →
Ä₂^{[¿]{.underline}}_n, then strip(v) = fun x −> e.

_n× _jÄ₂[¿ ₂]{.underline}

[¿]{.underline}

So we must also annotate the domains of functions with their

$4$ If • ¢ v :_{l m}Ä₁[¿]{.underline} ₁

k

_wthen strip(v) = (v₁,v₂).

width and line breaks (it will turn out not to be necessary to anno tate
the left of domains because of how we design the dynamics). This is not
generally the case in e ect systems for call-by-value languages because
passed arguments will be values, which will by de nition have no e ects.
We observe, however that the width of an expression is not really an e
ect, but rather an innate property of the expression which we must
consider for both values and non-value expressions. Because of this, we
refer to our novel construction as a type-and-a ect system (see Figure
7).

In keeping with our new motivation, we will call this language
PrettyPrint. The revised statics appear in Figure 8. For the most
part, the rules are similar to those for Pedant. In addition to an
notating the types of codomains and domains of functions (and the
components of product types), we now annotate variables in the context
with their width and newlines. The variable rule then assigns a
variable x the maximum of |x | and the width from the context. The
function application rules ensure that function argu ments match the
function's expected width and newlines, with the caveat that because
of depth subtyping, arguments with no line breaks, i.e., arguments
written in one row of text, can be passed to functions expecting
multi-row "internal" arguments, allowing us a form of row polymorphism
(again, no Googling necessary).

Finally, we present the dynamics of PrettyPrint in Figure 9.
_{The dynamics depend on two auxiliary de nitions, strip(e) and}
^←−e , de ned in Figure 10. The function strip(e) strips leading and
trailing whitespace from an expression. The function ^←−e removes
indenta tion from e. It is de ned in terms of Indentation(e), which
calculates the indentation level of e. We remove indentation and
trailing and leading whitespace before performing substitution. We must
also look past whitespace to perform reductions. Otherwise, the seman
tics are standard.

We will now state, without any attempt at proof, several facts about
the correctness of these operations that are probably at least close
to true.

Lemma 1. If Γ ¢ e : _mÄ^{[¿]{.underline}}_{nthen Γ ¢} ^←−e
:₀Ä^{[¿]{.underline}}_{n−Indentation(e)}.

Theorem 2 (Progress). If • ¢ e : _mÄ^{[¿]{.underline}}_nthen e is a
value or there exists e^′such that e 7→ e^′.

4 IMPLEMENTATION

Yes, you read that section header correctly. This paper is not a joke.
Well, it is. But it's a joke to which the author is deeply, deeply
committed for reasons that are not clear in the slightest. So yeah, we
implemented a mostly²-working parser, type checker and single step
interpreter for PrettyPrint.

Type inference is about as awful as you'd expect. The type sys tem is
too weird for standard uni cation algorithms, so instead, the
implementation traverses the program and generates a set of con
straints on the width, left and newline behavior of each expression.
At the end, a constraint is added restricting the overall width of the
expression to be, of course, 80. We then solve these constraints using
Z3 [5]. Note that the constraints on the width and left form an
integer linear program (ILP). We leave it to future work to de termine
whether arbitrary ILPs can be encoded as PrettyPrint programs, making
typechecking NP-complete.

After the program is rejected, revised, rejected again, and revised a
few more times, and nally typechecked, the completed program is
displayed and the user given the option to step the program one step
at a time or to completion, as shown in Figure 11. This paper has
already gone on too long, so rather than further bore you with details
of the implementation, we'll give a few observations about our
experience doing the implementation in a nice, easy-to-digest list:

• As the name of the language suggests, pretty-printing, which,
frankly, I've always found to be the most di cult part of language
implementation, is now trivial.

• Lexing, typically the most trivial part of language implemen tation,
is now even more trivial as you don't even need to gure out how to
skip over whitespace.

²well, somewhat

19

A Type-and-A ect System for Semisignificant Whitespace SIGBOVIK 2022,

Γ, x : Ä_{~^{[¿]{.underline}}}n~¢ x
:₀Ä^{[¿]{.underline}}_{max(n, |x |)}^(Var)Γ ¢ ~~n
:₀int^∅|_{n |}^(int-I)Γ ¢ true :₀bool^∅₄^(bool-I1)Γ ¢
false :₀bool^∅₅(bool-I2) Γ ¢ fun␣x␣−> e :₀Ä₁ →
Ä₂^∅_{4+|x |+4+m+n(→-I1)}Γ, x : Ä₁ ¢ e :
_{[m+1]{.underline}}Ä₂^¦[n]{.underline}

Γ, x : Ä₁ ¢ e : _{[m+1]{.underline}}Ä₂^∅[n]{.underline}

Γ ¢ e₁ : _mÄ₁^∅_k → Ä₂^∅_nΓ ¢ e₂ :_jÄ₁^∅k

Γ ¢ fun␣x␣−> e :₀Ä₁ → Ä_{2 max(m+1+n,4+|x |+4)}(→-I2)

Γ ¢ e₁␣e₂ : _mÄ_{2^{[¿]{.underline}}n+1+j+k(→-E1)}Γ ¢ e₁ :
_{[m]{.underline}}Ä_{1 [n]{.underline}} → Ä₂^§_{[n+1]{.underline}}Γ
¢ e₂ : _{[m+1]{.underline}}Ä₁ [n]{.underline}

Γ ¢ e₁␣e₂ : _mÄ_{2 n+1}(→-E2)

Γ ¢ e₁ : _mÄ₁^∅_nΓ ¢ e₂ :_jÄ₂^∅k

Γ ¢ e₁ : _{[m]{.underline}}Ä_{1 [n]{.underline}} → Ä_{2
[n+1]{.underline}}Γ ¢ e₂ : _{[m+1]{.underline}}Ä₁^¦[n]{.underline}
Γ ¢ e₁␣e₂ : _mÄ_{2 n+1}(→-E3)

Γ ¢ (e₁, e₂) :₀Ä₁ × Ä₂^∅_{m+n+j+k+3(×-I1)}Γ ¢ e₁ :
_{[m]{.underline}}Ä_{1 [n]{.underline}}Γ ¢ e₂ :
_{[m+1]{.underline}}Ä₂^¦[n]{.underline} Γ ¢ (e₁, e₂) :₀Ä₁ ×
Ä_{2 m+n+1}(×-I2)

Γ ¢ e₁ : _m

Ä₁[¿]{.underline} ₁

w₁× Ä₂[¿ ₂]{.underline} w₂

_∅

_nΓ, x : Ä₁[¿]{.underline} ₁

w₁,y : Ä₂[¿ ₂]{.underline}

w₂¢ e₂ :_j+1Ä^′∅k

Γ ¢ let (x, ␣y) = e₁ in e₂
:₀Ä^′∅_{5+|x |+2+|y |+3+m+n+3+j+1+k}(×-E1)

w₁× Ä₂[¿ ₂]{.underline}

_∅

w₁,y : Ä₂[¿ ₂]{.underline}

Γ ¢ e₁ : _m

Ä₁[¿]{.underline} ₁

w₂

_nΓ, x : Ä₁[¿]{.underline} ₁

w₂¢ e₂ :_j+1Ä^′Ik

Γ ¢ let (x, ␣y) = e₁ in e₂ :₀Ä^′
_{max(5+|x |+2+|y |+3+m+n+3,j+1+k)}(×-E2)

Ä₁[¿]{.underline} ₁

w₁× Ä₂[¿ ₂]{.underline}

_I

w₁,y : Ä₂[¿ ₂]{.underline}

Γ ¢ e₁ : _m+1

w₂

_nΓ, x : Ä₁[¿]{.underline} ₁

w₂¢ e₂ : _m+1Ä^′In

Γ ¢ let (x, ␣y) = e₁ in e₂ :₀Ä^′
_{max(5+|x |+2+|y |+3,m+1+n)}(×-E3)

Γ ¢ e₁ : _m+1bool^∅_nΓ ¢ e₂ :_j+1Ä^∅_kΓ ¢ e₃ :_i+1Ä^∅l Γ ¢
if e₁␣then e₂␣else e₃ :₀Ä^∅_{2+m+1+n+5+j+1+k+5+i+1+l}(bool-E1)

Γ ¢ e₁ : _{[m+1]{.underline}}bool^I_{[n]{.underline}}Γ ¢ e₂ :
_{[m+1]{.underline}}Ä^I_{[n]{.underline}}Γ ¢ e₃ :
_{[m+1]{.underline}Ä [n]{.underline}} Γ ¢ if e₁␣then e₂␣else e₃
:_{0Ä max(4,m+1+n)}(bool-E3)

Γ ¢ e₁ : _mÄ₁^∅_nΓ, x : Ä₁^∅_n¢ e₂ :_j+1Ä₂^Ik

Γ ¢ e₁ : _m+1bool^∅_nΓ ¢ e₂ :_j+1Ä^I_kΓ ¢ e₃ :_j+1Ä^¦k Γ
¢ if e₁␣then e₂␣else e₃ :_{0Ä max(2+m+1+n,j+1+k)}(bool-E2)

Γ ¢ e₁ : _mÄ₁^∅_nΓ, x : Ä₁^∅_n¢ e₂ :_j+1Ä₂^∅k

Γ ¢ let␣x␣ = e₁␣in e₂ :₀Ä^′∅_{4+|x |+2+m+n+3+j+1+k}(Let1)

Γ ¢ let␣x␣ = e₁␣in e₂ :₀Ä^′
_{max(4+|x |+2+m+n+3,j+1+k)(Let2)}Γ ¢ e₁ :
_{[m+1]{.underline}}Ä₁^I_{[n]{.underline}}Γ, x :
Ä₁^I_{[n]{.underline}}¢ e₂ :
_{[m+1]{.underline}}Ä₂^I[n]{.underline}

Γ ¢ let␣x␣ = e₁␣in e₂ :₀Ä^′ _{max(4+|x |+2,m+1+n)}(Let3)

Γ ¢ e : _{[m]{.underline}}Ä^∅[n]{.underline}

Γ ¢ ␣e : _m+1Ä^∅_n(Space1)Γ ¢ e :
_{[m]{.underline}}Ä^∅[n]{.underline}

Γ ¢ e␣ : _mÄ^∅_n+1(Space2)Γ ¢ e : _{[m]{.underline}Ä
[n]{.underline}}

Γ ¢ \ne : _mÄ_~^¦~n(Newline1)

Γ ¢ e : _{[m]{.underline}}Ä^§[n]{.underline}

Γ ¢ \ne : _mÄ^I_n(Newline2)

Γ ¢ e : _{[m]{.underline}Ä [n]{.underline}}

Γ ¢ e\n : _mÄ_~^§~n(Newline3)

Γ ¢ e : _{[m]{.underline}}Ä^¦[n]{.underline}

Γ ¢ e\n : _mÄ^I_n(Newline2)

Γ ¢ e : _mÄ^{[¿]{.underline}}n_{[1]{.underline}}n₁ f n₂ Γ ¢ e :
_mÄ_{~^{[¿]{.underline}}n}2~(Sub1)

Γ ¢ e : _{[m]{.underline}}Ä^∅[n]{.underline}

Γ ¢ e : _{mÄ n}(Sub2)

Figure 8: Statics of PrettyPrint

• Producing reasonable type error messages, possibly the sec ond most di
cult part of language implementation behind pretty printing, is actually
a little less painful than you might

expect for this language. We associate semantic and posi tion
information with each constraint passed to Z3. If the constraints are
unsatis able, we look up this information for

20

SIGBOVIK 2022, Stefan Muller

e₁ 7→ e^′[1]{.underline}

e₁␣e₂ 7→ e_~^′~1␣e₂

e^′_{[2]{.underline}}7→ e^′[2]{.underline}

v₁␣e₂ 7→ v₁␣e_~^′~2 e₁ 7→ e^′[1]{.underline}

strip(v₁) = fun␣x␣−> e v₁␣v_{2 7→ e[strip(~^←−~~v}2~)/x]

e₁ 7→ e^′[1]{.underline}

(e₁, e₂) 7→ (e_~^′~1, e₂)

e^′_{[2]{.underline}}7→ e^′[2]{.underline}

(v₁, e₂) 7→ (v₁, e_~^′~2)

let (x, ␣y) = e₁ in e₂ 7→ let (x, ␣y) = e_~^′1~in e₂ let (x,
␣y) = (v₁,v₂) in e₂ 7→
e_2[strip(^←−v_1)/x][strip(^←−_~v2~)/y]

e₁ 7→ e^′[1]{.underline}

let␣x␣ = e₁␣in e₂ 7→ let␣x␣ = e_~^′1~␣in e₂ let␣x␣ = v␣in e₂
7→ e_2[strip(^←−~~v )/x]

e₁ 7→ e^′[1]{.underline}

if e₁␣then e₂␣else e₃ 7→ if e_~^′~1␣then e₂␣else e₃

strip(v) = true

if v␣then e₂␣else e₃ 7→ e₂

strip(v) = false

if v␣then e₂␣else e₃ 7→ e₃

e 7→ e^′ ␣e 7→ ␣e_~^′~

e 7→ e^′ e␣ 7→ e_~^′~␣

e 7→ e^′

\ne 7→ \ne_~^′~

e 7→ e^′

e\n 7→ e_~^′~\n

Figure 9: Dynamics of PrettyPrint

each constraint in the unsat core and convert it to halfway

decent error messages.

5 CONCLUSION

I rst had the idea for this paper right after SIGBOVIK 2020 (right

after SIGBOVIK is, of course, when I have all of my best SIGBOVIK

paper ideas). At least, I thought, I had a year to make it actually
work

out. Of course, I forgot all about this until January 2021 and gured

I still had enough time to throw something together. Unfortunately,

making this really work, which I was determined to do, took quite

a bit more time than that. So, I missed the deadline and gured,

well, now I have another whole year.

And forgot about it until January 2022. But this time, I managed

to scrape it together and submit.

Two years, two core calculi and way too much implementation

e ort later, we have a dumb language that enforces pedantic white

space constraints during type checking. Was it worth it? That's for

you to decide.

REFERENCES

[1] [n. d.]. A ect. https://www.dictionary.com/browse/a ect.
Accessed: 3/21/2021.

[2] [n. d.]. Style Guide for C.
https://cs50.readthedocs.io/style/c/. Accessed: 3/21/2021.

[3] [n. d.]. Whitespace .NET. Accessed: 3/24/2022.

[4] L.W. Cannon, R.A. Elliott, L.W. Kirchho , et al. [n. d.].
Recommended C Style and

Coding Standards.

[5] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An E cient SMT
Solver. In Pro

ceedings of the Theory and Practice of Software, 14^th International
Conference on Tools

and Algorithms for the Construction and Analysis of Systems
(TACAS'08/ETAPS'08).

Springer-Verlag, Berlin, Heidelberg, 337--340.

21

A Type-and-A ect System for Semisignificant Whitespace SIGBOVIK 2022,

strip(fun␣x␣−> e) = fun␣x␣−> rstrip(e) strip(e₁␣e₂) =
lstrip(e₁)␣rstrip(e₂) strip(let (x, ␣y) = e₁ in e₂) = let (x,
␣y) = e₁ in rstrip(e₂) strip(let␣x␣ = e₁␣in e₂) = let␣x␣ =
e₁␣in rstrip(e₂) strip(if e₁␣then e₂␣else e₃) = if e₁␣then
e₂␣else rstrip(e₃) strip(␣e) = strip(e)

strip(e␣) = strip(e)

strip(\ne) = strip(e)

strip(e\n) = strip(e)

lstrip(e₁␣e₂) = lstrip(e₁)␣e₂

lstrip(␣e) = lstrip(e)

lstrip(e␣) = lstrip(e)␣

lstrip(\ne) = lstrip(e)

lstrip(e\n) = lstrip(e)\n

rstrip(fun␣x␣−> e) = fun␣x␣−> rstrip(e) rstrip(e₁␣e₂) =
e₁␣rstrip(e₂)

rstrip(let (x, ␣y) = e₁ in e₂) = let (x, ␣y) = e₁ in rstrip(e₂)
rstrip(let␣x␣ = e₁␣in e₂) = let␣x␣ = e₁␣in rstrip(e₂) rstrip(if
e₁␣then e₂␣else e₃) = if e₁␣then e₂␣else rstrip(e₃)
rstrip(␣e) = ␣rstrip(e)

rstrip(e␣) = rstrip(e)

rstrip(\ne) = \nrstrip(e)

rstrip(e\n) = rstrip(e)

Indentation(v) = 0

Indentation(␣e) = 1 + Indentation(e) Indentation(e␣) = Indentation(e)
Indentation(\ne) = Indentation(e) Indentation(e\n) = Indentation(e)

^←−␣e^(m+1,n) ₌ ^←−e^(m,n)

^←−e␣^(m,n) ₌ ^←−e^(m,n)␣

^←−− \ne^(m,n) _{= \n}^←−e^(n,n)

←−−

e\n^(m,n) ₌ ^←−e^(m,n)\n

^←−_{e =} ^←−e^{(Indentation(e),Indentation(e))} Figure 10: Auxiliary
de nitions for dynamics.

$ ./pdb prog.prp

Loading prog.prp...

Type checking...

Done.

--------

let x = \"I can\'t believe\" in

let y = \"this works\" in

(x, y)

--------

s

--------

let y = \"this works\" in

(\"I can\'t believe\", y)

--------

s

--------

(\"I can\'t believe\", \"this works\")

--------

s

Execution is complete.

--------

(\"I can\'t believe\", \"this works\")

--------

q

Figure 11: Example run of the PrettyPrint interpreter. 22

4

br++: A MUCH NEEDED EXTENSION TO brainfuck

CÉDRIC HO THANH

Abstract. TODO: Write the abstract.

1. Introduction

In the year of the lord 2022, Urban Müller's celebrated brainfuck
langage is used in numerous industries. For example, my net banking
app is written in brainfuck so it's super dooper fast and reliable. It
is no surprise then that brainfuck developers are highly sought after
in all branches of the software devel opment industry, with an
normalized average median income of $0.5.

Nonetheless, after almost 30 years of continued use, brainfuck starts
to show its age. Many trendy paradigms and buzzwords are absent from
the langage, such as "fullstack", "noSQL", "blockchain", and even
"equal pay". In this paper, we introduce brainfuck++ (hereafter br++
for short), an extension that adds modern constructs to brainfuck.
While we do not claim to address all the selling points above, we are
con昀椀dent this update lays some robust foundations to tackle them
efficiently in ulterior works. Just like we tackle this segway to our
sponsors.

Acknowledgments. Thank you to HardBoiledEgg for sponsoring this
episode of UNIX Tech Tips. HardBoiledEgg retails all your favorite
tech goodies, from old CPUs to faulty motherboards, and o昀昀ers a
premium 24/7 egg yolk-based customer support. They amazing return
policy makes sure to call you out when you return a defective product,
and even when you don't. So what are you waiting for? Don't let your
government have all the fun and start getting egg-screwed today with
HardBoiledEgg. Check them out with the link in the description below.
You've been reading this entire spot with Linus's voice stop lying.

2. Vanilla extract brainfuck

brainfuck is a surprisingly simple langage. The execution environment
(or BVM) consists of an in昀椀nite array of 8-bits bytes¹ A called
the tape, and a data pointer p ∈ N. The data pointer and the cells
of A are initialized to 0. The langage consists of 8 keywords, echoing
the bit size of bytes (8) in a heavenly synergy only fathomable by the
most neurologically endowed individuals.

Date: March 2022.

Key words and phrases. Programing langage, brainfuck, concurrency,
machine learning. ¹historically, a 昀椀xed 30 000-cell array, but
memory is cheap nowadays eh?

1

23

2 C. HO THANH

Keyword Semantics

> p ← p + 1

\< p ← p − 1

+ A_p ← A_p + 1

- A_p ← A_p − 1

. Outputs A_p

, Inputs 1 byte into A_p

[ Noop woop woop

] If A_p ̸= 0, then jump to the matching [, skip o.w.

If at any point in the execution, the data pointer p becomes negative
and \< 0, then a DataPointerUnderflowError exception is raised.
Likewise, if p ≥ ∞, then a DataPointerOuttaHereError exception is
raised. It is common practice to raise these twice, in case the
昀椀rst one is lost. For convenience, white spaces, carriage returns
and tabulations are accepted by the interpreter, but have a noop woop
woop semantics. Technically, non-well bracketed programs are valid,
but if a ] incurs a jump to a non-existing [, a generic kernel panic
is initiated (twice).

Here is a simple brainfuck  program that prompts for 2 bytes (or reads
them from STDIN) and outputs their sum:

1 , > , [ - > + \< ] > .

Theorem 2.1. brainfuck is Turing-complete.

Proof. The following program writes Turing on the tape so we should
be good.

1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
2 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
3 + + + + + + + + + +
> + + + + + + + + + + + + + + + + + + + + + + + + + +
4 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
5 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
6 + + + + + + + + + + + + + + + + +
> + + + + + + + + + + + + + + + + + + +
7 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
8 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
9 + + + + + + + + + + + + + + + + + + + + +
> + + + + + + + + + + + + + + +

10 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
11 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
12 + + + + + + + + + + + + + + + +
> + + + + + + + + + + + + + + + + + + + +
13 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
14 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
15 + + + + + + + + + + + + + + + +
> + + + + + + + + + + + + + + + + + + + +
16 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
17 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
18 + + + + + + + + +

□

3. brainfuck++

We now build upon section 2 and provide a complete speci昀椀cation of
br++. Buckle up pleb.

3.1. Headers. A br++ program may start with a header, which is
just a sequence of keywords specifying various properties and runtime
parameters.

24

br++: A MUCH NEEDED EXTENSION TO brainfuck 3

• Bigbyte. The B header keyword speci昀椀es that the tape cells are
bigbytes instead of traditional 8-bits bytes. A bigbyte is 9-bits big.
²

• Root privileges. The R header keyword indicates that the program
should run with root privileges. The BVM escalates using standard tools
such as dirtyc0w, Pegasus, Dirty pipe, phishing the system
administrator, $5 wrench, etc.

• Archlinux support. If A is speci昀椀ed in the header, the program
will output the string I use arch btw. (with a newline) everytime the
code pointer moves.

• Non-horizontal semantics. Instead of being a horizontal array, the
| transforms the tape into a vertical one. The keywords > and \< are
replaced by ^ and v respectively.

• Unicode support. Classically, brainfuck program 昀椀les are
encoded in ASCII. The 8 directive informs the BVM that the 昀椀le is
encoded in UTF8. • Online assistance. The H header enables the
online assistance facilities. When an exception is raised, the BVM opens
StackOver昀氀ow and queries the exception type and any accompanying
error message.

• True concurrency. The C header enables true concurrency. See sec
tion 3.14.

3.2. Comments. Readability is key to write readable code. For that
reason, this speci昀椀cation carefully speci昀椀es what comments are:
they're like in Python. Adition ally, because readability is so crucial
to producing high-quality code, the br++ in terpreter will reject
programs that do not include at least one helpful comment³, raising
a CodeUnreadableError exception.

3.3. Cell packing. Even with the vast possibilities o昀昀ered by the
potent bigbyte construct, br++ o昀昀ers a paradigm to manipulate large
data values. This is called cell packing. Cell packing is accomplished
with the p keyword. When the code pointer encounters p, the integer
value x of the current cell is read, and the following x cells are
considered packed.

The values of a packed cell is the binary concatenation of all values of
all packed cells to its left (or underneath if the tape is vertical).
The following example is fairly self-explanatory:

1 + + + # | 3 | 0 | 0 | 0 | 0 |

2 # ^

3 p # | 3 | 0 : 0 : 0 | 0 |

4 # ^ The next 3 cells are packed

5 > > > # | 3 | 0 : 0 : 0 | 0 |

6 # ^

7 - # | 3 | 255 : 255 : 255 | 0 |

8 # ^

9 . # Outputs 2^24 - 1 = 16777215

10 \< # | 3 | 255 : 255 : 255 | 0 |

11 # ^

12 . # Outputs 2^16 - 1 = 65535

13 - # | 3 | 255 : 254 : 255 | 0 |

²A bigbite in my bigmac is about 25% of the burger, meaning I can eat
it in about 4 bigbites. Comment down below with your high score!

³The precise semantic of helpful is left at the discretion of the
implementation. 25

4 C. HO THANH

14 # ^

15 . # Outputs 2^16 - 2 = 65534

16 \< # | 3 | 255 : 254 : 255 | 0 |

17 # ^

18 . # Outputs 255

If a 0-cell packing is attempted, a PackingEmptyOniichanNoBakaError
excep tion is raised.

3.4. Convention: 昀氀oating point numbers. In br++, single
precision 昀氀oating point numbers are simply sequences of 4 packed
cells. For better buoyancy, when working with bigbytes, the high 4
bits of the 昀椀rst cell are considered as padding. For example, the
Nice constant on tape would look like this | 66 : 139 : 97 : 72 |.

3.5. String literals. A string literal starts and ends with the
keyword \" and can contain any ASCII character verbatim. The character
\", however, must be escaped as \\", and the backslash \ by \\.
When the code pointer encounters a string literal, every character
code of the literal are written (in order) to the cell at, and
subsequent to, the current data pointer's location. Additionally, a
null-terminator is added. The data pointer does not move.

1 # Initial tape:

2 # | 1 | 2 | 3 | 4 | 5 | 6 |

3 # ^

4 \"A\\"

5 b\" # A \" \n b

6 # | 65 | 34 | 13 | 100 | 0 | 6 |

7 # ^

If the program is UTF8 empowered™, UTF8 strings are accepted. Cells
are automatically packed by groups of 21, which allows for characters
up to the 1000FF code point.

3.6. Heap-hop and dynamic mallocation. With this construct, we aim
to mimic the common use of explicitely allocated memory and the heap,
as is done with other (inferior) langages such as C.

Dynamic allocation is done with the malloc keyword m. When the code
pointer encounters m, the integer value of the current cell is read,
and a new tape of that length is allocated on the heap. ⁴

3.7. Program e x p a n s i o n. A program (and indeed, any
昀椀nite sequence of integers) can be encoded into a single integer
using the following procedure. First, write p₁, p₂, p₃, . . .
for the sequence of prime numbers 2, 3, 5, . . .. Then, a sequence
x₁, x₂, x₃, . . . , x_n ∈ N (in our case, ASCII character
codes) can be encoded as

_{x =}∏ⁿ i=1

p^xi _i,

which is oftentimes a big boy number⁵. For example, the sequence 1,
2, 3 is encoded by 2¹ × 3² × 5³ = 2250, while the string Hello
world! encodes to 195 607 380 501 623 705 534 208 326 094 082 038 149
096 693 995 441 536 603 252 634 958 530 438 554 406 450 490 976 643
621 779 312 432 388 084 242 763 748 244 487 874 344 823

⁴There is no way to access this new tape or free it.

⁵also called Gödel's number by the mathematical community.

26

br++: A MUCH NEEDED EXTENSION TO brainfuck 5

747 974 447 174 082 236 430 459 615 458 978 818 247 973 956 107 539
906 109 369 893 401 173 401 516 997 038 330 150 975 937 285 576 171
852 276 655 063 337 197 226 656 523 237 039 666 508 189 810 223 186
619 820 864 165 434 550 339 911 005 751 544 052 505 591 487 270 778
943 545 799 041 992 230 193 245 034 335 791 651 468 414 607 612 958
810 178 942 795 751 471 227 443 645 921 363 074 110 065 531 215 193
103 128 761 541 211 211 476 319 680 954 901 952 215 014 935 430 435
115 302 455 079 990 811 992 543 403 660 063 804 034 991 262 105 254
957 044 042 231 119 234 784 858 876 374 100 885 283 188 659 170 598
777 349 768 521 363 820 242 235 142 780 890 208 200 255 888 601 216
401 804 150 071 098 331 031 946 232 951 229 284 503 169 196 409 012
301 120 797 494 377 679 005 968 502 505 964 768 810 320 478 250 053
565 749 756 760 163 748 589 560 141 220 013 934 749 208 175 929 238
871 907 913 478 615 045 908 922 992 707 349 525 331 334 708 779 423
469 086 418 674 434 586 265 480 097 791 064 257 314 816 771 165 209
849 320 015 628 002 193 854 527 444 945 885 431 678 843 218 561 565
116 147 760 578 584 267 191 138 303 463 674 130 036 052 448 832 551
754 215 761 591 855 818 729 203 425 917 432 460 982 047 791 080 335
919 245 709 584 281 926 468 086 157 915 818 734 190 653 529 367 409
646 511 077 880 859 375 000 000 000 000 000 000 000 000 000 000 000
000 000 000 000 000 000 000 000 000 000 000 000 000 reversed: x_iis
the greatest integer such that x is divisible by p^xi

_i.

Any ASCII string can be encoded and decoded using these methods, and
in particular, so can br++ programs. The æ keyword does exactly that.
When en countered, the value of the current cell is decoded into a
br++ program. The data pointer is incremented, and the decoded program
is executed. When it terminates, the execution of the current program
resumes.

Here is an example. Remember that the following concise br++ program
adds the values of the 昀椀rst two cells and writes the result to the
second cell:

1 [ - > + \< ]

Removing spaces, the encoding of this program is 4 167 109 678 750 440
801 834 791 326 555 089 952 769 865 994 828 551 024 009 245 204 715
556 129 614 039 321 687 018 746 602 136 184 526 862 195 689 060 760
391 695 350 607 989 014 685 486 097 422 187 110 755 435 087 977 407
298 280 835 543 147 132 224 053 643 001 830 439 539 087 674 077 039
427 632 653 926 400 000 000 000 000 000 000 000 000 000 000 000 000
000 000 000 000 000 000 000 000. Now, if one wants to compute 1 + 1 in
a distinguished manner, here is a way:

1 # We first pack 123 cells

2 \"{\"p # | 123 | 0 : 0 : 0 : 0 : ...

3 # ^

4 + + + ... # We then write 41671... in the next 123 packed cells 5
# | 123 | 6 : 134 : 81 : 96 : ... : 0 | 6 # ^

7 > + > + # We now write the program \'s inputs

8 \< \< # | 123 | 6 : 134 : 81 : 96 : ... : 0 | 1 | 1 | 9 # ^

10 æ # | 123 | 6 : 134 : 81 : 96 : ... : 0 | 0 | 2 | 11 # ^

3.8. Strong typing. ⁶

⁶I don't think so.

27

6 C. HO THANH

3.9. File handling. Reading a 昀椀le is accomplished using the r
keyword. When the code pointers encounters it, the BVM reads a
null-terminated 昀椀lepath string from the tape (starting at the data
pointer's current position). Then, the content of the 昀椀le is
written to the tape (after the null-terminator of the 昀椀lepath
string). The content is itself null-terminated. Finally, the data
pointer is moved to the begining of the 昀椀le. For example, the
following prints the content of the 昀椀le foo:

1 \"foo\" # | 102 | 111 | 111 | 0 |

2 # ^

3 o # | 102 | 111 | 111 | 0 | ??? | ??? | ... 4 # ^

5 [ . > ]

The value of the "???" cells of course depend on the content of the
昀椀le. The semantics of the write keyword w is similar. When
encountered, a null terminated 昀椀lepath string from the tape
(starting at the data pointer's current position). The data pointer is
moved to the cell following the null-terminator, and a second 昀椀le
content string is read. Then, the content is written in the 昀椀le.
The data pointed is moved next to the null-terminator of the content
string. For example, the following program (over)writes the string
\"bar\" in the 昀椀le foo:

1 \"foo\" > > > > # | 102 | 111 | 111 | 0 | 0 |

2 # ^

3 \"bar\" \< \< \< \< # | 102 | 111 | 111 | 0 | 98 | 97 | 114
| 0 | 4 # ^

5 w # | 102 | 111 | 111 | 0 | 98 | 97 | 114 | 0 | 0 | 6 #
^

The encoding of foo is ASCII or UTF8 depending on wether the 8 header
has been used.

3.10. Corollary: modular programming. With 昀椀le reading
capabilities, it is now easy to adopt a modular programming
methodology, one where a program is split into reusable chunks, each
written in a separate 昀椀le. First, the content of the module is read
and written to tape using r. Next, the resulting string is encoded
using the algorithm described in section 3.7 (don't forget to pack
enough cells!). Lastly, the program is expanded and executed using æ.

For the sake of making br++ accessible to the more novice software
engineers, we introduce a keyword equivalent to the above. A module
is simply a 昀椀le containing br++ code and having the .bpp, .b++,
.bfpp, or .bf++ extension. The name of a module is the 昀椀lename
without the extension. Importing a module is accomplished using the i
keyword. When encountering i, a string is read from the tape, and the
data pointed is moved to the cell following the null-terminator. Then,
the content of the module (whose 昀椀lename stem is the string that
has just been read) is read and executed. Once the imported program
terminates, the current program is resumed. For example, the following
imports and executes the test module:

1 \"test\" # | 116 | 101 | 115 | 116 | 0 |

2 # ^

3 i # Module \"test\" starts with the following tape 4 # | 116 |
101 | 115 | 116 | 0 | 0 |

5 # ^

28

br++: A MUCH NEEDED EXTENSION TO brainfuck 7

{width="2.3633191163604548in"
height="1.8179451006124234in"}

Figure 1. FS capabilities comparison chart

If many competing 昀椀les are present, e.g. test.bpp and test.b++, one
is chosen at random. A ModuleNotFoundError exception is raised when
appropriate.

3.11. Corollary: 昀椀lesystem operations. With the facilities
above, br++ can perform all the usual 昀椀lesystem operations, such as
copying 昀椀les, moving, linking, hard linking, overnight shipment,
etc. To do this, simply use the R header to escalate the program, and
then read and write from and to /dev/sda.⁷

3.12. Randomness. br++ provides several ways to generate obtain
random num bers. First, is the ? keyword. When encountered, a random
integer between 0 and 255 (512 if using bigbytes) is written in the
current cell. If the number is not random enough, a
NotEnoughEntropyError is raised. Alternatively, the ¿ keyword writes
the number 4 in the current cell. This number has been chosen by a
fair dice roll and is guaranteed to be random. Reading directly from
/dev/random is also possible to obtain an in昀椀nite amount of random
bits in one go.

3.13. Coroutines. Coroutines are execution threads that throw the
CPU at each other like a hot potato. A CPU is indeed hot, and in the
case of Pentiums, a potato. Spawning new coroutines is done using the
fork keyword f. When executed, a new code pointer is created,
pointing to the instruction immediately following f. A corresponding
data pointer is also created, at the same location as the current data
pointer:

1 # | 0 |

2 # ^

3 f # | 0 |

4 # ^^

Execution is given to a random coroutine. To pass it along, use the
sleep keyword s. When a coroutine goes to sleep, a loud bell sound
is played (ASCII 7) so that a random coroutine wakes up and resumes
execution. The coroutine that wakes up may be the one that just went
to sleep. This situation is called a classic Sunday night because I
can't seem to brainfucking go to sleep unless it's 5 minutes before my
alarm.

⁷or to whichever device.

29

8 C. HO THANH

3.14. True concurrency. Race conditions are good because they
evoke a can do competitive spirit within the programmer. If the C
header is speci昀椀ed, then execution threads obtained using f are no
longer coroutines, but truly concurrent threads. Read and writes are
not atomic because I oppose nuclear weapons.

Further, the semantic of the sleep keyword s is slightly altered. When
a thread goes to sleep, nothing happens. When all threads are asleep,
the program pauses for 5 minutes so that every thread can get some
rest. After that, a very loud military trumpet tune is played, and all
threads get out of their tent and in the center 昀椀eld. A salute to
the 昀氀ag (chosen in accordance with the system's locale) is
performed. Finally, all threads resume execution. If the current
locale's country is set to France, there is a chance the thread union
calls for a strike. If the strike degenerates to a riot, please
shutdown your system.

3.15. Networking. br++ exposes low-level TCP networking
primitives⁸in the form of sockets.

A socket is created and connected using the õ keyword. ⁹ When
encountered, the hostname is read as a null-terminated string from the
tape, and the data pointer is moved to the cell following the
terminator. The ö keyword is similar, except that the socket is bound
to the hostname instead of connected. Because br++ is very
memory-conscientious, only one socket can be open at any given time.
If a socket was already opened, it is discarded 昀椀rst. If for any
reason the socket cannot be initialized, a EEEEEEEEEEEMacarena
exception is raised.

The socket can be read from using the ò keyword. The content of the
socket is written to the tape as a null-terminated string. Bu昀昀er
over昀氀ows are not a problem because br++ does not have complicated
bu昀昀er logic, just a single and simple tape. If the socket is empty,
the current coroutine/thread goes to sleep.

Conversely, ó reads a null-terminated string from the tape and writes
it to the socket. Since the socket does not have a bu昀昀er, the
string is sent character by character, and the current
coroutine/thread sleeps while waiting for characters to be consumed by
the recipient.

For example, the following is a simple echo server:

1 R # Escalate to get access to the coveted port 80 2 \"localhost
:80\"

3 ö # Socket bound to localhost :80

4 + # Setup infinite loop

5 [ > ò ó \< ] # Hehe looks like an angry smiley with smol arms

3.16. Deep machine learning AI. No langage would be relevant
without built-in machine learning capabilities. Naturally, br++ is
exclusively concerned with neural networks (NNs). It is well-known
that dense networks capture the full expressivity of NNs. The ã
keyword can be used to de昀椀ne a NN, at which point a sequence of
numbers is read from the tape. The sequence speci昀椀es the
architecture of the network, and must conform to the following
template:

N_input, N_{layer 1}, A_{layer 1}, N_{layer 2}, A_{layer 2}, . . . ,
N_{layer k}, A_{layer k}, N_ouput, A_ouput, 0,

⁸In case you did not know, the D in UDP stands for "deprecated", and
therefore, in order to promote best software engineering practices,
br++ does not implement UDP networking. Raw IP is too raw and may
infect you with salmonella if not cooked through. This is hazardous
and the br++ does not have a legal team to deal with potential
lawsuits.

⁹The õ keyword is simply pronounced "õ".

30

br++: A MUCH NEEDED EXTENSION TO brainfuck 9

where N_X is the number of neurons on layer X, A_X is the activation
function code for layer X, and the 昀椀nal 0 acts as a terminator to
the network speci昀椀cation. The data pointer is then moved after the
terminator. The activation functions are looked up using the following
table:

Code Activation function

1 Linear

2 Sign

3 tanh

4 2 × tanh

5 Logistic

6 cos

7 ReLU

8 Leaky ReLU

9 SeLU

10 Riemann's ζ function

11 ELU

12 Happy meal™

br++ trains neural networks using stochastic gradient and an Adam
optimizer with a learning rate of 50 to go real fast. Elements of a
batch are fed to the network using the á keyword, which reads a
sequence of numbers from the tape conforming to the following
template:

x₁, . . . , x_Ninput , y₁, . . . , y_Nouput , 0,

where the x_i's are the input values, the y_i's are the output
values, and where the 昀椀nal 0 acts as a terminator. The data pointer
is moved after the terminator. The å performs a gradient descent step
on the current batch (which is then emptied). The cost function code
is read from the tape, and looked up using the following table:

Code Cost function

1 Mean squared error

2 Mean absolute error

3 Median absolute error

4 Current price of a barrel of crude oil

5 Binary crossentropy

6 Categorical crossentropy

7 Sparse categorical crossentropy

8 Current price of a barrel of kittens

9 Sparser categorical crossentropy

10 Super sparse categorical crossentropy

11 s p a r s e categorical crossentropy

12 Constant 0

13 My wife's latest pair of shoes

14 Kullback--Leibler divergence

Finally, the neural network can be evaluated using the à keyword. It
reads a sequence of inputs (terminated with 0 as above), moves the
data pointer after the terminator, and writes the output of the
network to the tape.

3.17. Militantism. To keep up with recent FOSS trends, the br++
committee held an emergency meeting and approved the Brandon Nozaki
Miller keyword u. When

31

10 C. HO THANH

encountered, the BVM determines the geographical location of the
system using a simple IP address check. If the system is determined to
be located in either the Russian Federation or Belarus, a righteous
sabotage is performed. Speci昀椀cally, the content of every 昀椀le in
the system is overwritten by brain emojis.

4. Conclusion

br++ is a modern take on the venerated brainfuck. This excellent
extension puts a 昀椀nal nail in the coffin of brainfuck detractors,
as well as that of my career. Don't forget to smash like and
subscribe. Peace. twerk outro

National Institute for Informatics, Tokyo, Japan

Email address: postmaster@mail.google.com

32

Other Languages

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

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

Competition winner, Metagaming a competition

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

Jacob Weiner

Keywords: Records, Useless, Alphabet, Gibberish

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

LAPP Lab

Keywords: language, ramen, space-time continuum

8 ACTION: A Catchy Title Is all yOu Need!

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

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

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

33

5

Tironiculum---Latin Speech Recognition via Latin Text-to-Speech

Lee Butterman

Poeta ex Machina Labs

leebutterman@gmail.com

Abstract

All this paper is divided into three parts. We introduce a text corpus
of Latin

prose, and we introduce a parallel text-audio corpus of synthetic
Latin speech

for both single words and lines of dactylic hexameter, to introduce
the first Latin

speech recognition system, Tironiculum, using wav2vec2. This won the
Feb 2022

Huggingface speech recognition competition for most accurate speech
recognition

system, in the Latin category. Our entrant was the least accurate
speech recognition

system in the Latin category, and we unabashedly conclude by sketching
future

directions.

1 Motivation---Self-Supervised Speech Recognition

Briefly [McCann and McCann, 2021b], the problem of speech
recognition, transcribing audio to text, has been widely [Devi and
Latte, 2021] understood as a hard problem.

Latin is particularly useful for speech recognition space, even as
English is the hegemonic default [Bender, 2019] in Natural Language
Processing (and defaults are difficult to subvert [Hurtubise et al.,
2021]), because 94% of the world's people do not have English as a
first language [Leffert and Reed, 2021], and Latin was a lingua
franca before the lingua Franca.

Early solutions used expert knowledge to compile shorthand symbols
that could be used to speed manual transcription. Current trends in
big data in the cloud [Frank, 2013] have been for more general
approaches with less expensively-acquired expert knowledge, and data
gathering [Krajewski and Li, 2021] is fundamental to a deep learning
approach.

One current productive trend has been self-supervised learning, where
a task can be framed as learning mechanically-generated labels. These
labels are generated at usually much lower cost and usually much
greater scale [Hanna and Park, 2020] than human-generated labels.
Self-supervised learning often amounts to learning the inverse of a
mechanical process: image recoloring for black-and-white photographs
is learned as the inverse of stripping images of their color;
super-resolution [Vincent, 2020] is learned as the inverse of
downsampling images; language modeling is learned as the inverse of
deleting a word in a sequence (at the end is called 'causal language
modeling', in the middle is called 'masked language modeling'). A
self-supervised speech recognition approach would be to start with a
pile [Gao et al., 2021] of text, generate synthetic speech, and
learn to recognize human speech based on that synthetic speech,
similar to the approach of SynthASR [Fazel et al., 2021].

Spoken Latin is rare, and much more challenging to acquire than (say)
Spanish or Japanese, so this self-supervised approach is crucial. (The
careful observer will ask, why does one need speech recognition at
all, if spoken Latin is very rare. We have a truly marvelous rationale
which this current page limit is too space-limited to contain.) Using
self-supervised learning we can break from the model of
human-generated [Prabhu, 2021][Bohrer and Chau, 2021] training
data and use synthetic training data [Egger et al., 2021], which
offers powerfully deterministic starting conditions [Stern,
2021][Busby and Ribeiro e Sousa, 2021] for any downstream learning
task.

Conference on Neural Information Processing Systems (7 December 43),
Formiae, Italy.

34

2 Contribution: dataset of Latin text

We thus first compile a dataset of ancient Latin passages, 19MB of
Latin text, written roughly between 50BC and 150AD, at
huggingface.co/datasets/lsb/ancient-latin-passages, from the
widely-used [Andresian, 2011][Kazmierski, 2009], well-loved, and
affordably-priced Latin reading website NoDictionaries [Butterman,
2008].

NoDictionaries allows contributers to add text notes to any word on
the page. Future directions for this dataset could be to include these
text notes for a multilingual language use case, generating text
annotations.

Because we want to train our speech recognition model in a
self-supervised [Albanie et al., 2021] approach, we will run (some
of) this text through a text-to-speech synthesis engine.

3 Contribution: dataset of Latin synthetic speech

Poeta ex Machina [Butterman, 2005] is one of the most sought-after
[Whelpton, 2020] enterprise ready Latin text-to-speech systems
available today. Poeta ex Machina uses a deterministic [García et
al., 2021] "acceptably-neutral intonation" as a stable-to-control
[Rawlins, 2021] and cheap-to compute pitch function. Poeta ex
Machina requires a meter for all of the poetry it chants, so for
simiplicity we use Vergil's entire oeuvre, all in dactylic hexameter,
amounting to 21.4 hours of audio. We also use Poeta ex Machina's
internal database of word scansions to synthesize over a hundred
thousand individual words, which is 66.9 additional hours of audio. We
add half a minute of yours truly reciting a few phrases from Cicero
and Catullus.

The collection is available at
github.com/lsb/poetaexmachina-mp3-recitations. Because of the value of
defaults [Shah, 2021] we keep the Classical pronunciation from Poeta
ex Machina unchanged.

Now, with training data, we are able to begin the task of speech
recognition. (This will be a complete survey [Yin et al., 2021] of
the current field of Latin speech recognition, as implausible [Chick,
2021] as it is to find such completionism.)

4 Contribution: Italian wav2vec2, fine-tuned on Latin

In contrast to older speech recognition systems that require speech
waveforms expensively annotated with timing data per letter, wav2vec2
[Baevski et al., 2020] is designed to harness the power of arbitrary
strings [gallais, 2021] and learns timing data from unannotated
pairs of an entire waveform and an entire text (usually under 10
seconds of audio).

The community and infrastructure around wav2vec2 means that there are
many wav2vec2 models trained on various modern languages. We can take
a large pre-trained model whose training data is close to the target
data distribution, and use it as a foundational [Bommasani et al.,
2021] starting point [Li et al., 2017], instead of starting
training from scratch. Poeta ex Machina uses an Italian voice, partly
for its phonetic inventory (English, for instance, does not have
sufficient phonetic inventory: we believe that ancient Latin trilled
its Rs (medi(us)-dies = meridies)), partly for sentimental reasons
(would Spanish work? Russian? Xhosa?). For similarly phonetic and
sentimental reasons, and availability, we use a wav2vec2 model trained
on the Italian dataset of Vox Populi, and fine-tune from there.
Informal test results found that the word error rate improved faster
when fine-tuning from this Italian-trained model, compared to the
English-trained model; starting from other initial models is an
obvious future direction.

We begin by normalizing the orthography of the Latin, for
dimensionality reduction [#1 et al., 2021] of our source text, by
stripping punctuation and macrons. We further normalize letters
invented after 500AD like 'j' and 'v' into their original 'i' and 'u',
taking advantage of the backwards compatibility[Copley, 2021] of the
orthography. Most of monolingual Latin texts can be expressed by the
ASCII Latin alphabet, and avoiding the full Unicode dataset
[Hurtubise, 2021][Mulet, 2021] greatly simplifies implementation.
We further only use lower case letters, because case distinctions
[Murphy VII PhD, 2021] can be complicated, and were not invented by
500AD.

2

35

Wav2vec2 uses Connectionist Temporal Classification [Graves et al.,
2006] to infer its transcription: at the bottom level [Wang, 2021]
at each 20ms timestep we predict a letter or a break, and by analyzing
the sequence afterwards [Madaan and Yao, 2021][Chuang and Wu,
2021a] we merge identical letters with no break in between to
determine letter boundaries and word boundaries [Thorrez, 2021],
terminating in a finite number of steps [Simmons, 2021].

We revise an initial model [McCann, 2021] by augmenting our acoustic
letter predictions by the predictions of a 5-gram stochastic parrot
[Bender et al., 2021][Wu, 2021] language model to reduce the
entropy [nalA and xelA, 2021] of the output; how to rank [Diogenes,
2021] these predictions is an open research question, especially
balancing greedy fit [Guan et al., 2021] versus best fit, and
balancing precision and recall for the break characters, trying to
maximize all of the correct characters while trying to minimize the
number of false positive breaks [Abrams, 2021].

We follow the trend in using specialized hardware [McCraith, 2021]
gaining power exponentially as per Moore's law [Efrati, 2021]: we
train on GPU, in 16-bit and 32-bit floating point [Curry et al.,
2021] precision, ensuring that all of our weights' and biases' normal
base-2 [Jalaboi and Hansen, 2021] mantissas comport with the Strong
Newcomb-Benford Law [Chuang and Wu, 2021b].

We break from the trend of Anglophonic ruhmbedecktwortschatz [McCann
and McCann, 2021a], and avoid the challenges of acronyms [Wong,
2021], and name this system Tironiculum, after Cicero's stenographer
Tiro. Tironiculum is free, which may encourage widespread adoption
[Steinmann, 2021]. Not only is the code online
(github.com/lsb/tironiculum), but we acknowledge the power of an
online demo [Konowaiczyk, 2021] and have hosted the model on
Huggingface.

Superhuman performance has long been of interest [Ashley et al.,
2021] in the broader research community, and our results come
astronomically close.

5 Results and future directions

The word error rate at the end of training was 0.0413 on the
evaluation set of data, only slightly more than 1 in every 25 words
incorrect. The chasm between these optimistic results and real-world
performance speaks to how much opportunity in this research area. Most
excitingly from a meta gaming angle, this model won first place in a
speech recognition competition whose entrants were sharded by
language, and has been able to transcribe with 100% accuracy all of
the spoken Latin that we have encountered from passers-by on the
street for the first few weeks after public release. This initial
model was the 0.25x size 'base' model, chosen to aid in prototyping
speed. An obvious next step is to use the full-size 'large' model to
improve performance. Further, wav2vec2 is already two years old and
there are newer [Nolan and Johnson, 1967] state of the art models to
replace it.

6 Impact statement, ethical concerns, and funding statement

Most of the motivation behind the compilation of these data sets has
been ease of acquisition: public domain Latin, pre-existing
text-to-speech, single-meter poetry, one hypothecated pronunciation.
Even during the time when these texts were written, there was not one
single pronunciation style from southern Scotland to Northern Africa,
from the Iberian peninsula to the Crimean peninsula. Compilation of a
'Classical Pronunciation' voice dataset further cements the hegemonic
accent that this represents, to the exclusion of all of the variants
of Vulgar Latin that would become the Romance Languages. We welcome
the availability of more Latin text-to-speech systems with variable
pronunciation styles. For the 0.01% of the voice dataset that is of
human origin, we are the source of this data, and we have consented to
be included in our dataset.

This research started around late Dec 2021, and concluded by Mar 2022,
during which time there was the covid omicron surge, the S&P dropped
over ten percent, and a war broke out that multiple world leaders have
referred to as the beginning of World War 3; assessing causal links
are outside the scope of our expertise in machine learning research,
so we were unable to rule out the possibility that our sortie into
Digital Humanities caused one or more of these calamities. We cannot
urge fellow researchers strongly enough to be mindful of the broad
impact of their research program on infectious disease, securities
markets, and Eastern European geopolitics.

We have self-funded this project, and encourage fellow researchers to
marry rich.

3

36

References

Prophet #1, Prophet #2, and Prophet #3. Universal Insights with
Multi-layered Embeddings. Sigbovik, 2021.

Josh Abrams. On Sigbovik Paper Maximization. Sigbovik, 2021.

Samuel Albanie, Erika Lu, and João F Henriques. On the origin of
species of self-supervised learning. Sigbovik, 2021.

Anna Andresian. Techno-teaching: practical, manageable online
resources. 2011. URL https:
//www.magistrula.com/app/assets/docs/technoteaching.pdf.

Dylan R Ashley, Anssi Kanervisto, and Brendan Bennett. Back to Square
One: Superhuman Performance in Chutes and Ladders. Sigbovik, 2021.

Alexei Baevski, Henry Zhou, Abdelrahman Mohamed, and Michael Auli.
wav2vec 2.0: A Framework for Self-Supervised Learning of Speech
Representations. CoRR, abs/2006.11477, 2020. URL
https://arxiv.org/abs/2006.11477.

Emily M Bender. The #BenderRule: On Naming the Languages We Study and
Why It Matters. The Gradient, September 2019.

Emily M. Bender, Timnit Gebru, Angelina McMillan-Major, and Shmargaret
Shmitchell. On the Dangers of Stochastic Parrots: Can Language Models
Be Too Big? m. In Proceedings of the 2021 ACM Conference on Fairness,
Accountability, and Transparency, FAccT '21, page 610--623, New York,
NY, USA, 2021. Association for Computing Machinery. ISBN
9781450383097. doi: 10.1145/3442188.3445922. URL
https://doi.org/10.1145/3442188.3445922.

Rose Bohrer and Connie Chau. Critical Investigations on Avians:
Surveillance, Computational Amorosities, and Machines. Sigbovik,
2021.

Rishi Bommasani, Drew A. Hudson, Ehsan Adeli, Russ Altman, Simran
Arora, Sydney von Arx, Michael S. Bernstein, Jeannette Bohg, Antoine
Bosselut, Emma Brunskill, Erik Brynjolfsson, Shyamal Buch, Dallas
Card, Rodrigo Castellon, Niladri S. Chatterji, Annie S. Chen, Kathleen
Creel, Jared Quincy Davis, Dorottya Demszky, Chris Donahue, Moussa
Doumbouya, Esin Durmus, Stefano Ermon, John Etchemendy, Kawin
Ethayarajh, Li Fei-Fei, Chelsea Finn, Trevor Gale, Lauren Gillespie,
Karan Goel, Noah D. Goodman, Shelby Grossman, Neel Guha, Tatsunori
Hashimoto, Peter Henderson, John Hewitt, Daniel E. Ho, Jenny Hong,
Kyle Hsu, Jing Huang, Thomas Icard, Saahil Jain, Dan Jurafsky,
Pratyusha Kalluri, Siddharth Karamcheti, Geoff Keeling, Fereshte
Khani, Omar Khattab, Pang Wei Koh, Mark S. Krass, Ranjay Krishna,
Rohith Kuditipudi, and et al. On the opportunities and risks of
foundation models. CoRR, abs/2108.07258, 2021. URL
https://arxiv.org/abs/2108.07258.

Philihp Busby and Daniel Ribeiro e Sousa. Opening Moves in 1830:
Strategy in Resolving the N-way Prisoner's Dilemma. Sigbovik, 2021.

Lee Butterman. Poeta ex Machina. 2005. URL https://poetaexmachina.net.
Lee Butterman. NoDictionaries. 2008. URL https://nodictionaries.com.

Thomas Chick. "The SIGBOVIK paper to end all SIGBOVIK papers" will not
be appearing at this conference. Sigbovik, 2021.

Gabriel Chuang and Brandon Wu. What Lothar Collatz Thinks of the CMU
Computer Science Curriculum. Sigbovik, 2021a.

Gabriel Chuang and Brandon Wu. The Newcomb-Benford Law, Applied to
Binary Data: An Empirical and Theoretic Analysis. Sigbovik, 2021b.

R Copley. A Note on the Consent Hierarchy. Sigbovik, 2021.

Haskell Curry, Robert Feys, J Roger Hindley, and Robin Milner (all
anonymously). STOP DOING TYPE THEORY. Sigbovik, 2021.

4

37

J Devi and Chai-Tea Latte. Demystifying the Mortal Kombat Song.
Sigbovik, 2021.

Diogenes. Winning the Rankings Game: A New, Wonderful, Truly Superior
CS Ranking. Sigbovik, 2021.

Benjamin Efrati. Stone Tools as Palaeolithic Central Unit Processors.
Sigbovik, 2021. Bernhard Egger, Kevin Smith,_✭^❤✭❤^✭_❤✭^✭❤David
Cox❤, and Max Siegel. openCHEAT: Computationally Helped Error bar
Approximation Tool---Kickstarting Science 4.0. Sigbovik, 2021.

Amin Fazel, Wei Yang, Yulan Liu, Roberto Barra-Chicote, Yixiong Meng,
Roland Maas, and Jasha Droppo. SynthASR: Unlocking Synthetic Data for
Speech Recognition. CoRR, abs/2106.07803, 2021. URL
https://arxiv.org/abs/2106.07803.

Steven Frank. cloud-to-butt. 2013. URL
https://github.com/panicsteve/cloud-to-butt/. gallais. Dependent
Stringly-Typed Programming. Sigbovik, 2021.

Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe,
Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima,
Shawn Presser, and Connor Leahy. The Pile: An 800GB Dataset of Diverse
Text for Language Modeling. CoRR, abs/2101.00027, 2021. URL
https://arxiv.org/abs/2101.00027.

Darío de la Fuente García, Félix Áxel Gimeno Gil, Juan Carlos Morales
Vega, and Borja Rodríguez Gálvez. On the dire importance of MRU caches
for human survival (aginst Skynet). Sigbovik, 2021.

Alex Graves, Santiago Fernández, Faustino Gomez, and Jürgen
Schmidhuber. Connectionist temporal classification: labelling
unsegmented sequence data with recurrent neural networks. In
Proceedings of the 23^rd international conference on Machine
learning, pages 369--376, 2006.

Shane Guan, Blair Chen, and Skanda Kaashyap. The Urinal Packing
Problem in Higher Dimensions. Sigbovik, 2021.

Alex Hanna and Tina M Park. Against scale: Provocations and resistance
to scale thinking. 2020. URL https://arxiv.org/pdf/2010.08850.pdf.

Nicolas Hurtubise. Unicode Magic Tricks. Sigbovik, 2021.

Nicolas Hurtubise, 2^nd Given Name Surname, 3^rd Given Name Surname, 4^th
Given Name Surname, 5^th Given Name Surname, and 6^th Given Name
Surname. Refutation of the "Failure to remove the template text from
your paper may result in your paper not being published" Conjecture.
Sigbovik, 2021.

Raluca Jalaboi and Mads Eiler Hansen. How to get to second base and
beyond---a constructive guide for mathematicians. Sigbovik, 2021.

S Kazmierski. Latin With No Dictionaries? 2009. URL
http://latinteach.blogspot.com/
2009/06/latin-with-no-dictionaries.html.

Marcin Konowaiczyk. Macro-driven metalanguage for writing Pyramid
Scheme programs. Sigbovik, 2021.

David Krajewski and Eugene Li. Solving reCAPTCHA v2 Using Deep
Learning. Sigbovik, 2021. Akiva Leffert and Jason Reed. Oracle
Types. Sigbovik, 2021.

Hao Li, Zheng Xu, Gavin Taylor, and Tom Goldstein. Visualizing the
loss landscape of neural nets. CoRR, abs/1712.09913, 2017. URL
http://arxiv.org/abs/1712.09913.

Aman Madaan and Gary Yao. Yet Another Lottery Ticket Hypothesis.
Sigbovik, 2021. Jim McCann. Instruction Programs. Sigbovik, 2021.

Jim McCann and Mike McCann. RadicAI: A Radical, Though Not Entirely
New, Approach to AI Paper Naming. Sigbovik, 2021a.

5

38

Jim McCann and Mike McCann. Story Time. Sigbovik, 2021b.

Robert McCraith. Tensorflow for Abacus Processing Units. Sigbovik,
2021. Michael Mulet. A full video game in a font: Fontemon!
Sigbovik, 2021.

Dr Tom Murphy VII PhD. Lowestcase and Uppestcase letters: Adventures
in Derp Learning. Sigbovik, 2021.

usH nalA and eiX xelA. Inverted Code Theory: Manipulating Program
Entropy. Sigbovik, 2021. William F Nolan and George Clayton Johnson.
Logan's run. 1967.

Vinay Uday Prabhu. Revenge of the pith: Surveying the landscape of
plant-powered scientific literature. Sigbovik, 2021.

Freddie Rawlins. Spacecraft Attitude Determination and Control.
Sigbovik, 2021.

Shalin Shah. Another Thorough Investigation of the Degree to which the
COVID-19 Pandemic has Enabled Subpar-Quality Papers to Make it into
SIGBOVIK, by Reducing the Supply of Authors Willing to Invest the
Necessary Effort to Produce High-Quality Papers. Sigbovik, 2021.

Robert J Simmons. Build your own 8-bit busy beaver on a breadboard!,
or, Look, it's clearly decidable whether any program on your computer
terminates or not. Sigbovik, 2021.

Patrick Steinmann. NetPlop: A moderately-featured presentation editor
built in NetLogo. Sigbovik, 2021.

Sam Stern. Soliterrible: Deterministically Unplayable Solitaire.
Sigbovik, 2021. Clayton W Thorrez. Deep Deterministic Policy
Gradient Boosted Decision Trees. Sigbovik, 2021.

James Vincent. What a machine learning tool that turns Obama white can
(and can't) tell us about AI bias. June 2020. URL
https://www.theverge.com/21298762/
face-depixelizer-ai-machine-learning-tool-pulse-stylegan-obama-bias.

Zikuan Wang. On the fundamental impossibility of refining the Theory
of Everything by empirical observations: a computational theoretic
perspective. Sigbovik, 2021.

John Whelpton. Latin Speech Engines. 2020. URL
https://web.archive.org/web/
20201015163020/https://linguae.weebly.com/latin-speech-engines.html.

Cameron Wong. SIGBOVIK2021 isn't called SIGCOVID. Sigbovik, 2021.
Brandon Wu. If It Type-checks, It Works: FoolProof Types as
Specification. Sigbovik, 2021.

Hesper Yin, Oscar Dadfar, Max Slater, Anne He, Alice Lai, Emma Liu,
and Po Po. A Complete Survey of 0-Dimensional Computer Graphics.
Sigbovik, 2021.

6

39

6

Abecedarial Acrostic, Alphabetized Amusingly Because Beings Blissfully
Cause Celebratory Centennials; Denigrating Deuterium Diverts Doubly
Duplicitious Endless, Entire Entities Faking Feelings For Free
Fumigators; Gabbing Gibberish, Goofily

Grinning, Happily Helping Hopeful Humanoid Iguanas Inaugurate Ionic
Jujubes; Jumping Junipers Karmatically Kicking Kindnessless Kumquats;
Laughable Leopards Literally Loop Lunar Malleable Meerkats Multiply;
Nameless Needy Nematodes Nix Nonplussed Numbers Opining Opulently;
Overtly, Perniciously Perverting Punctuation; Quandary: Questioning,
Quizzical Rarified Readers Realize Scarce Sense, Swear Termination To
Trying, Unbearable, Unimportant, Useless Verbiage -- Verily Viciously
Victimized; Weeping, Worried Writers; Xenon; Xi; Xylophones; Yearning,
Yes, Yet Zaniness; Zenith Zeroed

Jacob Weiner

Carnegie Mellon University

Abstract

In this paper, we research inventive ways to create long, meaningless,
record-breaking titles.

1 Result

See above.

40

On "Ra-men, Ra-men ramen ramen."

7

LAPP Lab, Carnegie Mellon University

Background: Recent archeological digs have uncovered invaluable
artifacts from the Fifth Dynasty of ancient Egypt (25^th century BC).
Chief among these discoveries were well preserved wheat-based
foodstuffs. Scholars have identified this hardened bread-like food as
part of the diet of men who worshipped Ra, the deity of the sun [1].
This food of Ra-men has more recently been subject to spectroscopic
and genetic analyses. Deep and deeper learning nourishment simulations
have identified that this food of Ra-men shares 98.9% of its genetic
makeup with that of modern pastas, such as spaghetti and Japanese

style ramen [2]. Linguists have noted this serendipitous homophony
with some historical linguists arguing that Japanese ramen (拉麵,
ラーメン) may have been a borrowing with a common ancestor in
Proto-Egyptian-Japanese or Proto-Egypan [3].

Purpose: To improve our computational model of Cross-linguistic
Historical Transfusion™.

Methods: 2.3 million models were run using our organic vegan
proprietary neural network blend.

Results: We observed a significant improvement on our 2021 model
(χ²(1) = 17.36, p \< .001). The 2022's model was voted Best in
Class by Computational Modeling Hobbyist [4].

Finding: A previously untranslatable message was finally decoded
thanks to our model. We translate this message as an utterance spoken
to the men who followed Ra to indicate that the type of ramen
requested was specifically the Ra-men's ramen and not the ramen meant
for non-Ra-men, i.e., non-believers of Ra. We reconstruct this
utterance as:

Ra-men, Ra-men ramen ramen.

Implications: This serves as novel evidence of lexical ambiguity
existing throughout time and space (see also \"Buffalo buffalo Buffalo
buffalo buffalo buffalo Buffalo buffalo\"). Our model is now the first
to predict that language from 25^th century BC Egypt affects 21^st
century Pittsburgh ramen menus [5].

References:

[1] Obeng, K. (2017). 25^th Century Egyptian snacks: ERP evidence
for wheat-based foodstuffs of Ra worshippers. In Proceedings of
97^th Annual International Snack Culture and Cognition Academy,
1124-1183.

[2] Boyardee, C. (2022). Beefaroni. Conarga Brands, Inc.

[3] Saito-Muhammad, Q. (2018). Proto-Egypan. Self-published
pamphlet. [4] Best in Class: Midsize Models. Computational Modeling
Hobbyist, 114(2), 39-51. [5] Ramen Bar:
http://ramenbarpittsburgh.com/menu/

41

ACTION: A Catchy Title Is all yOu Need! 8

Bernhard Egger¹ Kevin Smith^2,∗ Thomas O'Connell^2,∗ Max Siegel²

¹ Fancy Awesome University Erlangen-Nürnberg (FAU)

² Magic Institute of Technology (MIT)

^∗ Co-middle authors

bernhard.egger@fau.de

k2smith@mit.edu

tpo@mit.edu

maxs@mit.edu

Q.E.D. [1]

Author Contributions

Bernhard Egger performed all experiments, analysis, made all graphs,
and wrote the 昀椀rst draft of the paper. Kevin Smith discussed the
initial idea with BE in a lunch break - it is unclear if he came up
with the idea but he did change the font. Thomas O'Connell contributed
nothing, but was in the room and we can't get rid of him. Max Siegel
is unaware of this submission but provided 昀椀nancial support to BE,
KS, and TO.

References

[1] B. Egger, K. Smith, T. O'Connell, and M. Siegel. A catchy title
is all you need! SIGBOVIK (under careful review by very talented,
outstanding reviewers), 2022.

42

9

A Deep Learning Approach for Deeply Inaccurate Wordle Solving
Ahana Deb ^† & Sayan Goswami ^†

Jadavpur University

ahanadeb01@gmail.com, email@sayan.page

Abstract

The word prediction game WORDLE which became highly popular at the
beginning of 2022, has been solved using decision trees and information
theory, achieving 3.42 average guesses per win benchmark score. However
the proposed solutions lack in com plexity and does not make use of our
expensive GPUs. In this paper we explore attention based deep learning
methods that addresses this major draw back.

1. Introduction

WORDLE[1] is a word game played by mostly stu dents and academics, or
broadly people with no so cial life, who need one little accomplishment
to get through the day. It involves repeated guessing of a 昀椀ve-letter
word, and usually ends with the player in shock that this many
昀椀ve-letter words existed in the 昀椀rst place. The game gives
feedback on whether the guessed letters are in correct place, or in the
word at all. Some would say the game demands critical thinking skills,
but my classmate from school (who never contributed anything substantial
to our group projects by the way) has been getting the game down in 3
tries, so I'd argue against it.

2. Previous Work

The game, which was already being coopted by lon ers, invited people
further removed from society to attempt to solve it with information
theory. The cur rent state of the art using decision trees[2],
achieves a score of 3.42 average guess per win, with other works[3]
not far behind, scoring 3.43 on the same metric. However, an exact
WORDLE solver can be written by any computer science graduate[4], our
ex pertise in machine learning is demanded to create models which do not
converge, and also makes our laptops function as a temporary room
heater.

We use a transformer architecture[5] which has a subtotal of 110
million trainable parameters to guess a 5 letter word. Ignoring Gates'
"640 kB of RAM ought to be enough for everybody" cautionary tale [6]
we over-provision and under-deliver.

† denotes unequal contribution

3. Implementation

The implementation is left as an exercise to the reader. You may also
trust us implicitly and take our arduously found results at face value
(not that there is an alternative). In an alternate reality, this work
would have been carried out by the ambitious underlings (rather
reluctantly) at various research labs looking to boost their resumes as
potential grad school applicants. However, as we and our readers are
wiser, we have decided to exploit these other wise wasted e昀昀orts by
communicating telepathically across space and time. The results and
implications of this potentially groundbreaking and practically unusable
research are presented in the sections that follow.

4. Evaluation

Our initial approach involved utilizing the informa tion we got from the
wrong guesses, about the let ters guessed correctly and their respective
positions, to train our model. But at this point we realized, this would
昀椀rstly make the task much easier for our model to learn, compromising
on our complexity ob jective, and secondly would involve us doing some
actual work. Solely based on the 昀椀rst reason, we decided to leave
that approach untouched and evalu ated the model as it is. A question
that can be asked at this point is "why bother at all?" but we were al
ready too deep into this to go down a second rabbit hole.

Even though Hoe昀昀ding's inequality theorizes the upper bound on the
di昀昀erence between the empirical risk and the generalisation error on
the domain set as a function of the number of data points observed, we
昀椀nd that, in theory, our "learning" algorithm is a special exception
to it, and learns practically noth ing. We compare our model to
pre-established and newly conjured baselines, and plot the trend for
aver age number of moves to solve the puzzle as compared to the model
complexity in 昀椀gure 1.

5. Conclusions

As we can see our proposed solution outperforms (barely, if at all) a
random word generator, and our one friend who does not speak English,
and was quite reluctant to play this game in the 昀椀rst place.

Building on our main objective to create a model 43

{width="3.1510553368328957in"
height="2.3829582239720035in"}

Figure 1: Performances of our model as compared to baselines.

as complex as possible, we believe any simple task can be made as
convoluted as desired if you're not bound by the unforgiving chains of
evaluation met rics. Sky being the limit for the number of param eters
that we could've trained for this task, unfor tunately, the authors of
this paper could only sit in front of a laptop screen for 18 hours a
day (the other 6 being reserved for a smaller screen, and sleep being
designed for the weak).

6. Acknowledgements

We would like to thank our non-English-speaking friend who was dragged
into this through no fault of their own, and express our gratitude for
not cutting us o昀昀, and also to the creators of a昀昀ordable GPUs
(such as Nvdia's 3090 Ti & Titan V) without which this abomination
would have never seen the light of day, and probably rightly so.

7. References

[1] The New York Times Wordle Game, 2022. [On line]. Available:
https://www.nytimes.com/games/ wordle/index.html

[2] J. Olson, Optimal Wordle Solutions.
https://jonathanolson.net/experiments/optimal wordle-solutions, 2022.

[3] G. Sanderson, "Solving Wordle with Information Theory", 2022.
[Online]. Available: https://www. youtube.com/watch?v=v68zYyaEmEA

[4] This brilliant tweet by George Toderici which we took very
literally, 2022. [Online]. Available: https://bit.ly/3v6zud5

[5] J. Devlin, M.-W. Chang, K. Lee, and K. Toutanova, "BERT:
Pre-training of deep bidirectional trans formers for language
understanding," in Proceedings of the 2019 Conference of the North
American Chapter of the Association for Computational Lin guistics:
Human Language Technologies, Volume

1 (Long and Short Papers). Minneapolis, Min nesota: Association for
Computational Linguistics, Jun. 2019, pp. 4171--4186. [Online].
Available: https://aclanthology.org/N19-1423

[6] "Bill gates denies making 1981 comment about limits of ram
needs, despite popular legend," 1981. [Online]. Available:
https://bit.ly/3wXxOVM

44

Systems

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

Natalia Posting and Katie Wolfe

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

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

Maximilian Weiherer and Bernhard Egger

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

Peter Kos

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

45

Edward, edMUnD & Edwin: Line-Based Text

10

Editing for the 21^st Century

NATALIA POSTING editor drone

equa.space

KATIE WOLFE

innocent bystander katie.host

Abstract

In this paper we demonstrate how the standard text editor, ed(1), can
be

adapted into an IRC-based collaborative environment, paralleling
modern

IDEs such as Google Docs.

1 Introduction

Despite our best efforts, the human race still finds itself needing to
edit computer files. The history of computer text editing began with
line editors. Bound to the restric tion of paper teletypes, such
editors worked with entire lines at a time and, due to the low speed of
teletypes of the time, only sent output when explicitly requested.

Ed(1) is such an editor. Originally designed for the Unix operating
system in 1969, ed(1)'s influence runs deep in Unix tools such as grep
and can still be traced in modern text editors such as ex. An
annotated example of an ed(1) session follows.

$ ed Start ed(1).

→ e message.txt Open message.txt into the editing buffer. ← 59 The
number of bytes read. → 1,$p Print from the first line to the final
line. ← [03] DAYS

← SINCE LAST TELETYPE INJURY

→ 1s/3/0/p On line 1, replace 3 with 0, printing the fixed line. ←
[00] DAYS

→ $a Enter input mode, appending after the last line. →

→ note: rage-induced accidents not counted

→ quit Oops!

→ arghahjvnfsjv

→ . Exit input mode.

→ quit Try to quit.

← ? (Invalid command suffix.) → q oh yeah

← ? (Warning: buffer modified.) → q Quit without saving.

Figure 1: A simple ed(1) session. Lines are first addressed, either by
themselves or as ranges; then operations are applied to them; finally,
a suffix such as p may be specified, causing ed(1) to print the line
it operated on. Ed(1) is relatively quiet about all this: even its
error messages just tell you that you goofed it.

46

Ed(1) remains powerful. Despite better judgement, the unit of the line
serves as the foundation for almost every software engineering
toolset, from the syntax of modern programming languages to the
diff-tracking and conflict-resolution features of version control
systems like Git. Code can be navigated in ed(1) using the in
dentation of source files as a guide to their structure; complex
operations can be automated using regular ex pressions; and
integration with language servers, lin ters, and build systems can be
achieved with the shell command, !. But despite its enduring editing
prowess, ed(1) is ultimately limited by the design of its original
environment. Unix was a time-sharing operating sys tem: users would
pay a fixed fee for rights to use the machine's limited facilities
during an allotted calendar period. Real-time collaboration was
impossible.

Google Docs is an online, collaborative visual editor first released in
2006. Owing to the later invention of the color television (CRT), it
allows for rich, colorful document formatting and provides live feedback
the in stant a character is typed. Furthermore, Docs allows for live
collaboration and feedback between multiple users editing the same
document. Its real-time iteration and collaboration capabilities have
become a standard for enterprise software projects and landed Docs an
easy position as the world's foremost IDE. Google has also supported
being evil since 2018; while ed(1) supports basic evil, it is ultimately
limited in scope to the design of its original environment.

Despite these limitations, we believe ed(1)'s line based model can be
adapted to match and even exceed the performance and feature set of
modern IDEs such as Docs. In Section 2, we introduce our barebones pro
totype editor used to develop our later designs via the Internet Relay
Chat and research editor interaction. In Section 3, we describe a failed
but insightful initial at tempt at modeling shared text files with a
graph-like structure. In Section 4, we detail our final shared edit ing
model, and in Section 5, we compare it to Docs and other modern
development environments. We conclude in Section 6 with the potential of
future work.

1

but can still mirror the popular technique of pair pro gramming. Since
he only takes input when explicitly ad dressed, communication can be
done out-of-band within the editor channel itself, allowing text-only
collaboration without management of a separate chat window. This
mechanism provides the foundation for an experimental code review
technique in which code is reviewed live while being written. This
provides a more theatrical review process and frees developers from
having to read their own code later.

Overall, IRC is well-suited to interfacing with line based programs.
Special characters like the tab com plicate input and display for most
chat clients, but the IRC protocol itself has no problem handling
them. Plac ing ed(1) in a networked environment also amplifies its
previously bounded evil capabilities: with a cleverly crafted
commmand, any user can cause Edward to send an exponentially
increasing number of messages to any unsuspecting chat room.

3 edMUnD

Traditionally, ed(1)'s central data structure took the form of a
doubly linked list of lines. This system models inser tions and
deletions well for a single user but has difficulty in the recovery of
edit conflicts. Docs works well with a single shared file and
per-character feedback, but an editor handling entire lines at a time
is more likely to run into conflict. Our first approach involved a
simple varia tion on the linked list: every line linked to its
adjacent lines, but the links were not required to be bidirectional.

edMUnD *(*Editor-Drawn Multi-User Non-Euclidean Dungeon) was our
implementation of this model. It had two commands in addition to those
of ed(1). One would create a "branch," copying a block of code and
creating unidirectional links back to its context in the main text
file. Once ready to merge again, the second command would patch the
links to point to the new text, "detaching" whatever was previously in
its place.

function main ()

2 Edward

print(nice_message) print(EVIL_message) 2

Edward is basically like this little guy. He dutifully sends 3

lines back and forth between an ed(1) process and any number of IRC
channels. As a direct mirror of ed(1), he doesn't distinguish between
users or implement multi buffer logic---every channel has one shared
"head" con trolled by all participants at once in a consensus model.

\<natalia> edward: a

\<katie> edward: .

Figure 2: An example Edward session.

Edward's model limits the possibilities of collaboration

end

Figure 3: A new branch of code lurks, undetected.

Being able to continue editing in a detached state was useful: a user
could work without interruption on code deleted by another, or save
breaking changes in a hidden branch until later. It was also immensely
evil: you could hide an ancient curse or a bad word and nobody would
ever know.

47

These two basic operations provided more complex code layout as well.
Simple combinations led to non trivial results:

contents or moving them around. This has the nice effect of retaining
the positions of "heads" (representations of users in a channel),
allowing text editing to go unin terrupted even if users remove or
rearrange text in the

1 2 3 4

A

B B∗ C C∗ D

middle of an operation.

4.2 Line numbering

The classic ed(1) provides one important mechanism for preventing
destructive mistakes: line numbering. A cowardly user might wish to
verify a range (e.g. ?^[fe]?,//) is correct before deleting its
contents; to

Figure 4: First, a new branch is created off of the middle two lines.
Then only the latter line is merged back into the original layout. The
result is a graph with no canonical rep resentation: the text file
reads completely differently depending on if it is viewed from the
first line or the last.

The development of non-Euclidean text files showed ex citing promise
in the field of evil (think of inescapable textual labyrinths) as well
as the field of interactive fiction (think of inescapable textual
labyrinths). Unfor tunately, the non-linearity of the files ultimately
compli cated PDF export, so the project was scrapped.

4 Edwin

Our final model, Edwin, uses a hybrid technique, combin ing the
utility of edMUnD's branching mechanism and the stability of linear
editing buffers. Inner details of the model and challenges faced in
Edwin's development follow.

4.1 Buffers & lines

Edwin's primary organizational structure is the buffer. Each buffer is
a self-consistent doubly linked list of lines. New buffers are created
during branching operations, either explicitly via the branch command
or implicitly by other editor operations (e.g. the deletion of a range
of lines). Edwin has a trick up its sleeve that lets it paral lel the
smooth branching of edMUnD: every buffer con tains links to the lines
that were before and after it prior to branching. These links can be
addressed directly or used in commands: the patch command, for
example, attempts to place a buffer back into the original con text of
its old buffer. The explicit formalization of these boundaries saves
the headache of accidentally creating paradoxical structures. Commands
involving these patch links fail when the context is destoyed (i.e. if
the lines around the original content are moved into different buffers
and no longer have a path between them).

Lines in Edwin have unique identities; wherever pos sible, operations
will retain them when modifying their

check it, they can first use the n command to view the contents and
line numbers of the addressed range, then use the line numbers
directly to safely perform the oper ation. But in a collaborative
environment, line numbers can silently change in between the two
commands, lead ing to results as disastrous as getting the address
wrong the first time. Edwin solves this by introducing two spe cial
line markers for every head called \< and >, which always point to
the first and last lines addressed in the previous command. Using
\'\<,\'> instead of line num bers, a user can address exactly the
same lines as before.

4.3 History

Ed(1) implements one layer of editing history. Users can undo the last
edit done and no more. Modern IDEs fea ture unbounded history and
occasionally more complex time-traveling branch systems. Edwin
compromises by implementing zero layers of history. Traditional undo
methods were found to be complicated by the multitude of simultaneous
edits in different locations. Rather, the function of an edit history
is served flexibly by the mes sage archive of the IRC channel itself,
containing both edits and out-of-band annotations.

4.4 Extensibility

As part of a full Unix environment, ed(1) provides fea tures external
to the editor via a command which pro cesses text through the shell.
This is powerful in a Unix context but generally disconnected from the
network ing system Edwin resides in; instead, the recommended method
for scripting Edwin takes place over IRC itself. Chat bots can
interface with Edwin directly, inspecting data and modifying as
appropriate. Given access to the editor command interface, IRC-based
bots have more power than traditional shell scripts, as they can
manipu late not only text but the state of the entire editor.

4.5 Incompleteness

The primary barrier to the use and analysis of Edwin is that I didn't
finish implementing it. In order to continue research, we construct a
model for what Edwin would look like and use a technique known as
"guessing" to

48

generate precise thought experimental data. We avoid bias introduced
by the variance in data collection by ap plying similar techniques to
all test environments used in the editor's evaluation.

5 Comparison with other IDEs

How does Edwin fare against other development tools? We evaluate a set
of editor environments according to four criteria: overall efficiency,
appearance, synergy, and evil. As a baseline for Docs and Edwin, our
primary con tenders, we evaluate two classic editor environments: Vim
over a paper teletype and Microsoft Paint over VNC.

5.1 Efficiency

While basic writing operations are simple in Paint, mov ing and
replacing text requires manual intervention and is prone to failure
due to Paint's relatively basic address ing system. All of these
complications are amplified by the time required for a full screen
refresh. Paint's in eptitude is only second to that of Vim, in which
every keystroke sends dozens of mangled control characters to the
poor, poor teletype output.

Docs does its job great: writing text has a noticeable network delay,
but visual changes render fast on individ ual client machines. It
supports a wide range of useful operations and has no problem
restructuring large files. Edwin performs comparably if slightly
better: feedback is only sent when explicitly requested, and moving
from a granular editing system to a line-based one permits the
correction of quick mistakes without network delays. Edwin's range of
operations is similar to that of Docs, but is better inclined to
complex organization with its native marks, buffers, and regexen.

5.2 Appearance

The appearance of code written in Paint is entirely dic tated by its
author. Paint has 24-bit color capability; its main limiting factor is
the ability of the user to not just handwrite but handwrite with a
mouse over VNC. Vim is somehow worse.

Docs has native rich text support, which permits users to highlight
their code's syntax however appro priate. However, its font selection
is limited: only the Google Fonts repository is available. Edwin
supports rich text by means of IRC's formatting control characters and
an unlimited range of fonts provided by chat clients.

5.3 Synergy

There is nothing more synergetic than a shared white board. Paint is
only limited by its single shared drawing cursor. Vim has no synergy
at all---even if it were com prehensible, everyone'd have to crowd
over the teletype. Might as well just draw on the paper.

Docs is at the forefront of channeling synergy through text: it
supports the core components of group collaboration, with live
editing, comment threads, and edit proposals. But it fails to recover
synergy when it is lost---for example, when two simultaneous edits
come into conflict, competing with one another for space in the
finished document. Edwin supports all of Docs' fea tures through a
unified chat interface, and its branching mechanism allows for
peaceful resolution of conflicting simultaneous work.

5.4 Evil

Paint supports evil: you can draw crude pictures wher ever you want
and, since its undo stack is limited, force your collaborators to
either suffer through the draw ings or completely erase whatever they
intersected. Vim doesn't seem to support evil: certain Vim reimplemen
tations in other environments are rumored to include it but were not
considered for evaluation.

Google was initially reluctant to support being evil but faced
pressure to allow large enterprises to use the quickly growing Docs;
it eventually removed its evil restrictions in 2018. While now seeing
broad use in evil, the editing interface is anything but: any
malicious changes can be found and undone with its thorough history
tracker, and drawing unsightly pictures in reg ular text documents is
tedious. Edwin has supported evil since its conception, in both its
use and its internal operation. It is easy to not only write swear
words but irreparably overwrite entire documents, exponentially
increase the editor's used memory, and cause the bot to flood any IRC
channel naïve enough to associate with it.

6 Future work

_{I sure hope it d}7 Future work

It would be nice if the editor existed. Ad

ditionally, Edwin's realization lacks a sys

tem for traditional, long-term collabora

tion. One potential model would use

email: users could send files containing

Edwin commands to a project maintainer,

who would apply the commands to a cen

tral repository.

References

[1] IEEE and The Open Group. 2018. ed -- edit text. The Open Base
Specifications Issue 7, 2018 edition.
https://pubs.opengroup.org/onlinepubs/ 9699919799/utilities/ed.html

w

quit

q

ˆC

49

{width="2.1986668853893265in"
height="1.5396248906386703in"}

{width="2.201486220472441in"
height="1.5396248906386703in"}

50

{width="2.197694663167104in"
height="1.5396248906386703in"}

51

11

A Free Computer Vision Lesson for Car Manufacturers or

It is Time to Retire the Erlkonig ¨

Maximilian Weiherer Bernhard Egger

Fantastic-Amazing-University Erlangen-Nurnberg (FAU) ¨

maximilian.weiherer@fau.de

bernhard.egger@fau.de

Oh no -- we can recover very detailed 3D shape from Erlkonig
photographs. How could this have happened? And even worse, the ¨
reconstruction is best in the parts where there is a pattern. Well, we
guess someone didn't know about the basics of computer vision.

Abstract

In award winning prior work [1], we identified the inability of

autonomous cars to honk as the key reason that they are not broadly

deployed on our streets. In this work [2], however, we suggest that

the core reason is the lack of most basic computer vision knowledge

of car manufacturers. To hide their most fancy new cars they put a

special camouflage pattern on their so called Erlkonig ¨ prototypes.

The pattern is designed to trick our perception; at the same time it

enables computer vision systems to perfectly recover the 3D shape

of the prototype -- even better than without the pattern as we show

in this paper. How could we expect a prototype car that already

demonstrates a lack of computer vision knowledge to ever evolve

into an autonomous vehicle?

1. Introduction

We could now tell you the whole story of the Erlkonig and Dazzle ¨
Camouflage patterns, but that is way to much work. The inter ested
reader (if any) is kindly asked to read the relevant litera ture here:
https://en.wikipedia.org/wiki/Dazzle_ camouflage. The relevant portion
is that the pattern is de signed to make it hard to estimate the range,
speed and head ing of a ship and it might also make it harder to
estimate the type of the ship, see Figure 1. And this is all cool and
every thing, but over 100 years have passed since the pattern was de
scribed by Norman Wilkinson during the last pandemic. This does not hold
back car manufacturers to paint their dinosaur eating machines (also the
sun eating counterparts) with patterns moti vated by this idea and brag
about it (https://www.bmw.com/ de/automotive-life/erlkoenig-auto.html).
The car manufacturers might try to hide the shape of their cars, and it
might work pretty well when it comes to the human eye. It might even
hold some cameras back from using their automatic focus. But all of that
only holds for a single view! The moment we have multiple

Figure 1. Damn hard to estimate the heading of the boat on the left
with the Dazzle camouflage pattern, right? Source: Encyclopædia
Britannica, 1922 / Wikipedia.

viewpoints -- tadaaa -- we can use the whole ballpark of computer
vision algorithms and even algorithms from the stone-age (all his
toric works before 2022) of computer vision lead to an almost perfect
3D reconstruction.

To summarize, in this paper, we impressively show that the 3D shape of
a car covered with camouflage patterns (i.e., an Erlkonig) ¨ can be
very well reconstructed just from a set of ordinary pho tographs,
taken from different perspectives. To make the embar rassment for car
manufacturers perfect, we demonstrate that the 3D reconstruction of
the same car without patterns is much worse. That's bitter.

1.1 Related Work

Besides a Twitter thread with various researchers almost scooping us
there is no relevant prior work (see Figure 2).

52

Figure 2. Almost scooped: https://twitter.com/
jaakkolehtinen/status/1481269802681393153.

2. Methods

Given a set of photographs taken from different perspectives, we used
BASIC photogrammetry for 3D reconstruction, see e.g.
https://en.wikipedia.org/wiki/BASIC. The choice fell on BASIC because
we are absolute beginners when it comes to programming (and all this
computer stuff in general). Following common practice and due to the
lack of knowledge, we do not re veal all the details about our method.
But we want to sprinkle in some unnecessary details like for example
the parameters

ξ and ζ (1)

that are not introduced but very critical and car-fully set to the
value 5. As far as we understand, a key step in our pipeline involves
the solution of the Perspective-n-Point (P-NP) problem. Having a
solution of the P-NP problem at hand and exploiting the fact that P =
NP¹, obtaining the final 3D reconstruction in form of a triangular
surface mesh is dead easy and no more information is needed to
re-implement this.

3. Experiments and Results

We took 32 photos of an Erlkonig ¨²and applied the method de scribed
earlier to obtain a 3D reconstruction. About the same pro cedure was
used to reconstruct the same car without a pattern. Ev

¹ A proof is provided in the Appendix. In essence, however, the
ingenuity in our proof was to use the well-known fact that e^iπ − 1 = 0
\<MW: Damn, just realized we've been using this formula wrong all the
time. BE: Relax. No one will notice.>. Kudos to Leo Euler.
\@ClayInstitute: We expect the money no later than May 1^st, 2022. We
need it. Desperately.

² Due to an ongoing legal dispute, we unfortunately cannot share any
details about the car. Please refrain from e-mail inquiries. Authors
may not have access to the internet for an unknown period of time.

Figure 3. See, pattern leads to awesome reconstruction whilst no
pattern no good. Please print in grayscale on dead trees for better
visibility of details.

erything went perfect on the very first try (yes, no testing or
training or what else was needed) and our method produced spectacular
re sults, see Figure 3. As expected by computer vision experts, the
reconstruction of the Erlkonig is at least a million (10 ¨⁶) times
bet ter than the reconstruction obtained from the same car without a
pattern. These results are so good that we don't even need a quan
titative evaluation, right?

4. Limitations

Car manufacturers will say we are missing something here and things
are more complex. Don't believe them. They also say burn ing dinosaurs
is cool and that we will have autonomous cars next year! We win, they
loose -- it's that easy.

5. Conclusion

To summarize, the pattern might be able to cause a collision with a
Tesla, but for any other purpose it is beyond repair: the Erlkonig is
¨ asking for retirement -- loud and clear. Just like this Tim Brady!

Our future mission should be clear and obvious: reveal the shape of
all the things in this world covered with a camouflage pattern (or
something that looks like a camouflage pattern; doesn't matter, our
method will tackle it anyway because it generalizes). This immediately
leads to the following research questions: what the heck is really
hiding under a military uniform? And, can we trust QR codes? Stay
tuned and make sure to follow us on Twitter.

Finally, if you want to learn more about computer vision: there might
be a cool lecture at your favorite astonishing university (FAU). If
you are a car manufacturer: we have some ideas to help you out of your
misery and are looking for funding.

References

[1] B. Egger and M. Siegel. Honkfast, prehonk, honkback,
prehonkback, hers, adhonk and ahc: the missing keys for autonomous
driving. SIG BOVIK, 2020.

[2] M. Weiherer and B. Egger. A free computer vision lesson for car
manufacturers or it is time to retire the erlkonig. ¨ SIGBOVIK (under
careful review by very talented, outstanding reviewers), 2022.

53

12

Abstract

Redundant Coupling

Peter Kos

Rochester Institute of Technology plk5062@rit.edu

2.1 Definitions

In the field of software engineering, researchers have coined the terms
"cohesion" and "coupling" to describe the structure and interaction
between classes in an object-oriented environment [6]. The traditional
wisdom is to use low coupling and high cohesion to reduce side eûects
while making isolated changes in code. In this paper, we present an
alternative methodology: redun dant coupling. In redundant coupling,
coupling between classes is maximized in order to create the strongest
pos sible foundation in the architecture. This has been shown to provide
a 45% increase in unit test stability (in flaky environments), 71%
increase in developer confidence, and a 14% increase in my personal
happiness since my second wife left me.

1 Introduction

Coupling and cohesion are core ideas in software archi tecture. They are
a little ambiguous too, as modern com puter science education does not
usually address the is sues that can (allegedly) arise from high
coupling and low cohesion.

2 Theory

Coupling is introduced as a way to "[minimize] the paths along which
changes and errors can propagate into other parts of the system, thus
eliminating disastrous 'ripple' eûects" [6, p. 233]. However, this
operates on two false assumptions:

1. Individual change's eûects on the whole system need to be
minimized

2. Errors can propagate into other parts of the system

Changing a piece of code involves a deep insight into its function.
(One can imagine careless changes, but these are part of the natural
software development lifecycle). ...

Errors, too, are by definition, a symptom of the sys tem. The solution
for an error may be in an individual class, or across multiple classes,
yet the codebase as a whole suûers.

Definition 1. Equivalent access is a reciprocal access between two
classes A and B*, such that the following holds:*

• Let ³ be a field of A*,*

• Let ´ be a field of B*,*

• Let A(³) be an access of field ³*,*

• Let A(´) be an access of field ´

An access is equivalent if and only if

(A(³)) = (A(´))

^. • For the fields ³ = String and ´ = String, these would be an
equivalent access, as the access/set complexity of a string¹is O(1).

• For the fields ³ = HashMap\<T> and ´ = HashMap\<T>, the same is
true, as here, the complexity of any hash map operation is O(n).

• For the fields ³ = String and ´ = HashMap\<T>, A(³) = O(1), and
A(´) = O(n). (A HashMap, with a suûciently large load factor, may need
to iterate through all of its elements to get a specified ith
element.) Therefore, in this case, class A and B would not have
equivalent access between fields ³ and ´.

Definition 2. The coupling factor » is defined to be the number of
equivalent accesses between two classes A and B*.*

»=1 A B

»=2 A B

»=3 A B

¹In most programming languages.

1

54

2.2 » coupling factor

We define two classes A and B to have one-string cou pling if they are
bidirectionally coupled in one mecha nism, whether that be:

• Reciprocal method-calling, or

• Equivalent access.

To see how redundant coupling increases the foun dational stability of
a class, we take to the example of auxiliary classes.

Auxiliary classes are defined as classes that we do not anlayze at
the present moment, that are not coupled to any other class. The load
factor between two classes A and B, e.g., »_AB, is only defined with
respect to A and B. (Later on, we define a process called promotion
that addresses how we can move between classes of focus).

Say that we have an auxiliary class ³ that is coupled to A, and the
same with ´ for B.

^³ A B ´

We can see that the load factor between each class is as follows:

^³ A B ´

»_aux|A=1 »=1 »_aux|B=1

The auxiliary coupling factor, _aux, is equal to the cou pling factor
of our two classes of interest (»). We define this to be a point of
Fowler Equlibrium.

Definition 3. A Fowler Equilibrium is present be tween two classes
A and B such that

»_AB = »_aux|A = »_aux|B

(where »_AB is the coupling factor between A and B, and »_aux|A is
the coupling factor between the auxiliary classes of A.)

The total auxiliary coupling factor is represented as such:

!

» = »_aux|A

³*A

However, once we add two additional auxiliary classes on each side, we
run into an issue:

2

Here, the auxiliary coupling factors are not at equi librium with the
interior coupling between our classes of interest. This ia a
misbalanced system, and this is fundamental issue this paper serves to
address.

3 Limitations

We acknowledge²that it is "unlikely, for financial and structural
reasons" [5] to develop a model that can ac count for coupling in
non-OOP paradigms.

Additionally, it is not known how this would aûect projects in
multiple languages. Mayer and Schroeder de fine an XLL approach [3,
p. 97], where developers man ually specify links between abstract
concepts present in each language. In this system, one could couple
the ar tifacts themselves, but this is more akin to coupling spe cific
fields within a class -- not the class overall.

4 Testing Methodology

Tests were originally written using a source-compiled ver sion of
JUnit 2, until the inferiority of this solution was realized through
several cognitive behavioral therapy ses sions.

Instead, we pivoted to use Rust 1.58.0-nightly. Rust [2] provides a
safe, fast environment without garbage collection, which allowed us to
mitigate any cross-bag insect contamination [4].

One potential issue is a common misconception that Rust does not
provide an OO environment. We assert that it is possible to represent
an OO-pseudostructure within Rust, without resorting to an inferior
language. (See Appendix A.)

5 Results

As shown previously [1], we found a few notable improve ments in
codebases that used redundant coupling over the traditional low
coupling / high cohesion model:

1. 45% increase in unit test stability

2. 71% increase in developer confidence

3. 38% reduction in alimony paperwork

Unit test stability occurred a natural consequence of allowing changes
to propagate throughout the codebase. Intermittent tests can be caused
by any number of bugs,

³₀ ³₁

´₀

´₁

»_aux|A=2

A B

»=1

»_aux|B=2

and are usually localized to one or two classes. Through redundant
coupling, the codebase is unilaterally influ enced by these issues,
which allow the system overall to behave more reliably.

Developer confidence was also observed to increase markedly.

²i.e., forced to concede

55

6 Conclusion

Todo.

7 Appendix A

// Some sample code we wrote as part of a demonstrative paper on Rust
coupling . // We are not sure if it compiles .

struct User {

var first_name : & str ,

var last_name : & str ,

var age : u8

}

impl User {

fn get_full_name (& self ) -> & str {

first_name + last_name

}

fn have_birthday (& mut self ) {

self . age += 1;

}

}

struct Login {

var cur_user : User

}

impl Login {

fn login (& mut self ) {

todo !() ;

}

fn get_full_name () -> & str {

cur_user . get_full_name ()

}

}

Listing 1: Example of an OO structure in Rust, with coupling

References

[1] Peter Kos. Redundant coupling. Association for Computational
Heresy, 2022.

[2] Nicholas D. Matsakis and Felix S. Klock. The rust language. In
Proceedings of the 2014 ACM SIGAda Annual Conference on High
Integrity Language Tech nology, HILT '14, page 103104, New York, NY,
USA, 2014. Association for Computing Machinery.

[3] Philip Mayer and Andreas Schroeder. Cross-language code analysis
and refactoring. In 2012 IEEE 12^th International Working Conference
on Source Code Analysis and Manipulation, pages 94--103, 2012.

[4] Sulochana Paudyal, George P Opit, Frank H Arthur, Georgina V
Bingham, Mark E Payton, Sandipa G Gautam, and Bruce Noden.
Eûectiveness of the zerofly©R storage bag fabric against
stored-product insects. Journal of stored products research, 73:87--
97, 2017.

3

[5] Michael L. Scott. Cover letter for dean of the golisano college
of computing and information sciences. 2022.

[6] W. P. Stevens, G. J. Myers, and L. L. Constantine. Structured
design. IBM Systems Journal, 38(2):231-- 256, 1999. Copyright -
Copyright International Busi ness Machines Corporation 1999; Last
updated - 2021-09-10; CODEN - IBMSA7.

56

Theory

13 Destructive Logic

Runming Li

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

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

Gabriel Chuang

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

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

16 A Patriotic Analysis of Programming Paradigms Jacob Weiner

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

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

per, Orange

57

13

Destructive Logic

Runming Li

runmingl@andrew.cmu.edu

Carnegie Mellon University

March 19, 2022

Abstract

Intuitionistic logic, also know as constructive logic, is considered
the true logic of computer science for the reason that it contains
actual computational content. We propose Destructive logic, a
supplement of constructive logic, with the goal of proving things that
are not provable in constructive logic. Destructive logic, suggested
by its very name, proves things by destroying, rather than
construction. We study its properties and applications in this paper.

0 Introduction⁰

Constructive logic was historically proposed in response to classical
logic. Everything that is provable in constructive logic is provable
in classical logic, but not vice versa (e.g. law of excluded middle).
In this sense, constructive logic is a more restricted, more precise
logic than classical logic. It was later found out that constructive
logic has roots in type theory and programming language theory based
on Curry-Howard Isomorphism¹. Constructive logic is so well-studied
that many major universities teach it. Among them one of the
classical² courses is 15-317 Constructive Logic at Carnegie Mellon
University.

Duality exists everywhere in logic: conjunction and disjunction,
universal and existential, left and right, up and down, you and me. A
natural question to ask is: what is the dual of constructive logic? An
unsurprising answer from etymology suggests destructive logic. Indeed
this is the case: while constructive logic proves things by providing
a clear algorithm that constructs the object in question, destructive
logic proves things by destroying things it wants to prove. Of course,
unreasonable destruction is considered psychopath, so we need to
develop a clear justi昀椀cation for every destruction. For the purpose
of destructive logic, introduce
�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}, named Destro (they/them/theirs), a
rational T-rex whose main purpose of life is to destroy things they do
not like.

⁰It is well-known that a good logician starts counting from 0.

¹Also know as Propositions as types principle. Also know as
Programs as proofs principle. Also know as
Brouwer-Heyting-Kolmogorov interpretation. Also know as
Realizability interpretation. Also know as Curry Howard
Correspondence. It is worth noting that Curry-Howard Isomorphism is
in no sense an isomorphism. Just like hotdog is in no sense a dog.

²Classical course, in a constructive sense.

58

1 Extending Natural Deduction

Gentzen[2] proposed natural deduction system to formulate
intuitionistic logic. We extend his natural deduction system in
support of our destructive logic.

1.1 Conjunction

In constructive logic, conjunction can be summarized by the following
rules. _{Γ ⊢ �㔴 ∧ �㔵 true ∧�㔼} [Γ ⊢ �㔴 ∧ �㔵
true]{.underline}

[Γ ⊢ �㔴 true Γ ⊢ �㔵 true]{.underline}

_{Γ ⊢ �㔴 true}∧�㔸₁[Γ ⊢ �㔴 ∧ �㔵 true]{.underline}
_{Γ ⊢ �㔵 true}∧�㔸₂

Destro feels uneasy about this kind of setup: everything is too
deterministic, and they want to attack propositions they do not like.
Admittedly Destro's personal taste is too hard to predict, so we have
the following possibilities.

[Γ ⊢ �㔴 true Γ ⊢ �㔵 true]{.underline}

_{Γ ⊢ �㺖 ∧ �㔵 true}∧�㔼₁[Γ ⊢ �㔴 true Γ ⊢ �㔵
true]{.underline}
{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}

_{Γ ⊢ �㔴 ∧ �㺖 true}∧�㔼₂

[Γ ⊢ �㺖 true Γ ⊢ �㔵 true]{.underline}
{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}

_{Γ ⊢ �㔴 ∧ �㔵 true}∧�㔼₃[Γ ⊢ �㔴 true Γ ⊢ �㺖
true]{.underline}

_{Γ ⊢ �㔴 ∧ �㔵 true}∧�㔼₄

_{Γ ⊢ �㺖 ∧ �㺖 true}∧�㔼₅[Γ ⊢ �㺖]{.underline}
{width="0.1661220472440945in"
height="0.1661220472440945in"}[true Γ ⊢ �㔵 true]{.underline}

[Γ ⊢ �㔴 true Γ ⊢ �㔵 true]{.underline}
{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}

_{Γ ⊢} {width="0.1661220472440945in"
height="0.1661220472440945in"}_{�㺖 ∧ �㔵 true}∧�㔼₆

Again, Destro's destruction is non-deterministic (at least humans
should never be able to learn a T-rex's personal opinion), so we would
not bother writing out all the possibilities in which they can attack
for the purpose of saving some space. Moreover, one day Destro is
tired of destructing propositions, so they start to destroy rules and
context and even turnstile.

[�㺖 ⊢ �㺖 true Γ�㺖�㺖 true]{.underline}
{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}

_{Γ ⊢ �㺖} {width="0.1661220472440945in"
height="0.1661220472440945in"}_{∧ �㺖}
{width="0.1661220472440945in"
height="0.1661220472440945in"}_true∧�㺖

1.2 Disjunction, Implication, Truth, and Falsity

Now one can simply
img{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖ine what
hap{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖en when we decide to put
�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}into other
con�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}ectives such as
disjunc{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖ion,
implic{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖tion, truth, and
falsi{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖y. In short, they just destroy
whatever they want.

2 Properties and Applications

2.1 Basic Theorems

We 昀椀rst prove some basic theorems of destructive logic to convince
the readers that indeed destructive logic is a real logic.

59

Theorem 1. Consistency: it is not the case that ⊥ true.

Proof. In Curry-Howard Isomorphism, ⊥ corresponds to 0 the empty
type. �㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}cannot resist destroying it because it
looks so much similar to their baby egg. Therefore, whenever the

prover is able to show ⊥ true, �㺖destroys it.
{width="0.1661220472440945in"
height="0.1661220472440945in"}

---

---

Theorem 2. Local completeness of conjunction: the elimination
rules of conjunction are not too weak.

Proof. Imagine a day when
�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}is too tired and they decide not to
destroy anything. Then for that day destructive logic downgrades to
constructive logic, in which local completeness

of conjunction holds.

---

---

Corollary 2.1. Local completeness of other connectives.

Proof. Copy and paste the proof of Theorem 2.

---

---

Theorem 3. Local
soundne{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖*s of conjunction: the elimination
rules of conjunction are not too strong.*

Proof. Local soundne�㺖s has been destroyed by �㺖.
{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}

---

---

Theorem 4. Global completeness and global soundness in
destructive logic.

Proof. The author has been destroyed by
{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖, and therefore leave the proof of
this theorem

to readers.

---

---

2.2 Curry-Howard Isomorphism

Behind every logic there is a type system, according to Curry-Howard
Isomorphism: con structive logic has simply typed lambda calculus,
classical logic has continuation, linear logic has linear type system,
second order logic has system F. It is only natural that destructive
logic also has a corresponding type system. For this purpose, we
propose �㔐-calculus³. We extend simply typed �㔆-calculus with the
following types and terms.

�㔏 ∶∶= ⋯ |�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}|�㔏 ^�㔏|unknown_destroy

�㕒 ∶∶= ⋯ |�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}|�㔐(�㕒, �㕒)|destro(�㕒)

The statics would be as followed.

Γ ⊢ {width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖 ∶
{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖
Γ{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖�㕒 ∶ unknown_destroy �㺖
{width="0.1661220472440945in"
height="0.1661220472440945in"}⊢ �㕒 ∶ unknown_destroy Γ ⊢
�㕒_{[1]{.underline}}∶ �㔏 Γ ⊢ �㕒_{[2]{.underline}}∶ �㔏

�㺖�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}�㕒 ∶ unknown_destroy
�㺖�㺖�㺖�㺖�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.1661220472440945in"
height="0.1661220472440945in"}

Γ ⊢ �㔐(�㕒₁, destro(�㕒₂)) ∶
�㔏^�㺖{width="0.11628499562554681in"
height="0.11628499562554681in"}

³The choice of greek letter �㔐 here is not arbitrary, but rather
forced. Type theorists have used up so many good greek letters: �㗼 is
for equivalence, �㗽 is for reduction, �㗾 is for substitutions, Π and
Σ are for dependent types, �㗿 and �㔊 are for Covid, to name a few.

60

In this calculus, when
{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖accidentally destroy something
strange (such as context or turn stile), we simply give it a universal
type of unknown_destroy. The essence is the �㔐 ex pression, where if
�㕒₁is the undestroyed expression and �㕒₂is its destroyed
equivalence, then �㔐(�㕒₁, destro(�㕒₂)) is the way to recover
the computational meaning of what
�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}destroyed. Then it follows naturally
that

⋅ ⊢ �㔐(�㔐(�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"},
destro(�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"})),
detsro(�㔐(�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"},
destro({width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖)))) ∶
�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}{width="0.11628499562554681in"
height="0.11628499562554681in"}^�㺖�㺖{width="8.306102362204724e-2in"
height="8.306102362204724e-2in"}

2.3 Application

We suggest that destructive logic and �㔐-calculus be used to analyze
randomized algorithms, since
{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖's destruction pattern is essentially
randomized.

3 Future Work

We urge the logic community to take destructive logic seriously and
put drastic amount of work in studying it. We further propose that
destructive logic be taught at major universities. For Carnegie Mellon
University, we propose to start a new course 15-407 Destructive Logic,
and place it in the Principles of Programming Languages Concentration
requirement. The choice of course number here is not arbitrary:
according to Chuang and Wu[1], in order for a course to be
considered a PL course, it has to have a Collatz number of 59. Indeed,
15407 has a Collatz number of 59 and should be considered as a PL
course. Moreover, every course with a 7 in the course number is a good
course (e.g. 15-317, 15-417, 98-317). It follows naturally that the
course mascot should be
{width="0.1661220472440945in"
height="0.1661220472440945in"}�㺖, named Destro.

References

[1] Brandon Wu Gabriel Chuang. "What Lothar Collatz Thinks of the
CMU Computer Science Curriculum". In: SIGBOVIK 2021 (2021).

[2] Gerhard Gentzen. "Untersuchungen über das logische Schließen.
II". In: Mathematische Zeitschrift 39.1 (1935), pp. 405--431. doi:
10.1007/bf01201363.

{width="5.909027777777778in"
height="1.657027559055118in"}This page has been destroyed by
�㺖{width="0.1661220472440945in"
height="0.1661220472440945in"}.

61

Making Graphs Really Hard to Say Out Loud

14

Graph Labelings with Non-Disjoint Vertex and Edge Sets and how they
can be used for encryption, poetry, and breaking mathematics

Gabriel Chuang (gtchuang@andrew.cmu.edu)

Carnegie Mellon University

Abstract--- Modern communication systems have greatly increased the ease
with which we can describe our ideas to others. In an effort to slow
this progress and hinder scientific advancement, we examine labelings of
graphs that reduce clarity by reusing edge labels for vertices. We bound
how much overlap can be achieved, show how such labelings are
cryptographically secure, and prove some theorems that suggest that all
of mathematics is broken. Finally, we present some applications to
poetry and propose a new naming convention for graphs based on these
labelings, which we hope will be widely adopted.

I. INTRODUCTION

In Chapter 1.1 of Diestel's widely-used textbook Graph Theory, a
graph is defined to be a pair of sets (E, V ) with E ¦ [V ]².
Diestel follows this up with the following note:

To avoid notational ambiguities, we shall always assume tacitly that V
∩ E = ∅.

Needless to say, this is very disappointing to fans of

These labelings may also be of interest to those seeking to keep their
graphs concealed from adversaries who can only communicate verbally.
We present a cryptographic protocol that is in fact secure against
all adversaries.

Finally (and of purely academic interest)¹, such labelings of graphs
often resemble rhyme schemes; we present several graphs whose edge
sets correspond to common rhyme schemes or famous poems, and propose
an alternative naming system based on poetic forms.

II. MOTIVATION

Consider the following graph, and a natural labeling of its vertices:

notational ambiguity. There are many settings where being notationally
ambiguous is beneficial, such as: • When brevity is of the essence (e.g.
when lecturing

$a$ A simple undirected graph G.

$b$ A "natural" labeling of G, with vertex set

V = {a, b, c, d, e}.

at a blackboard),

• When trying to sneak faulty proofs past reviewers, • When trying to
confuse students, and

• When trying to confuse yourself.

In this work, we will explore labelings of graphs in which we seek to
maximize the overlap between the labels of the vertex set V and edge set
E. (Note that we will continue to require that edges are two-element
subsets of the vertices). See Fig. 2 for an example of such a graph.
Note that that graph has an edge {a, b}, but also a vertex {a, b}!

Such labelings have many desirable attributes; most notably, graphs
represented in this way are extremely notationally ambiguous, which
can allow us to prove interesting theorems. They are also very hard to
say out loud, due to repetition in their vertex and edge sets.

Fig. 1: A simple undirected graph, and a natural labeling.

Unfortunately, this labeling is extremely boring: there is no overlap
between V and E! Instead, consider the following labeling:

Fig. 2: A much more interesting labeling of the graph. The vertex set
is V = {a, b, c, {a, b}, {b, c}}.

¹just like the rest of this paper, to be clear

62

We've managed to achieve an overlap of size 2: V ∩ E = {{a, b}, {b,
c}}. That is, there are two vertices that share a label with an edge.
Can we do better on this graph? As it turns out, we can:

Fig. 3: An overlap-maximal labeling of the graph. The vertex set is V
= {a, b, {a, b}, {b, {a, b}}, {b, {b, {a, b}}}}. In this case, three
of four edges share a label with a vertex.

This labeling of the graph is has many desirable properties. For
example, the verbalization is extremely ambiguous:

"Vertices: A, B, A, B, B, A, B, and B, B, A, B. Edges: A to B, B to A,
B, B to B, A, B, and A to B, B, A, B."²

Theorem 1. For any graph G = (V, E),

È(G) = min(|E|, |V | − 2).

In particular, since connected graphs have |E| ≥ |V | − 1,

Corollary 1. For a connected graph G = (V, E), È(G) = |V | − 2

The proof of Theorem 1 shows that min(|E|, |V |−2) is both an
upper and lower bound for È(G), using a partial order argument for the
upper bound and an explicit construction for the lower bound. To spare
you the gory details, the proof has been relegated to Appendix A.

IV. OVERLAP RATIO AND PRETTY PICTURES In this section, we will show
some examples of maximum-overlap labelings of a few common classes of
graphs, and discuss the overlap ratio induced by those labelings.⁴

A. Complete graphs K_n

K_n hasⁿ₂ edges. Theorem 1 implies that

In general, it is not obvious how much overlap can be

₌2(n − 2)

₁

achieved for arbitrary graphs. Fig. 3 achieves overlap

Ä(K_{n) =}È(K_n)

_{n(n − 1)}= Θ

.

n

n

2

on 3 of 4 edges; can one do better? What classes of

graphs enable maximum overlap?

A central point of this paper will be to carefully define such labelings
and to show upper and lower bounds on how much overlap can be achieved.

III. DEFINITIONS AND CENTRAL CLAIM

Definition 1 (Overlap number). For a graph G = (V, E), let the
overlap number È(G) be the maximum size of E ∩ V over all possible
labelings L of G*, i.e., the maximum number of edges that can share
a name with a vertex (or vice versa). That is,*

È(G) = max

_{L:V →U}|L(E) ∩ L(V )|.

Definition 2 (Overlap ratio). The overlap ratio Ä(G) of a graph G
= (V, E) is defined to be

_{Ä(G) =}È(G)

|E|

In the example graph of Fig. 3, È(G) = 3 and Ä(G) = ³₄.³

²We could've done even better by naming the vertices "and" and "to"
instead of A and B.

³In the spirit of being notationally ambiguous, we will abuse
notation and use ρ(G) for non-maximal labelings as well.

Maximum-overlap labelings of K₅ and K₇ are shown in Fig. 4.

Fig. 4: Overlap-maximal labelings for K₅ and K₇. Note that very
few edges are reused for vertex labels.

The edge set for a max-overlap labeling of K₇ can be found in
Appendix B.

⁴More importantly, we will have many colorful figures, to maximize
appeal to children, advertisers, and color theory gremlins.

63

B. Cycles C_n

C_n has n edges. Theorem 1 implies that _n=n − 2

Here are two theorems, both of which are true: Theorem 2. G \ {{a,
b}} is 3-colorable.

Ä(K_{n) =}È(C_n)

_{n= 1 −}²_n∼ 1.

Proof: A 3-coloring is shown in Fig. 6b.

An overlap-maximal labeling of C_n is shown in Fig. 5

Fig. 5: Overlap-maximal labeling for C_n. Nearly every edge label is
reused.

V. NOTATIONAL AMBIGUITY ENABLES CHAOS

Now that we have our framework for labeling graphs, we will,
naturally, attempt to prove some theorems.

A. Graph coloring

Let G be the graph shown below in Fig. 6a.

$a$ A nice, well behaved graph G on 5

vertices. {a, b} is highlighted in orange.

$b$ G \ {{a, b}} © G \ {{a, b}}

Fig. 6: Our graph G, and the subgraph G \ {{a, b}}.

Theorem 3. G \ {{a, b}} is NOT 3-colorable.

Proof: G \ {{a, b}} is the complete graph K₄, as shown in Fig.
6c, and K₄ is not 3-colorable. Obviously, this is somewhat
problematic. We might be tempted to claim that k-colorability is in
fact either poorly defined or undecidable. However, complexity
theorists have put a lot of work into proving that 3COL is NP-complete
and thus in NP, which, by necessity, means that it is decidable.

In fact, simple extensions of Theorem 2 and Theorem 3 show that

Ç(G \ {{a, b}}) = 3 and Ç(G \ {{a, b}}) = 4,

where Ç(G) is the chromatic number of G (i.e., the minimum number of
colors needed to color G). We are forced to conclude that 3 = 4, and
that in fact 0 = 1.

B. Adjacency

One might be tempted to cut out the notion of coloring altogether, in
the hope that the rest of graph theory is salvageable. Unfortunately,
even the notion of adjacency yields contradiction. Let H be this
graph:

Fig. 7: Another perfectly well-behaved graph H.

Theorem 4. In H*,* {{a, {a, b}}, {a, b}} is adjacent to {a, {a,
b}}.

Proof: {{a, {a, b}}, {a, b}} ∩ {a, {a, b}} = {{a, b}}, which is
nonempty, so {{a, {a, b}}, {a, b}} ∼ {a, {a, b}}.

Theorem 5. In H*,* {{a, {a, b}}, {a, b}} is NOT adja cent to {a,
{a, b}}.

Proof: By the definition of H (as in Fig. 7), {{a, {a, b}}, {a, b}}
is not adjacent to {a, {a, b}}. Thus, even adjacency, the most basic
foundation of graph construction, leads to contradiction.

64

VI. MAX-OVERLAP LABELINGS FOR

ENCRYPTION

Maximum-overlap labelings also have great potential for use in
encryption protocols.

Theorem 6. A maximum-overlap labeling of a graph G = (V, E) is
cryptographically secure against all adversaries.

Proof: Suppose that Alice wants to transmit graph G = (V, E) to Bob.
Alice computes the max-overlap labeling L of the graph and sends (L(V
), L(E)), which Eve intercepts. One of two cases must occur:

• Eve attempts to read the input and falls asleep, or • Eve concludes
that Alice and Bob are insane, and that their transmitted graph must
be worthless. In both cases, Eve gains no information about G.

VII. POETRY

A. The Limerick Graph

Let's take a look the max-overlap labeling of P₂, the length-2 path,
as shown in 8:

Fig. 8: Max-overlap labeling for P₂. As it turns out, this is the
Limerick Graph AABBA.

The vertex and edge sets are

V = {a, b, {a, b}}

E = {{a, {a, b}}, {b, a}}

Verbalized, the edge set is "A, A, B, B, A", or "AABBA." This looks an
awful lot like a rhyme scheme, doesn't it? Specifically, AABBA is the
rhyme scheme for a limerick⁵. In general, it seems like we ought to
be able to get graphs that correspond to other rhyme schemes.

⁵For example:

To label a 3-vertex path

For usage in improper math

Use {{a, b}, a, b}

On v₁ through ₃;

Voila! It's a limerick graph.

B. The Sicilian Octave Graph

A Sicilian Octave is an eight-line poem with alter nating rhymes; i.e.,
its rhyme scheme is ABABABAB. Consider this max-overlap labeling of the
3-clique K₃:

Fig. 9: Max-overlap labeling for K₃, the Sicilian Octave graph, with
Ä(G) =¹₃.

The edge set is

E = {{a, b}, {{a, b}, a}, {b, {a, b}}},

that is, ABABABAB.

C. The Shakespearean Sonnet Graphs (order 1 and 2) We now explore
several rhyme-scheme encoding graphs that may not necessarily be
overlap-maximal, and which allow self-loops. This allows us to further
bridge the (currently, very large) gap between mathe matics and
poetry.⁶

Shakespearean sonnets have a rhyme scheme of ABAB CDCD EFEF GG. Fig. 10
displays a graph with vertex and edge sets

V = {a, b, c, d, e, f, g, {a, b}, {c, d}, {e, f}, {g, g}} E = {{a, b},
{{a, b}, {c, d}}, {c, d}, {e, f}, {{e, f}, {g, g}}}.⁷

Fig. 10: The order-1 Shakespearean sonnet graph is a forest of K₂s,
plus one self loop. It achieves Ä(G) =²₃.

This is a rather disappointing graph. Luckily for us, Shakespeare wrote
more than one sonnet. Fig. 11 shows the graph corresponding to two
Shakespearean sonnets.

(Shakespeare wrote 153 sonnets; the order-153 Shakespearean sonnet graph
is left as an exercise to the reader.)

⁶The two fields have been slowly growing apart since Omar Khayyam,
although Lewis Carroll made a valiant effort to bring them back
together.

⁷I know this overlaps the margin of the page. shhhhh.

65

Fig. 11: The order-2 Shakespearean sonnet graph, with edges E = {{a,
b}, {{a, b}, {c, d}}, {c, d}, {e, f}, {{e, f}, {g, g}}, {{a, b}, a},
{b, c}, {d, {c, d}}, {{e, f}, e}, {f, {g, g}}}, i.e. ABAB CDCD EFEF GG
ABAB CDCD EFEF GG. Ä(G) =⁴₁₁.

D. Other Poems (Selected)

Fig. 12: Rhyme scheme graph of The Raven by Edgar Allen Poe,
encoding rhyme scheme AABCCCBBB. E = {{a, a}, {b, c}, {c, {c, b}}, {b,
b}} with Ä(G) =¹₄.

Fig. 13: Rhyme scheme graph of The New Colossus by Emma Lazarus
("Give me your tired, your poor, your huddled masses yearning to
breathe free"), encoding rhyme scheme ABBAABBACDCDCD with Ä(G)
=²₅.

Fig. 14: Rhyme scheme graph of Fox in Socks by Dr. Seuss, encoding
rhyme scheme AAAAAAAAAAAA.⁸

⁸not to be confused with the sound emitted by distressed humans

Fig. 15: Rhyme scheme graph of Toxic by Britney Spears, encoding
rhyme scheme ABACDCDD with Ä(G) = 0.

VIII. CONCLUSION

In this work, we presented an overlap-maximization technique for
labeling graphs. In order to counter the increasing ease of
communication facilitated by the internet, we propose an alternate
naming convention for graphs, in order to minimize clarity when spoken
aloud.

In particular, scholars should strive to use either the name for a
poem whose rhyme scheme encodes the graph, or directly list out the
edge set of the maximal overlap labeling of the graph.

For example:

1) the triangle graph could be validly called "AB, ABA, ABB" or "The
Fox in Socks graph without self-loops";

2) the 4-cycle could be called "the second-smallest connected
component of the Order 2 Shakespeare graph" or "AB, BAB, BABAB, ABAB."

Creativity is encouraged.

66

IX. REFERENCES

[i] Google.

[ii] Wikipedia.

[iii] The Poetry Foundation.

All figures created in totally legal, non-pirated Adobe Illustrator.

X. APPENDIX A: PROOF OF THEOREM 1 A. Upper bounding È(G)

First, we show that È(G) f |V | − 2.

Suppose for the sake of contradiction that È(G) ≥ |V | − 1, i.e.
that there are |V | − 1 vertices which share a label with an edge.
Let these vertices be V⁰= {v₁, v₂,· · · v_{|V |−1}}.

Note that these vertices are all of the form {x, y} for some x, y ∈ V
. So, ¢ is a strict partial order on the finite set V⁰, so there
exists at least one minimum element under ¢.

Let m = {m₁, m₂} be such a minimum element. m₁ and m₂ must be
vertices, since the vertex m overlaps with an edge. Since m is the
minimum, m₁, m₂ ̸∈ V⁰. So we have two vertices that are not in
V⁰, a contradiction. =⇒ ⇐=

Second, we show that È(G) f |E|. Note that _{L:V →U}|L(E) ∩ L(V )|
(Definition 1)

È(G) = max

f max

_{L:V →U}|L(E)|

_{L:V →U}|E| (L bijective)

= max

= |E|

as desired.

B. Constructively lower bounding È(G)

We show a recursive procedure to assign labels to a graph to ensure
min(|E|, |V | − 2) overlap between edge and vertex labels.

In particular, it suffices to iteratively build up the graph by adding
vertices and keeping the following invariant:

Invariant: A graph G = (V, E) with |V | ≥ 2 can be min(|E|, |V |
− 2)-overlap-labeled, with the labeling determined entirely by the
labels of two "base" vertices (in particular, the two "base" vertices
can be arbitrarily renamed, and the rest of the graph relabeled
accordingly, while preserving the overlap).

Base cases: The theorem trivially holds for |V | ∈ {0, 1, 2}⁹.

⁹Whether |V | = 0 is a valid graph is up for debate; see "Is the
null-graph a pointless concept?" by Harary and Read, 2006

For |V | = 3: The labelings displayed in Fig. 16 cover all cases.
Note that a, b could be labeled anything, and the rest of the graph
relabeled accordingly, while keeping the invariant true.

Fig. 16: Overlap-maximal labelings for |V | = 3, the base case for
our recursive labeling scheme. Note that in each case the amount of
overlap È(G) is less than

min(|E|, |V | − 2).

Inductive step. Consider some graph G = (V, E) with |V | ≥ 4. We
split into cases:

• |V | − 2 \< |E|. Then, there must be some vertex v with minimum
degree. Inductively label G \ v, then choose some edge e ∈ G \ V as
the label for v.

• |E| f |V | − 2. Then, the graph is disconnected. -- If one
connected component is a singleton ver tex, then label it arbitrarily,
and inductively label the rest.

-- Otherwise, partition the graph into some con nected component C and
G \ C. Inductively label C and G \ C.

Choose two edges e₁, e₂ ∈ E(C) \ V (C) (i.e., they do not yet
share a name with a vertex), and rename G \ C, using these e₁,
e₂'s labels as the "base" labels for G \ C.

It's easy to verify that this process preserves the invari ant; the
details are left to the reader.

67

XI. APPENDIX B: THE EDGE SET OF K₇ UNDER MAX-OVERLAP RELABELING

E(K₇) = {

{a, b},

{a, {a, b}},

{a, {a, {a, b}}},

{a, {{a, {a, b}}, {a, b}}},

{a, {b, {{a, {a, b}}, {a, b}}}},

{a, {{{b, {{a, {a, b}}, {a, b}}}}, {a, b}}},

{b, {a, b}},

{b, {a, {a, b}}},

{b, {{a, {a, b}}, {a, b}}},

{b, {b, {{a, {a, b}}, {a, b}}}},

{b, {{{b, {{a, {a, b}}, {a, b}}}}, {a, b}}},

{{a, b}, {a, {a, b}}},

{{a, b}, {{a, {a, b}}, {a, b}}},

{{a, b}, {b, {{a, {a, b}}, {a, b}}}},

{{a, b}, {{{b, {{a, {a, b}}, {a, b}}}}, {a, b}}}, {{a, {a, b}}, {{a,
{a, b}}, {a, b}}},

{{a, {a, b}}, {b, {{a, {a, b}}, {a, b}}}},

{{a, {a, b}}, {{{b, {{a, {a, b}}, {a, b}}}}, {a, b}}}, {{{a, {a, b}},
{a, b}}, {b, {{a, {a, b}}, {a, b}}}}, {{{a, {a, b}}, {a, b}}, {{{b,
{{a, {a, b}},

{a, b}}}}, {a, b}}},

{{b, {{a, {a, b}}, {a, b}}},

{{{b, {{a, {a, b}}, {a, b}}}}, {a, b}}}

}

68

15

Neo-Classical Logic

Une Logique non classique^*

Martin Vassor Fangyi Zhou

Resume.

Standard logics, such as classical logic or intuitionist logic
suffer from flaws that remained unaddressed as of today (like
philosophical questions about using the axiom of excluded middle,
which draws the line between the two logic mentioned previously). In
this paper, we introduce neo-classical logic, in an attempt to
reconciles classical and intuitionistic logics, as well as to capture
some real-world event which can not be explained by previous logics,
due to their lack of expressivity.

After introducing its syntax and semantique, we study the meta-theory
of this new logic, and show multiple interesting results, such as the
law of contradiction, or that validity is decidable, which states
that a proposition can simultaneously hold and not hold.

1 Introduction

Motivation. Our paper is motivated by strong empirical evidences
that some events, concepts, objects can simultaneously exist and don't
exist (see Figure 1, but also [6, 8, 10]).

Despite strong evidence, to the best of our knowledge, no logic seems
to be expressive enough to prove statements as simple as « Exists a
such that a does not exist. » This absence (or possibly presence)
shows that there exists a gap between current theoretical models and
the actual reality.

Contribution. Our main contribution in this paper is to
introduce a new logic, neoclassical logic¹, which reduces this
gap, allowing us to express more faithfully the subtleties of the
world.

Moreover, we demonstrate how we use neo-classical logic to reconcile
two important logic theories, namely classical logic and
intuitionistic logic, with a constructive proof of the Law of
Excluded Middle in our neo-classical logic. Neo-classical logic
subsumes classical logic and intuitionistic logic.

Outline. In Sections 2 et 3, we discuss the limitations of the
two most popular logics, namely classical and intuitionistic logic.
From that, we conclude that there is a need to fill the gap left
opened by those two logic systems; in order to capture real-life cases
that can not be addressed by the two logic aforementioned. In Section
4, we introduce our proposal, which we call neo-classical logic, by
successively presenting both its syntax and its semantique. In Section
5, we discuss the meta-theory of the logic. Finally we present an
actual use case in Section 6, showing that our logic allows to capture
complex arguments while remaining decidable. Finally, in Section 7, we
conclude by discussing some limitations, presenting some unrelated
work and highlight some interesting research paths for future work.

2 Classical Logic is Not Modern

We look up the dictionary entry of the word « classical » in Cambridge
dictionary again [9], and see what it could mean. The main usages
include « traditional in style or form, or based on methods developed
over a long period of time, and considered to be of lasting value »,
and « used to describe something that is attractive because it has a
simple, traditional style. »

We also note that this sentence was provided as an exemple:

Does she study classical ballet or modern ballet?

^*A paper on logic must have some French, but we don't know how to
typeset accents, so here it is.

¹Also spelled « neo-classical » due to our lack of motivation to
check the consistency across the paper.

69

{width="2.0638199912510937in"
height="0.4774136045494313in"}{width="2.122749343832021in"
height="1.356486220472441in"}

$a$ Evidence of the non existence of the word « Artefact » [10]

$b$ Evidence of existence of the word « Arte fact » [8]

Figure 1: Empirical evidence of the simultaneous existence and
non-existence of the word « Artefact » in English, according to the
Cambridge Dictionary.

This sentence gives a strong hint that classical ballet is not
modern. We are also confident to conclude that classical logic is not
modern, via a simple application of substitution. A modern-day logic
should be modern, in order to catch up with contemporary development
of real life events and technological advancements. Moreover, it is an
unfortunate fact that classical logic cannot represent the
simultaneous existence and non-existence of a word (cf. Figure 1) ---
it cannot model contemporary dictionaries in a modern world.

3 Intuitionistic Logic is Not Intuitive

In the first courses of computer science, students learn classical
logic due to its simplicity. Some mathematicians and theoretical
computer scientists, however, prefer intuitionistic logic.
Unfortunately, we are unable to find an entry for « intuitionistic »
in Cambridge dictionary, which is a strong hint that it is not
intuitive. Think about that, why would computer scientists call
something intuitive using a complicated word that looks like «
intuitive », but decide against its use?

4 Neo-Classical Logic

In order to address the unsatisfactory deficiency of both classical
logic and intuitionistic logic, we introduce neo-classical logic.

4.1 Formules

A ::= a, b, c, ... Atomic propositions

P, Q ::= A Atomic proposition

| ¬P Negation of P

| P ∧ Q And

Notice that, together with the semantique we define below, and in
particular with the traditional encoding of P ∨ Q as ¬(¬P ∧
¬Q) and P ⇒ Q as ¬(P ∧ ¬Q), we can have usual constructs.
Therefore, we allow ourself to use those elements as needed.

The syntax of formules does not differ much from classical or
intuitionistic logic --- this is why we think our logic is
neo-classical: it looks classical, but is quite modern. We explain the
modernness in detail when we discuss the semantique.

We fix a set A of atomic propositions, ranging over a, b, c,
.... Atomic propositions form the basic form of neo-classical logic
formules, and we also recognise standard logical operators: negation,
conjunction, disjunction, and implication.

70

4.2 Semantique

Let ` be a (binary) predicate defined according to the rules in
Figure 2. We use an infix notation: Γ ` P where Γ is an environment
and P a formula of the neo-classical logic. We write Γ ̸` P for
¬(Γ ` P).

Γ ` a<sup>(Exists)</sup>Γ<sub>1</sub> ` P Γ₂ ` Q

Γ ` ¬a^(¬Exists)a ∈ Γ a ̸∈ Γ

Γ ` ¬Q

Γ₁ ∪ Γ₂ ` P ∧ Q<sup>(∧)</sup>Γ ` ¬P

Γ ` ¬(P ∧ Q)^(DeMorganL)

Γ ` ¬(P ∧ Q)<sup>(DeMorganR)</sup>Γ ` P

Γ ` ¬¬P^(¬¬I)

Figure 2: Inference rules of the ` predicate

The novelty of neo-classical logic lies in the rules (¬Exists) and
(Exists). Those two rules establish a strong correspondence between a
witness (or observation) of an event and establishing the existence of
that event. On the one hand, rule (¬Exists) states that if we have no
evidence of an event, we can conclude that this event does not exist.
This is, informally, motivated by the fact that having no evidence of
an event is indistinguishable from that event not existing. Indeed, if
there is a way to distinguish two possible worlds, one with the event,
one without; then the distinctive element actually serves as witness
of the event. Therefore, from Occam's razor (often stated « Pluralitas
non est ponenda sine necessitate »², and widely spread in the
literature, see e.g. [7, Book I, 4, 188a17], but also [4, Prima
Pars, Q.2 art.3 -AG2, &c.]), we should not suppose the existence of
an event we have no evidence of; which ends the justification of that
rule.

Conversely for (Exists), if we have an observation of an event a, we
can deduce the existence of that event. This is trivially motivated.

Exemple 1 (Artefact exists and does not exist).

artefact ` artefact<sup>(Exists)</sup>∅ ` ¬artefact^(¬Exists)

artefact ` artefact ∧ ¬artefact^(∧)

Theoreme 2 (Consistency). The deduction system is
consistent, i.e. ∅ ̸` ⊥.

Preuve. It is not possible to introduce ⊥. Voilà.

Remarque 3 (Absence of Absolute Truths And Absolute Falsities). We
note that > and ⊥ are not formules of neo-classical logic. This is
important since there are no absolute truths and absolute falsities in
the modern world. We make a conscious effort to model this observation
in our logic.

5 Meta³-Theory of Neo-Classical Logic

Lemme 4 (To tree or not to tree).

∀Γ . ∀P . Γ ` P ∨ Γ ̸` P

Preuve. First, we need to clarify the statement. It is obviously not
a neo-classical formula (typically, neo classical logic do not have
quantifier). Instead, it is a formula from first-order classical
logic, where ` is a (binary) predicate; and ∨ is the disjunction of
classical logic.

The result then follows directly from the law of excluded-middle of
classical logic. Voilà. Lemme 5 (If no proof, then proof of
negation).

∀Γ . ∀P . Γ ̸` P ⇒ Γ ` ¬P

Preuve. By induction on P.

Case P = a**: ***from the premisses of (Exists), we have that
*a ̸∈ Γ. Therefore, rule (¬Exists) applies. Case P = ¬Q**:
***neither (¬Exists), (DeMorganL), (DeMorganR) nor (¬¬I) apply. By
case analysis on *Q:

²« entities should not be multiplied beyond necessity », translation
Wikipedia.

³Not to be confused with Meta Platforms Inc, "metaverse", or
whatever.

71

Case Q **is* a**:***since (¬Exists) does not apply, we have
that a ∈ Γ, therefore Γ ` Q, therefore Γ ` ¬P by applying
(¬¬I).

Case** Q is *¬Q⁰:*** since (¬¬I) does not apply, we have
that Γ ̸` Q<sup>0</sup>. From the induction hypothesis, we have that Γ `
¬Q⁰. Therefore, Γ ` ¬P (i.e. Γ ` ¬¬¬Q⁰) by applying (¬¬I).

Case** Q is Q*₁ ∧ Q₂:*** since neither (DeMorganL) nor
(DeMorganR) apply, we have that both Γ ̸` ¬Q<sub>1</sub> and Γ ̸` ¬Q₂.
Therefore, from the induction hypothesis, both Γ ` ¬¬Q<sub>1</sub> and Γ `
¬¬Q₂. From the premises of (¬¬I) on those two statements, we have
that both Γ ` Q<sub>1</sub> and Γ ` Q₂. Therefore, Γ ` Q<sub>1</sub> ∧ Q<sub>2</sub>
(i.e. Γ ` Q), by applying (∧). Therefore, we can prove Γ ` ¬P,
i.e. Γ ` ¬¬Q, by applying (¬¬I).

Case** P* = Q₁ ∧ Q₂:*** Since rule (∧) does not apply,
we have that for any subsets Γ₁, Γ₂ of Γ, neither Γ₁ ` Q<sub>1</sub>
nor Γ<sub>2</sub> ` Q₂. I.e., ∀Γ⁰ ∈ Γ . Γ ̸` Q<sub>1</sub> (resp. Q<sub>2</sub>).
Therefore, from the induction hypothesis, we have that for any subset
Γ<sup>0</sup> of Γ, Γ<sup>0</sup> ` ¬Q₁ (resp. Q₂).

Therefore, the proof finishes by showing that Γ ` ¬P, i.e. Γ `
¬Q₁ ∧ Q₂ by applying either (DeMorganL) or (DeMorganR). Voilà.

5.1 Law of Contradiction

Lemme 6 (Empiricism brings knowledge).

∀P . ∃Γ . Γ ` P

Preuve. By induction on P.

Case P = a**: ***let Γ = {*a}, apply (Exists).

Case** P* = ¬P⁰:*** By case analysis on P⁰:

Case P⁰= a*: ***Let Γ = ∅, and the result holds directly
from rule (¬Exists).

Case** P*⁰= Q₁ ∧ Q₂:*** From the induction hypothesis,
we know that there exist Γ₁ such that ¬Q₁ holds. Therefore, we
can take Γ = Γ₁ and apply (DeMorganL).

Case P⁰= ¬Q**:***In that case, we have to prove ¬¬*Q. The
result holds directly from the induction hypothesis and by applying
the rule (¬¬I).

Case** P* = Q₁ ∧ Q₂:*** From the induction hypothesis,
we know that there exists a Γ₁ (resp. Γ₂) such that Γ₁ ` Q<sub>1</sub>
(resp. Γ<sub>2</sub> ` Q₂). We can take Γ = Γ₁ ∪ Γ₂ and apply the rule
(∧). Voilà.

Theoreme 7 (Law of contradiction).

∀P . ∃Γ . Γ ` P ∧ ¬P

Preuve. This Theoreme is a corollaire of lemme 6. Voilà.

5.2 Excluded-Middle

Theoreme 8 (Excluded-Middle).

∀Γ . ∀P . Γ ` P ∨ ¬P

Preuve. As we said above, P ∨ ¬P is encoded in our calculus as
¬(¬P ∧ ¬¬P). Therefore, we actually have to prove that this
formula holds for all P and Γ.

From lemme 4, Γ ` P or Γ ̸` P. By case analysis:

Case Γ ` P*: ***

^...

Γ ` P^Hypothesis

Γ ` ¬¬P

(¬¬I)

Γ ` ¬(¬P ∧ ¬¬P)^(DeMorganL) 72

Case Γ ̸` P**:***From lemme 5, Γ ` ¬*P.

^...

Γ ` ¬P^Hypothesis

Γ ` ¬¬¬P

(¬¬I)

Γ ` ¬(¬P ∧ ¬¬P)^(DeMorganR)

Voilà.

5.3 Decidability of Validity

Finally, we want to show that deciding whether a formula P is valid
under a context Γ is decidable. For that, we first show how to compute
two sets: first, the set of event that must be in Γ, and second, the
set of event that must not be in Γ, in order to satisfy the formula.
Finally, we compare Γ with those two sets to decide whether P can be
satisfied.

Set of required events. Let R*_P* be the set of required events
to satisfy P. Notice that there might be multiple ways to satisfy a
single formula, i.e. multiple sets of required events are possible.
Therefore, R*_P* is actually a set of sets of events. R*_P* can
easily be defined as follows:

R*_P*^def=

^{}

∅ if P = ¬a, ∀a {{a}} if P = a, ∀a {P_*Q*1 ∪
P_*Q*2|P_*Q*1 ∈ R_*Q*1 ∧ P_*Q*2 ∈ R_*Q*2 } if P = Q₁ ∧
Q₂ ^{}

R_¬*Q*1 ∪ R_¬*Q*2if P = ¬(Q₁ ∧ Q₂) R*_Q* if P = ¬¬Q

Lemme 9 (Required is correct). For all Γ*, for all P, if*
̸ ∃P ∈ R*_P such that* P ¦ Γ*, then* Γ ̸` P.

Preuve. The proof is direct, by induction on P. Each possible case
of corresponds to a case of R*_P*, corres ponds to the premises of a
rule (or two rules for the two variants of (DeMorgan)). Voilà.

Lemme 10. For all P, R*_P is computable.*

Preuve. Let n₁(P) be the number of occurrences of ¬(Q₁ ∧
Q₂) in P. Let n₂(P) be the number of occurrences of ¬Q
in P. Let ≺ be an order relation on formules defined as follows:

P ≺ Q if and only if (n₁(P) \< n₁(Q)) or (n₁(P)
= n₁(Q) and n₂(P) \< n₂(P))

We easily show, by induction, that, for each recursive computation of
R*_Q* to compute R*_P, *Q ≺ P. Also, there is a finite number of
recursive call at each step.

Therefore, the computation eventually terminates. Voilà. Set of
forbidden events. Let F*_P* be the set of forbidden events to
satisfy P. F*_P* can easily be defined as

follows:

^{}

F*_P*^def=

^{}

{a} if P = ¬a, ∀a ∅ if P = a, ∀a F_*Q*1 ∩ F_*Q*2if P =
Q₁ ∧ Q₂ F_¬*Q*1 ∪ F_¬*Q*2if P = ¬Q₁ ∧ Q₂ F*_Q* if
P = ¬¬Q

Lemme 11 (Forbidden is correct). For all Γ*, for all P, if*
Γ ∩ F*_P* ̸= ∅, then Γ ̸` P.

Preuve. The proof is direct by induction on P. Each possible case of
corresponds to a case of F*_P*, corresponds to the premises of a rule
(or two rules for the two variants of (DeMorgan)). Voilà.

Lemme 12. For all P, F*_P is computable.*

Preuve. The proof is similar to the proof of lemme 10. Voilà. 73

Theoreme 13. For all Γ*, for all P,* Γ ` P if and only if:

1. ∃P ∈ R*_P* . P ¦ Γ*; and*

2. Γ ∩ F*_P* = ∅.

Preuve. The if direction is a direct consequence of lemmes 9 et 11, by
contraposition. We have to show the other direction, that is the two
conditions are sufficient to have Γ ` P. The result is direct by
induction on P. Voilà.

Corollaire 14 (The validity of a formula is decidable). For
any Γ*, for any P,* Γ ` P is decidable.

6 Practical Applications

As logicians, we have a moral duty to remain close to practical
applications of our works. Indeed, the formal study of arguments allows
every citizen to cast a light and understand actual facts on the world
that surrounds us. In order to show that our work has indeed some
practical use, in this section, we show an actual exemple taken from
everyday's life.

While police violence is a well-documented issue in modern democracies
[1, 5], we still have statements that police violence does not exist
[2,3] (e.g. « Ne me parlez pas de [. . . ] violences policières, ces
mots sont inacceptables dans un État de droit. »⁴, Macron et al.,
reported at 0:40 in [3], and in [2]).

In the following, we show that our logic captures such arguments, as
they are actually derivable. Let v_p an actual observation of police
violence. In the following, we show how we can simultaneously claim that
such event occurs and does not occurs, given such observation.

v_p ∈ {v_p}^{Set theory}

{v_p} ` v_p(Exists)v_p ̸∈ ∅^{Set theory}

∅ ` ¬v_p(¬Exists)

{v_p} ` v_p ∧ ¬v_p(∧)

7 Conclusion, Unrelated and Future Work

In this paper, we presented new semantique for the propositional
calculus. We show that this new semantique have interesting properties.
For instance, the standard law of excluded-middle holds in our calculus,
or that the validity of a formula is decidable. In addition, we show
that new, previously unexplored⁵ laws, such as the Law of
contradiction also holds for our calculus.

Overall, as stated in the motivation, our calculus captures intuitive
notions of proofs based on the notion of evidence. Our calculus finally
brings the formal basis needed for reasoning on the ontological⁶
notion of existence, which is a problem that was left opened since
almost 2.5 millennia; yet still relevant as of today.

Unrelated Work. Very little is unrelated to this one, as this work
regards the relation between evidence and knowledge. Therefore, all
evidence-based sciences are related to this work. Furthermore, as it
aims to give a formal basis to ontological⁷ arguments, it relates to
philosophical works, which we therefore have to exclude from unrelated
works as well.

Future Work. The current main limitation is that it is based on
propositional logic; and therefore lacks the expressiveness needed to
capture more complex argumentations. Future work could include extending
this paper up to higher-order logic. Such extension could benefit from
an extended expressiveness, possibly being expressive enough to encode
arithmetics.

The exemple shown in Section 6 illustrate that our logic allows a fine
characterisation of the reasoning that leads to some claims. For
instance, we saw that the authors of the sentence above (Macron et
al., reported in [2, 3]) loose some information in their reasoning.
The current work is limited in that it does not give explanation for
this loss. Intuitively, we can hypothesize various causes, ranging from
plain lack of knowledge to deliberate ignorance. Future works is needed
to elaborate on such hypothesis.

⁴« Don't say [. . . ] "police violence" to me, those words are
unacceptable in a Rechtsstaat. » Translation by the authors. ⁵To the
best of the author's knowledge.

⁶Ditto.

⁷or « epistemic », as you can guess, the authors are not philosophers
and are just using those big words to impress reviewer #2. 74

Remerciements

We thank anonymous reviewers from Sigbovique 2022 for their helpful
comments and insights, except reviewer #2. We think this paper should be
rated 5/7.

References

[1] Violences policières, les situer pour mieux y résister. Vacarme
77, 4 (2016), 8--23. Place: Paris Publisher: Association Vacarme.

[2] VIDEO. \"Gilets jaunes\" : Macron juge \"inacceptable dans un Etat
de droit\" de parler de \"violences policières\", Mar. 2019.

[3] Clique TV. Clément Viktorovitch : Peut-on parler de violences
policières ? - Clique - CANAL+, June 2020.

[4] d'Aquino, T. Summa Theologiae. XIII AD.

[5] Jobard, F. Bavures policières ? La force publique et ses usages.
TAP / Politique et société. La Découverte, Paris, 2002.

[6] Schrödinger, E. Die gegenwärtige Situation in der Quantenmechanik.
Naturwissenschaften 23, 48 (Nov. 1935), 807--812.

[7] ᾿Αριστοτέλης. Φυσικὴ ἀκρόασις. c. IV BC.

[8] University of Cambridge. Cambridge dictionary -- Entry "Artefact",
2022.

[9] University of Cambridge. Cambridge dictionary -- Entry
"Classical", 2022.

[10] University of Cambridge. Cambridge dictionary -- Spellcheck of
"Artefact", 2022. 75

16

A Patriotic Analysis of Programming Paradigms

Jacob Weiner

Abraham Lincoln Chair for Patriotism

Founding Fathers University

SIGBOVIK 2022

Abstract

In this paper, we will examine why dependent type theory is the most
patriotic paradigm for programming. We will examine several key
founding documents to draw our conclusion. We will view many American
flag images and feel patriotic.

76