Skip to main content

Functions

The propositions-as-types interpretation states that proofs are programs. The meaning of this applies principally to functional programming, so let's first limit the python-space with constraints.

  1. We will deal with total functions, meaning if I say def f(x: float) -> float:, what I mean is that you can give f any float. A vocabulary I might use is "signature", in this case, f's "signature" (or its "type signature" or just "type") is float -> float, meaning it's input or argument type is float and its output or return type is float.
  2. We will deal with pure functions, meaning if I say that f is a function, what I mean is that its behavior is constrained entirely by its signature, and I can test it by supplying inputs and doing nothing else. If I need to test it by mocking up state or running a headless browser, then it is not pure.
  3. Functions that are total and pure are deterministic, meaning for every state from which anybody could call f at 2, f(2) == f(2). If f(2) == 3 on Tuesday in your console, then f(2) == 3 on Wednesday in your CI environment.

It's unlikely, but not impossible, that you've ever seen real world software obey these constraints entirely. Mathematics, however, is not so base and vile. In fact, obeying these constraints makes your python more like mathematics: what mathematicians mean by "function" is equivalent to the constraints that functional programmers aspire to. (Take another look at the determinism constraint. Now recall "the vertical line test" from precalculus. Exercise: What is the relationship between the two?)

The epsilon-delta notion of limit.

This is not a blog post that teaches limits from the ground up. If you just want to know enough calculus to appreciate the python, watch this video on KhanAcademy real quick.

In brief, we are concerned with the relationship between wiggling in the x direction and wiggling in the y direction--- does one impose constraints on the other? How can we refine our wiggling behavior to better understand the function at hand?

embed image here.

This post deals with the verbal, logical structure of the epsilon-delta notion of limit, leaving geometry to other resources. The notion can be expressed in symbols, in fact you can understand it independently of visuals if you want. Shortly, the definition of limit will be given symbolically, and from this definition we will extract a proof strategy.

Take some distance function dist-- we'll use the following definition for the remainder of the post: 

def dist(x: float, y: float) -> float: 
  """the standard metric on R"""
  return abs(x - y)

Now take some f : D -> R, it has some domain (probably an interval subset of the real numbers) and it returns a real number. (this is sort of like having a return type of float). You're interested in the behavior of f about some number a from its domain. 

the limit as x goes to a of f(x) == f(a) 
if and only if
forall eps > 0, (there) exists delt > 0, (such that) forall x in D,   
  if dist(x, a) < delt then dist(f(x), f(a)) < eps

