10553, church encoded as ((4*((3*(((5^3)*7)+4))+1))+1)

10553.txt

λs.λz.(λs.λz.s(s(s(s z))))(λz.(λs.λz.s(s(s z)))(λz.(λs.λz.s(s(s z)))(λs.λz.s(s(s(s(s z)))))(λz.s(s(s(s(s(s(s z)))))))(s(s(s(s z)))))(s z))(s z)

others.txt

These also don't fit in a tweet:
11491: ((((2^11)*5)+1)+((5^4)*2)) 
λs.λz.(λs.λz.s(s(s(s(s(s(s(s(s(s(s z)))))))))))(λs.λz.s(s z))(λz.s(s(s(s(s z)))))(s((λs.λz.s(s(s(s z))))(λs.λz.s(s(s(s(s z)))))(λz.s(s z))z))
11514: (((4^5)*11)+((5^3)*2))
λs.λz.(λs.λz.s(s(s(s(s z)))))(λs.λz.s(s(s(s z))))(λz.s(s(s(s(s(s(s(s(s(s(s z)))))))))))((λs.λz.s(s(s z)))(λs.λz.s(s(s(s(s z)))))(λz.s(s z))z)
12659: ((7*((7*((4^4)+2))+2))+3)
λs.λz.(λs.λz.s(s(s(s(s(s(s z)))))))(λz.(λs.λz.s(s(s(s(s(s(s z)))))))(λz.(λs.λz.s(s(s(s z))))(λs.λz.s(s(s(s z))))s(s(s z)))(s(s z)))(s(s(s z)))
13439: (((13^3)*6)+((4^4)+1))
λs.λz.(λs.λz.s(s(s z)))(λs.λz.s(s(s(s(s(s(s(s(s(s(s(s(s z)))))))))))))(λz.s(s(s(s(s(s z))))))((λs.λz.s(s(s(s z))))(λs.λz.s(s(s(s z))))s(s z))
13687: ((7*(((3^2)*((6^3)+1))+2))+2)
λs.λz.(λs.λz.s(s(s(s(s(s(s z)))))))(λz.(λs.λz.s(s z))(λs.λz.s(s(s z)))(λz.(λs.λz.s(s(s z)))(λs.λz.s(s(s(s(s(s z))))))s(s z))(s(s z)))(s(s z))
14519: ((7*((8*((4^4)+3))+2))+1)
λs.λz.(λs.λz.s(s(s(s(s(s(s z)))))))(λz.(λs.λz.s(s(s(s(s(s(s(s z))))))))(λz.(λs.λz.s(s(s(s z))))(λs.λz.s(s(s(s z))))s(s(s(s z))))(s(s z)))(s z)
14734: ((4*(((3^3)+2)*((5^3)+2)))+2)
λs.λz.(λs.λz.s(s(s(s z))))((λs.λz.(λs.λz.s(s(s z)))(λs.λz.s(s(s z)))s(s(s z)))(λz.(λs.λz.s(s(s z)))(λs.λz.s(s(s(s(s z)))))s(s(s z))))(s(s z))
14783: ((((7^4)*6)+2)+((5^3)*3))
λs.λz.(λs.λz.s(s(s(s z))))(λs.λz.s(s(s(s(s(s(s z)))))))(λz.s(s(s(s(s(s z))))))(s(s((λs.λz.s(s(s z)))(λs.λz.s(s(s(s(s z)))))(λz.s(s(s z)))z)))

10 characters larger than yours:

(1+((4*3)*5))*(1+(4*(1+((2*3)*7))))
λs.λz.(λm.λp.(λ2.(λ3.(λ4.λ5.(λ7.m(s(m(m 4 3)5))(s(m 4(s(m(m 2 3)7)))))(p 4 3))(p 2 2)(p 2 3))(s 2))(s(s z)))(λm.λn.λf.λx.m(n f)x)(λm.λn.λf.λx.m f(n f x))

There's something wrong with your expression, but I can't figure out what. This is the type ghci gives:
(\xs -> \xz -> (\xm -> \xp -> (\x2 -> (\x3 -> (\x4 -> \x5 -> (\x7 -> xm(xs(xm(xm x4 x3)x5))(xs(xm x4(xs(xm(xm x2 x3)x7)))))(xp x4 x3))(xp x2 x2)(xp x2 x3))(xs x2))(xs(xs xz)))(\xm -> \xn -> \xf -> \xx -> xm(xn xf)xx)(\xm -> \xn -> \xf -> \xx -> xm xf(xn xf xx)))
:: (((t -> t) -> t -> t) -> (t -> t) -> t -> t)
-> ((t -> t) -> t -> t) -> (t -> t) -> t -> t

But it's an interesting way to attack the problem. If you add exponentiation, which is just application, it might be shorter.

The core part works:

Prelude> let p=(+)
Prelude> let m=(*)
Prelude> let e=(^)
Prelude> let s=(+1)
Prelude> let z=0
Prelude> m(s(m(m 4 3)5))(s(m 4(s(m(m 2 3)7))))
10553

Let's do it differently:

Prelude> (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))
10553

So:

λs.λz.(λm.(λ2.m(s(m(m(s(s 2))(s 2))(s(s(s 2)))))(s(m(s(s 2))(s(m(m 2(s 2))(s(s(s(s(s 2))))))))))(s(s z)))(λm.λn.λf.λx.m(n f)x))

Which is tweetable :)
[Edit: I think I dropped a parenthesis somewhere :/ Now fixed, I hope]

Now entirely coded in ghci:

