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)))

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!