Sea

Sea is a three command simple translation of Underload. Sea was discovered by Orby during October of 2020.

Commands

Sea consists of three commands: (, ), and &. ( and ) are quoting operators as in Underload. & is the sole sufficient concatenative combinator.

Rewrite rules

Expression	Rewritten
(a) &	(K) (S') a
(b) (a) K	a
(d) (c) (b) (a) S'	((d) c) a (d) b

Note that only (, ), and & are Sea commands. K and S' are presented as conceptual aids.

Theory

Notice we can reconstruct S' from (, ), and &

 ()()()()()()()&()&&
 ()()()()()()(K)(S')(K)(S')&
 ()()()()()()(K)(S')(K)(K)(S')S'
 ()()()()()()(K)((S')K)S'(S')K
 ()()()()(())(S')K()K(S')K
 ()()()()S'()K(S')K
 (())()()K(S')K
 (())(S')K
 S'

Once we have S' we can recover K.

We first prove that ()()(&)& pops two values off-stack. We call this command R

Proof as follows:

(d)(c)()()(&)&
(d)(c)()()(K)(S')&
(d)(c)()()(K)(K)(S')S'
(d)(c)()(()K)S'(a)K
((d)c)()K(d)()K
(d)()K
[empty]

So we can construct K by follows:

()&()R()()&()R()S'
(K)(S')()R()(K)(S')()R()S'
(K)()(K)()S'
((K))(K)K
K

Then we can construct some useful comands:

• discard (!) as ()R
• fake-cons (H, {{{1}}}) as ()()S'
• parenthesize (A) as ()H!
• execute (^) as ()HK
• discard-below (q, (b)(a)q＝(a)) as AK
• discard-2-below (t, (c)(b)(a)t＝(b)(a)) as AH!q^
• duplicate (:) as ()AHA(^)(^)S'!t, and
• swap (~) as AH!:::S'!qtt. (It's left for an exercise as the reaser to prove them.)

We've constructed the Underload commands ():^a~!, with * left. This isn't implementable, but we can prepend a ^ to all elements and do this translation:

Caption text

Underload	Sea (with constructed commands) !
(	(^
)	)
:~!	see the constructed commands above
a	a(^)~* (equivalence)
^	()~^
*	H!

(note (^b)(^a)* results in equivalent to (^b a))

Also, Sea can be translated into pure underload code:

Caption text

Sea	Underload
K	~!^
S'	a~a~*~a*~a(a~a*:*^!a~*)**^a~a*~a*~a*^a~a~*~a*^a(^)~*~(^)~*^
&	(K)~(S')~^

So, we've proved Sea is a simple translation from Underload (with S removed).

See also

• The Theory of Concatenative Combinators