Given:

T ≡ λxy.x
F ≡ λxy.y
~ ≡ λx.x(λuv.v)(λab.a)

What is ~T ?

~T = (λx.x(λuv.v)(λab.a))(λcd.c)
(λcd.c)(λuv.v)(λab.a) = TFT
λuv.v = F

Hence ~T = F

Conversely, what is ~F ?

~F = (λx.x(λuv.v)(λab.a))(λcd.d)
(λcd.d)(λuv.v)(λab.a) = FFT
λab.a = T

Hence ~F = T

Let's continue on the madness. The multiplication of two numbers x and y can be computed using the lambda function:

(λxyz.x(yz))

What is (λxyz.x(yz))22 ?

(λxyz.x(yz))22
(λyz.2(yz))2
(λz.2(2z))

λz.(λxy.x(x(y)))((λuv.u(u(v)))z)
λz.(λxy.x(x(y)))(λv.z(z(v)))

λz.(λy.(λv.z(z(v)))((λv.z(z(v)))(y)))
λz.(λy.(λv.z(z(v)))(z(z(y))))
λz.(λy.(z(z(z(z(y))))))
λzy.(z(z(z(z(y))))) = 4

In Lambda Calculus, natural numbers can be defined as:

0 ≡ λs.(λz.z) ≡ λsz.z
1 ≡ λsz.s(z)
2 ≡ λsz.s(s(z))
3 ≡ λsz.s(s(s(z))) and so on.

Given the successor function: S ≡ λwyx.y(wyx), what is 2S3 ?

2S3 = (λsz.s(sz))(λwyx.y(wyx))(λuv.u(u(uv)))
(λz.(λwyx.y(wyx))((λwyx.y(wyx))z))(λuv.u(u(uv)))
(λwyx.y(wyx))((λwyx.y(wyx))(λuv.u(u(uv)))) = S(S3)

S3 = (λwyx.y(wyx))(λuv.u(u(uv)))
λyx.y((λuv.u(u(uv)))yx)
λyx.y((λv.y(y(yv)))x)
λyx.y(y(y(yx))) = 4

S(S3) = S4 = (λwyx.y(wyx))(λuv.u(u(u(uv))))
λyx.y((λuv.u(u(u(uv))))yx)
λyx.y((λv.y(y(y(yv))))x)
λyx.y(y(y(y(yx)))) = 5

Hence 2S3 = S(S3) = S4 = 5

[Theory: [Graph: {*}]->(Attr)->[Conceptual]]->(Attr)->[Nice]

• 05 Sep 2005
• E3 Visa for Australians
• 8 Sep 05
• E-3 E3 VISA - FINAL RULE
• H-1B Support Statement 07-06-05.doc
• Labor Condition Application for Nonimmigrant Workers (9035 Form 2008-04-05.pdf)
• Labor Condition Application Cover Pages (9035CP Form 08-04-05.pdf)
• Dual Intent Doctrine

Pretty amazing. Companies in the US are now required to report all the H1B foreign worker wages to the Department of Labor, and get published online to the world! You can find the search engine here.

Some Interesting findings for the highest paid H1B Software practitioners in year 2003:

• Microsoft: one H1B Software Architect with annual salary of $165K
• Sun: two H1B Senior Staff Engineer with annual salary of $141,667.00
  
• Apple: one H1B Software Engineer with annual salary of $140K
• Yahoo!: one H1B Information Services with annual salary of $125K
  
• Google: one H1B Software Engineer with annual salary of $120K
• eBay: one H1B Rule Engine Designer with annual salary of $115K