Prelude> let unchurch n = n (+1) 0
Prelude> let z = \f x -> x
Prelude> let s = \n f x -> f(n f x)
Prelude> let m = \a b f x -> a(b f)x
Prelude> unchurch (s(s(s(s(z)))))
4
Prelude> unchurch $ m (s(s z)) (s(s(s z)))
6
Prelude> unchurch $ (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))
10553

If we lambda lift m then ghci complains about whatever which I think is mostly monomorphism.

Ok, if you use s and z this way then you'll have to define them as part of the lambda expression, something like:

(λs.λz.λm.(λ2.m(s(m(m(s(s 2))(s 2))(s(s(s 2)))))(s(m(s(s 2))(s(m(m 2(s 2))(s(s(s(s(s 2))))))))))(s(s z)))(λf.λx.f x)(λf.λx.x)(λm.λn.λf.λx.m(n f)x)

Now I'm curious, which encoding you were using?

This one: http://en.wikipedia.org/wiki/Church_numerals

It's the same, then I don't get your comment about "if you use s and z this way...".

I can't apply (+1) and 0 to this expression, it doesn't typecheck: λs.λz.(λm.(λ2.m(s(m(m(s(s 2))(s 2))(s(s(s 2)))))(s(m(s(s 2))(s(m(m 2(s 2))(s(s(s(s(s 2))))))))))(s(s z)))(λm.λn.λf.λx.m(n f)x))

It's a problem of typing not of the encoding :)
So the problem is solved if we don't have to add definitions of s and z to the term, which you are using mostly due to typing issues.

The type has to be right to be a church numeral. A function to which I can apply (+1) and 0 has type (a -> a) -> a -> a. Your expression has type (((a -> a) -> a -> a) -> (a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a.

Church numerals (or any other church encoded structures) don't need to be typed so it can't possibly be a type problem, by definition. It's a problem of inference, as it works with "let x = e1 in e2" but not "(\x -> e2) e1", in the second case the compiler in inferring a less suitable signature than it needs to.

Prelude> let z = \f x -> x
Prelude> let s = \n f x -> f(n f x)
Prelude> let m = \a b f x -> a(b f)x
Prelude> :t (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))
(\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))
  :: (t1 -> t1) -> t1 -> t1
Prelude> (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z)) (+1) 0
10553
Prelude> :t ((\m -> (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))) (\a b f x -> a(b f)x))
((\m -> (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))) (\a b f x -> a(b f)x))
  :: (t -> t) -> t -> t
Prelude> ((\m -> (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))) (\a b f x -> a(b f)x)) (+1) 0
10553

No, the above type is not what ghc infers, but what I manually calculate from your expression, it really can't be simplified. That last expression doesn't prove anything, because you are using your own choice of s and z, while it should work for any s and z.

For example, this should work too:

Prelude> let z = 0
Prelude> let s = (+1)
Prelude> let m = \a b f x -> a(b f)x
Prelude> :t (\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))
(\n2 -> m(s(m(m(s(s n2))(s n2))(s(s(s n2)))))(s(m(s(s n2))(s(m(m n2(s n2))(s(s(s(s(s n2))))))))) ) (s (s z))

Ok, now I see what you're meaning. Using the definition from the wikipedia Church numerals:

z = \f x -> x
s n = \f x -> f (n f x)

With this definitions multiplication works. Roughly speaking they should have types like these:

type N a = (a -> a) -> a -> a
z :: N a
s :: N a -> N a

You're using them in a way that have these types:

z :: a
s :: a->a

These break multiplication. Using the wiki definition multiplication works:

m :: N a -> N a -> N a
m a b = \f -> a (b f)
n6 :: N a
n6 = m (s (s (s z))) (s (s z))

n6 (+1) 0
6

Using your definitions how would you write multiplication?

Now we're getting somewhere!

So my mistake was to use s and z, that's confusing! I should have used f and x. I did not mean to say that the expression gets passed the successor function and zero in church numerals. So:

f :: a -> a
x :: a
z :: (a -> a) -> a -> a
s :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a

But these s and z are not given.

Yes. The definition of z and s should be part of the term, so 3 is encoded as:

(s(s(s z))(λn.λf.λx.f(n f x))(λf.λx.x)

With this we have no free terms and only λ calculus is required to evaluate it.
Using these rules I don't think it's possible to encode 10553 in a tweet. AFAICS the factorization I used (i.e. "(1+((4_3)5))(1+(4_(1+((2_3)_7))))") is the shortest in terms of operators (only s and m).

Yes, but there's exponentiation, which is free! F.e. (λf.λx.f(f(f x)))(λf.λx.f(f x)) or (3 2) is 2^3.

I found these factorizations:

*Main> (2*3*17)^2+(2*5)^2+7^2
10553
*Main> unchurch $ p(n2(m n2(m(s n2)(p(m n2 n5)(s(s n5))))))(p(n2(m n2 n5))(n2(s(s n5))))
10553

*Main> 2^13+3^7+5^3+7^2
10553
*Main> unchurch $ p(p((p n7(p n3 n3))n2)(n7 n3))(p(n3 n5)(n2 n7))
10553

The second one is promising, it needs only 7 and 2:

*Main> unchurch $ p(p((p n7(s(s(s(s n2)))))n2)(n7(s n2)))(p((s n2)(s(s(s n2))))(n2 n7))
10553

So it would be something like this:

(λs.λz.λp.(λ2.(λ7.p(p((p 7(s(s(s(s 2)))))2)(7(s 2)))(p((s 2)(s(s(s 2))))(2 7)))(s(s(s(s(s 2))))))(s(s z)))(λn.λf.λx.f(n f x))(λf.λx.x)(λa.λb.λf.λx.a f(b f x))

Which is tweetable if I didn't commit any (new) mistakes.

BTW I didn't knew about free exponentiation, sweet!