Untitled

We are interested in making a virus in the lambda calculi. The aim is for the virus to preserve functionality, this is, if we have a lambda-expression f such that

f x => g

for an infected version of f, namely f[v]

f[v] x => g[v]

where g[v] is the infected version of g.

In 'pure' (or untyped) lambda calculus all our values are lambda-expressions of the form 'λx.[...]' so we need not worry about primitive types yet. At the end I'll peek at a way to deal with this in Scheme, a trivial task, really.

Now, how do we preserve functionality while infecting a λexpr? Remember that for any expression f

(λd.λx.d x) f

is equivalent to just 'f'. So our first idea would be to wrap the host function in such a way and then infect it within the new expression:

(λd.λx.V (d x))

Here V is our (yet undefined) viral expression. when applied to a function f and an argument x it reduces to

(λd.λx.V (d x)) f x

=> (V (f x))

==> (V g)

===> g[v]

of course, we want our g[v] to have the form

(λx.V (g x))

where g is precisely our g expression. that way our virus should take as argument a function (the host function) and return a lambda expression that takes the argument to the function and does the application

(λd.λx.V (d x))

Looks familiar? Turns out this is precisely the form our viral expression V is going to adopt, for if

d x => g

then

V g => (λx.V (g x))

Thus V is of the form (λd.λx.V (d x))

We can see then, that V is a recursive function that can be expressed like

V = (λd.λx.V (d x))

But in the lambda calculus we need to work around recursive functions due to the lack of assignment expressions. How do we make a recursive function? Remember the Y-combinator?

(λf.(λx.f (x x)) (λx.f (x x)))

Where a function is fed to itself, this is, it is repeated in the definition.

Inspired by this idea, and with some little thinking we arrive to the following definition for our virus:

V* = (λv.λd.λx.(v v) (d x))

As you can see, it looks pretty much like our former definition, where we replace V with (v v), but what exactly is the 'v' we are feeding? turns out it is V* itself:

(λv.λd.λx.(v v) (d x)) (λv.λd.λx.(v v) (d x))

=> (λf.λx.[(λv.λd.λx.(v v) (d x)) (λv.λd.λx.(v v) (d x))] (f x))

The resulting expression we'll call V°. It's easy to see that (V* V*) => V° and

V° = (λd.λx.(V* V*) (d x))

But a closer look will reveal that V° takes an expression and returns a 'wrapped' version of it, like the first form we saw, so applied to f we have

(λd.λx.(V* V*) (d x)) f

=> (λx.(V* V*) (f x))

When applied to an argument x such that [f x => g] then we have

(V* V*) g

and so

V° g

and finally

(λx.(V* V*) (g x))

Thus, this is the virus we wanted, it does both preserve functionality and 'copy' itself to the new function.