Substitution is objective (II)
mbuliga@pm.me or @xorasimilarity on telegramContinues from: Substitution is objective (I)
Uses: Pure See
Main:
The abstracted duplication from part (I) does not treat the two variables obtained from duplication on equal footing.
Indeed, we have a beta reduction
(\(=d.c).T) C -> \(=d.C).(T[c=C])
and then a copy-beta reduction
\(=d.C).(T[c=C]) -> (T[c=C])[d=C]
Let's see the treatment of duplication in Pure See style.
Analysis of the duplication inside the S combinator with pure see
I use this as an exploration with the purpose to improve the pure see draft.
Recall that the order of commands in pure see does not matter!
For the "mol" and "chora" ... "of" see note 1. and note 0.
Definition of the S combinator in pure see:
in 0 as S_combinator mol (
see 1 from a as 0; \\ \a.1 = 0
see 2 from b as 1; \\ \b.2 = 1
see 3 from c as 2; \\ \c.3 = 2
as 4 from 5 see 3; \\ 4 5 = 3
as a from d see 4; \\ a d = 4
as b from e see 5; \\ b e = 5
in c chora ( \\ duplication of c into d and e
from origin see d as u;
from origin see e as v;
) of (
see origin from u as v;
);
);
An alternative form where among variables we have variables like "(from c see u)" which come from evaluations, i.e. passage to the algebraic form by (ALG) (note 3.) is described further.
Probably it is incorrect, because it is not clear that in the variable "(from c see u)" we pass to the limit.
in S as S_combinator mol(
see 1 from a as S; \\ \a.1 = S
see 2 from b as 1; \\ \b.2 = 1
see 3 from c as 2; \\ \c.3 = 2
see c from (from c see u) as (from c see v); \\ fanout from (ALG) and (SHUFFLE),
\\ missing is "chora" role,
as a from (from c see u) see 4; \\ a c = 4
as b from (from c see v) see 5; \\ b c = 5
as 4 from 5 see 3; \\ 4 5 = 3
);
How to apply it to something else (say "B")
as S_combinator from B see w; \\ S B = w
Explanation of the relation between the first and the alternative form of S_combinator
shuffle (
in c chora (
from origin see d as u;
from origin see e as v;
) of (
see origin from u as v;
);
) as (
in c chora (
from origin see origin as origin;
) of (
see origin from origin as origin;
see origin from d as e;
);
);
For the "shuffle" see note 2.
Notes:
0. The keywords "chora" and "of" admit mols as variables, with the syntax:
in a chora (b) of (c);
where "a" is a variable which does not appear in the mols (b) or (c).
Semantics:
- "chora" passes to the limit with the scale paramaters in (b),
- "of" keeps the scale parameter of (c) as is in the mol where the "chora" is,
- "in" signals that "a" plays the role of "origin" in mols (b), (c)
1. The keyword "mol" is added, with the syntax:
in a as b mol (c);
where "b" is the name (variable) of the mol (c)
"a" is a variable which appears only once in (c)
2. Clarify purpose of the "shuffle" keyword. Maybe the whole (SHUFFLE) should be rewritten with respect to the use of "chora" ... "of".
Syntax:
shuffle (a) as (b);
where (a) is the particular instance of the LHS of the shuffle
and (b) is the particular instance of the RHS of the shuffle.
3. Clarify the alternative form and it's relation with evaluations, or use of (ALG) and with "chora" (note 0. and note 2.)