Semantic Bracketing:

Functional terms are expanded to bracketed terms as follows:

• SMN ⇒ [x].〚SMN〛_x
• SN ⇒ [x].[y].〚SNx〛_y
• KN ⇒ [x].〚KN〛_x

(where x and y are fresh variables)

Bracketed terms are equivocated to non-bracketed terms as follows:

• 〚S(KU)I〛_x = Ux
• 〚S(KU)(KV)〛_x = K(UV)x
• 〚SMN〛_x = 〚M〛_x 〚N〛_x
• 〚SN〛_x = SNx
• 〚KN〛_x = N
• 〚S〛_x = Sx
• 〚K〛_x = Kx
• 〚I〛_x = x
• 〚U〛_x = Ux

See our forthcoming paper for more details.

Functional Reduction:

A reduction of the form:

• S(KU)I → U
• S(KU)(KV) → K(UV)

Abstraction Elimination Algorithm:

We use the following (βη) algorithm for eliminating abstractions:

[x].M ≡ KM [x].x ≡ I [x].Ux ≡ U [x].UV ≡ S([x].U)([x].V)

if x ∉ FV(M) if x ∉ FV(U) if neither (a) nor (c) applies

Barendregt's Axioms:

Barendregt postulates the following six equivalences:

1. S(S(KS)(S(KK)K))(K(SKK)) ≡ K
2. S(S(KS)(S(K(S(KS)))(S(K(S(KK)))S)))(K(K(SKK))) ≡ S
3. S(S(KS)(S(KK)(S(KS)K)))(KK) ≡ S(KK)
4. S(KK)(S(S(KS)(S(KK)(SKK)))(K(SKK))) ≡ S(KS)(S(KK))
5. S(K(S(KS)))(S(KS)(S(KS))) ≡ S(S(KS)(S(KK)(S(KS)(S(K(S(KS)))S))))(KS)
6. S(S(KS)K)(K(SKK)) ≡ I