Let's review quantifiers. Quantifiers come in two kinds-- the Universal Quantifier means "for each" or "for all". We say we're quantifying over all elements of a set/type. The other kind is the Existential Quantifier, which means "there exists" or "for at least one". Quantification can be thought of as a game where your opponent makes moves and you make moves. You can't control your opponent's move (you can't control which eps > 0 they will select), but you can control your moves (you can select a delt > 0).

In the definition of limit, pay attention to the rhythm of the quantifiers. Notice that they alternate: forall... exists... forall.... This is critical. Each successive quantified variable is dependent on what came before. So when you see forall eps, exists delt, ... you already know that delt is "a function of eps", which specifically means that the number delt is the output of some function at the input eps. In other words, when my opponent selects an eps, I can use that eps in my calculation of delt. In the end, the proposition if dist(x, a) < delt then dist(f(x), f(a)) < eps is dependent on everything that came before.

Let us begin translating this definition into Python.​

What do you think is the Python meaning of forall eps? Exercise: review the post up until this point, and think about it for 5 minutes (literal walltime) to try and anticipate where I'm going with this.

There must be some gibberish to form a page break, to make it harder for people to

Accidentally read ahead.

I hope we have wasted enough space with these three lines.

Recall our totality constraint. According to the totality constraint, a function is defined on every input. So if you declare def f(x: int) -> bool:, you are obligated to ensure that it doesn't fail on -2895 or 42 or 57 because those are all ints and you declared that you could turn any int into a bool. Did my choice of italics give it away yet? When you declare that you can turn any A into a B, you are declaring that you can turn every A into a B, so the analogy we'll use for forall eps is function declaration. 

# assume f, a are known and in scope
def proof_scope_1(eps):

That makes sense: when you write a function, you don't necessarily know what arguments are going to be supplied. If you did, you'd write constants instead of a function. Just as a function doesn't know at compile time what its arguments are going to be, you don't know at proof-writing time what your opponent's move is going to be. Think of the person calling the function as your opponent, not you.

Python's type-hinting system is not refined enough to express positive real number, so I omitted the type signature altogether. If I wanted, I could've written 

def proof_scope_1(eps: float): 
  assert eps > 0

to represent that eps is a positive real number, but it wouldn't exactly be truthful-- then the function wouldn't be defined on all of its input type, because it would fail on eps = -1.0 with AssertionError.

let's continue.

forall eps > 0, exists delt > 0: 

# assume f, a are known and in scope
def proof_scope_1(eps): 
  # select some function `foo`
  delt = foo(eps)

When it's your move, you can select a number and that number may be dependent on eps. Let's observe an example.

Suppose f = lambda x: m * x for some constant m. Later, we'll work this example. For now, I'll just give that we select foo = lambda eps: eps / abs(m). Since delt is allowed to be any function of eps so long as the outcome is strictly positive, our task is to select which function of eps we need.

Let's continue through the definition. forall eps > 0, exists delt > 0, forall x in D: 

# assume f, a are known and in scope
def proof_scope_1(eps): 
  delt = foo(eps) # select an appropriate foo
  def proof_scope_2(x):

forall is represented by def again.

To bring it all in, we'll represent the core proposition as a program. The program will be scoped by the quantifiers, and failure will mean you've failed to supply a proof (you've failed to supply the correct foo).

if dist(x, a) < delt then dist(f(x), f(a)) < eps: 

if dist(x, a) < delt: 
  assert dist(f(x), f(a)) < eps

Extracting a proof outline from the program

In this section we'll examine the lambda x: m * x example closer.

We'll start from the bottom and write down the assertion, and see if we can massage it into a viable expression working up to find a value of foo. That's it! 

dist(f(x), f(a)) < eps # unfold dist, f
abs(m*x - m*a) < eps # distributivity
abs(m * (x - a)) < eps # a lemma about abs and multiplication
abs(m) * abs(x - a) < eps # divide both sides by abs(m)
abs(x - a) < eps / abs(m) # fold dist
dist(x, a) < eps / abs(m) # our value of foo is lambda eps: eps / abs(m)

And we notice that dist(x, a) is in the conditional! In other words, we've worked backwards through the algebra that proves if dist(x, a) < eps / abs(m): assert dist(f(x), f(a)) < eps always succeeds. If it returned a bool instead of asserting, it would always return true

def proof_scope_1(eps): 
  delt = eps / abs(m)
  def proof_scope_2(x): 
    if dist(x, a) < delt: 
      assert dist(f(x), f(a)) < eps

Property-based testing with Hypothesis

A proof is not a unit test. But I represented the proposition, after scoping it through function defs, as an assert. I'd also like to show you in a system more expressive than python's types that this code actually runs.

Property-based testing is an automated way of making unit tests as proof-like as possible. Today, we will work with the testing framework Hypothesis. From the docs

Think of a normal unit test as being something like the following:

1.    Set up some data.
2.    Perform some operations on the data.
3.    Assert something about the result.

Hypothesis lets you write tests which instead look like this:

1.    For all data matching some specification.
2.    Perform some operations on the data.
3.    Assert something about the result.

This is often called property-based testing, and was popularised by the Haskell library Quickcheck.

Lets take a walk down to your projects dir. I will assume you have a python 3 installed, and I will not cover virtual environments (though you should use them rather than just pip installing all willy nilly).

mkdir epsdelt && cd epsdelt
pip install hypothesis
vim line_is_continuous.py # text editor of your choice

In your favorite text editor, begin by pasting in the above function and nested function. Then, insert the following imports at the top 

from hypothesis import given
from hypothesis.strategies import floats

Hypothesis works by decorating your functions with data generation instructions in a straightforward syntax.

If we want to test strictly positive floats eps, we proceed: 

@given(eps=floats().filter(lambda x: x > 0))
def proof_scope_1(eps): 
  ...

Let's use some compact interval D, represented as a tuple of the left endpoint and right endpoint. 

  ...
  @given(x=floats().filter(lambda x: D[0] <= x <= D[1]))
  def proof_scope_2(x): 
    ...

Now call your "test" 

if __name__=='__main__': 
  proof_scope_1()

You don't need to supply any arguments, because the decorators handle it for you.

In your shell, you can now run python line_is_continuous.py to see whether or not I lied to you about the value of foo!

In reality, Hypothesis wants us to change some of the settings, and I'll increase the verbosity of the test output. The complete document looks like this. 

from hypothesis import given, settings, HealthCheck, Verbosity
from hypothesis.strategies import floats

m = 1.5
dist = lambda x,y: abs(x-y)
a = 3
D = (2,4)


@settings(verbosity=Verbosity.verbose)
@given(eps=floats().filter(lambda x: x > 0))
def proof(eps): 
    global m, dist, a
    delt = eps / abs(m)

    @settings(suppress_health_check=(HealthCheck.filter_too_much,), max_examples=10)
    @given(x=floats().filter(lambda x: D[0] <= x <= D[1]))
    def proof_scope_2(x):
        global m, dist, a
        nonlocal eps, delt
        if dist(x, a) < delt: 
            assert dist(m*x, m*a) < eps

    proof_scope_2()

if __name__=='__main__': 
    proof()

Above, I mentioned that type hints don't express what I'm interested in. I don't have a type, in python, of strictly positive floats. Hypothesis, on the other hand, allows me to express this with its .filter(lambda syntax.

You've now:

  • experienced firsthand the analogy between logical scope and programming scope (principally through associating forall with def.
  • tested that your program runs on a real computer with real input

An important next step is to try breaking it.

Modify the value of foo so that line 15 is delt = (eps + 1) / abs(m). Test your understanding of the epsilon-delta notion of limit by predicting what will happen. also try: (eps - 1) / abs(m), 1 / abs(m), eps and predict what will happen for each.

I leave this as an exercise.

Further exercise-- abstract m, a, and D into functions and have Hypothesis test over them. Remember-- a must lie in D or the test case will be vaccuous!

footnotes:

  1. What we're actually doing is using the limit definition of continuity.
  2. There's a stronger idea in dependent type theory called a Pi type, which generalizes functions and conditionals into highly similar structures. I couldn't think of a way to spoof it in python today, so for now we'll have to stick with comparing forall to def and leaving conditionals as their own thing.
  3. It's actually very misleading to compare unit tests to proofs, even property-based tests. Proof involving forall is not "we tested so many cases, i'm sure the probability that we missed an important case is slim to none", it's a much stronger idea.