<commit_before>== Staged calculus of structures ==

Take inspiration from Guglielmi's subatomic logic and the calculus of
structures, but severely reinterpret and augment it:

Every stage s has atoms "@s.a". The notation -@s.a represents the dual
of @s.a.

Every stage s has a multiplicative disjunction @s[P Q] for
branching from a side effect in that stage.

Every stage s has a multiplicative conjunction @s(P Q) for
converging toward a side effect in that stage.

Every stage r and later stage s have an additive connective written
@rs[P Q] or @rs(P Q) for transporting information between those
stages. We use @rs[] when the main stage we're considering is r, and
we use @rs() when it's s.

-- NOTE: For ordered stages r, s, and t, we can infer from @rs(P Q) to
-- @st[P Q] and from @st[] to @rs() within the logic.

Universal quantification on stages (forall s. P) is like
branching from a stage-valued side effect in a pseudo-stage before all stages.

Existential quantification on stages (exists s. P) is like
converging toward a stage-valued side effect in a pseudo-stage after all stages.
-- TODO: Should this be "before all stages" instead?

-- TODO: Actually iron out some quantification rules and write them
-- below. We might want to reformulate this whole thing in terms of
-- quantifiers rather than connectives anyway (look for "in terms of
-- quantifiers"), and that point of view could help clarify what these
-- rules should be.

We don't have just one involutive negation. We have many involutive
negations, each based on a particular stage triple (r, s, t), where r
precedes s and s precedes t.

Based on the rules from "Linear Logic and Noncommutativity in the
Calculus of Structures" (Strassburger 2003) for system SLLS, what
follows are the rules for the down fragment (and most of the up
fragment) of our staged logic. (The up fragment is the dual of the
down fragment across one of our negations.) Unlike Strassburger, we
spell out rules for units rather than treating them as special cases
of the atom rules.

We'll let r, s, and t be stages such that r precedes s and s precedes
t:

@s()
@s[@s.a -@s.a]

@s()
@s[@rs() @st[]]
-- In terms of quantifiers:
-- <As _ : 0> _
-- <Es j : 2> <NegIf rst j> <Ars _ : 0> _

@st[@s.a @s.a]
@s.a

@st[]
@s.a

    @s[@s(      -- equivalent to "switch"
    @s[   @rs(  -- identical to "additive"
where each row "{ <" and the dual <| |> to < > means:
<{R U} {T V}>
{<R T> <| U V |>}

-- the "switch" rule, here for convenience
@s(@s[R U] T)
@s[@s(R T) U]
-- NOTE: The switch rule is special. See below.

-- the "additive" rule, here in case we get confused about the above
@rs(@s[R U] @s[T V])
@s[@rs(R T) @st[U V]]
-- In terms of quantifiers:
-- <Ars i : 2> <Es j : 2> P`i`j
-- <Es j : 2> <NegIf rst j> <Ars i : 2> <NegIf rst j> P`i`j

-- the "medial" rules
       @s[@st[
    @s(   @st[
@rs(      @st[  -- NOTE: This rule is special. See below.
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
where each row "{ <" means:
<{R U} {T V}>
{<R T> <U V>}

       @s[@st[
    @s(   @st[
@rs(      @st[  -- NOTE: This rule is special. See below.
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
-- for contrast:
       @s(@rs(  -- redundant with its dual, but here for symmetry
@st[      @rs(  -- special from the @rs(@st[ medial and this @rs(@st[
where each row "{ <" means:
<{} {}>
{}
-- TODO: See if there's a rule for @s[@rs(.

       @s[@st[
    @s(   @st[
@rs(      @st[  -- NOTE: This rule is special. See below.
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
-- for contrast:
@st[      @rs(  -- special from the @rs(@st[ medial and this @rs(@st[
@st[@s[         -- from additive
where each row "{ <" means:
<>
{<> <>}
-- TODO: See if there's a rule for @st[@s(.

       @s[@st[  -- implied by additive
    @s(   @st[
@rs(      @st[  -- special implied by @rs(->@st[
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
where each row "{ <" means:
<>
{}

-- TODO: See whether any of the rest of these rules is redundant.

Almost all rules for in-between connectives @st[] and @rs() remain
correct if we use @r[] and @r() in their place. The exceptions are
these and their duals:

  @st[]
  @rs()

  @st[]
  @rs(@st[] @st[])

  @rs()
  @st[@rs() @rs()]

  @st[@rs(R U) @rs(T V)]
  @rs(@st[R T] @st[U V])

The same is true in reverse; most rules for single-stage connectives
@s[] and @s() work with @st[] and @rs() too. However, the switch rule
isn't reachable.

The additive rule and the @rs(@s[ medial rule plug together nicely for
a theorem purely at the additive level, which we call "@rs(->@st["
above:

  @rs(A B)
  @s[@rs(@rs() @s[]) @rs(A B)]
  @rs(@s[@rs() A] @s[@s[] B])
  @s[@rs(@rs() @s[]) @st[A B]]
  @st[A B]


Future directions (TODO):

- Add exponentials. Like our atoms and connectives, exponentials will
  also need to be annotated with particular stages, perhaps like so:

  !rs.@s[R S]
  @s[!rs.R ?st.S]

  Will ?st.R be identical with !st.R? Probably not. Binary additives
  carry boolean (or nonconstructive there-exists-a-boolean)
  information across stages, and exponentials almost do the same for
  natural numbers, but the information is specifically about how many
  times a resource is replicated over @s[] or @s(), for a specific
  `s`.

- Add quantifiers over all stages, per the notes on quantifiers above.

- Integrate this with the dependent typing of Era's module system.
  This will probably require Pi/Sigma quantifiers where a variable
  ranges over some type, so we get to figure out whether it means
  anything (and what it means) to use each of our propositions as a
  type. Is @st[@s() @s()] like a (there-exists-a-)boolean type that's
  (nonconstructively) observable in stage `s`, and if so, what does it
  mean for `t` to appear in that type?

- Write a Penknife library that uses this kind of system (maybe an
  unsound variant) to do practical staged programming. This will
  probably require quantifiers-over-stages and exponentials. These
  features are important because I suspect any !-qualified proposition
  with no free variables is a type whose inhabitants are serializable
  values. Free variables represent something like the ability to point
  to memory in a particular stage: e.g. some OOP object may be stored
  in variables and passed to other objects, but not stored in files
  and passed to other Web servers.<commit_msg>In the staged CoS notes, added rules for exponentials and a notation for dependent linear connectives.<commit_after>== Staged calculus of structures ==

Take inspiration from Guglielmi's subatomic logic and the calculus of
structures, but severely reinterpret and augment it:

Every stage s has atoms "@s.a". The notation -@s.a represents the dual
of @s.a.

Every stage s has a multiplicative disjunction @s[P Q] for
branching from a side effect in that stage.

Every stage s has a multiplicative conjunction @s(P Q) for
converging toward a side effect in that stage.

Every stage r and later stage s have an additive connective written
@rs[P Q] or @rs(P Q) for transporting information between those
stages. We use @rs[] when the main stage we're considering is r, and
we use @rs() when it's s.

-- NOTE: For ordered stages r, s, and t, we can infer from @rs(P Q) to
-- @st[P Q] and from @st[] to @rs() within the logic.

Universal quantification on stages (forall s. P) is like
branching from a stage-valued side effect in a pseudo-stage before all stages.

Existential quantification on stages (exists s. P) is like
converging toward a stage-valued side effect in a pseudo-stage after all stages.
-- TODO: Should this be "before all stages" instead?

-- TODO: Actually iron out some quantification rules and write them
-- below. We might want to reformulate this whole thing in terms of
-- quantifiers rather than connectives anyway (look for "in terms of
-- quantifiers"), and that point of view could help clarify what these
-- rules should be.

We don't have just one involutive negation. We have many involutive
negations, each based on a particular stage triple (r, s, t), where r
precedes s and s precedes t.

Based on the rules from "Linear Logic and Noncommutativity in the
Calculus of Structures" (Strassburger 2003) for system SLLS, what
follows are the rules for the down fragment (and most of the up
fragment) of our staged logic. (The up fragment is the dual of the
down fragment across one of our negations.) Unlike Strassburger, we
spell out rules for units rather than treating them as special cases
of the atom rules.

We'll let r, s, and t be stages such that r precedes s and s precedes
t:

@s()
@s[@s.a -@s.a]

@s()
@s[@rs() @st[]]
-- In terms of quantifiers:
-- <As _ : 0> _
-- <Es j : 2> <NegIf rst j> <Ars _ : 0> _

@st[@s.a @s.a]
@s.a

@st[]
@s.a

    @s[@s(      -- equivalent to "switch"
    @s[   @rs(  -- identical to "additive"
where each row "{ <" and the dual <| |> to < > means:
<{R U} {T V}>
{<R T> <| U V |>}

-- the "switch" rule, here for convenience
@s(@s[R U] T)
@s[@s(R T) U]
-- NOTE: The switch rule is special. See below.

-- the "additive" rule, here in case we get confused about the above
@rs(@s[R U] @s[T V])
@s[@rs(R T) @st[U V]]
-- In terms of quantifiers:
-- <Ars i : 2> <Es j : 2> P`i`j
-- <Es j : 2> <NegIf rst j> <Ars i : 2> <NegIf rst j> P`i`j

-- the "medial" rules
       @s[@st[
    @s(   @st[
@rs(      @st[  -- NOTE: This rule is special. See below.
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
where each row "{ <" means:
<{R U} {T V}>
{<R T> <U V>}

       @s[@st[
    @s(   @st[
@rs(      @st[  -- NOTE: This rule is special. See below.
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
-- for contrast:
       @s(@rs(  -- redundant with its dual, but here for symmetry
@st[      @rs(  -- special from the @rs(@st[ medial and this @rs(@st[
where each row "{ <" means:
<{} {}>
{}
-- TODO: See if there's a rule for @s[@rs(.

       @s[@st[
    @s(   @st[
@rs(      @st[  -- NOTE: This rule is special. See below.
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
-- for contrast:
@st[      @rs(  -- special from the @rs(@st[ medial and this @rs(@st[
@st[@s[         -- from additive
where each row "{ <" means:
<>
{<> <>}
-- TODO: See if there's a rule for @st[@s(.

       @s[@st[  -- implied by additive
    @s(   @st[
@rs(      @st[  -- special implied by @rs(->@st[
@rs(   @s[      -- redundant with its dual, but here for symmetry
@rs(@s(         -- redundant with its dual, but here for symmetry
where each row "{ <" means:
<>
{}

@st[?st.R ?st.T]
?st.@st[R T]

@st[!rs.R !rs.T]
!rs.@st[R T]

@st[]
?st.@st[]

@st[]
!rs.@st[]

@s[?st.R T]
?st.@st[R T]

@s[]
?st.@st[]

-- TODO: See whether any of the rest of the rules is redundant.

-- Our dependent type quantifiers are formulated based on
-- "Redesigning the CLF type theory" by <NAME> 2009
-- <http://www.logosphere.org/~celf/download/clf.pdf>, with a
-- modification in notation so we have duals.
--
-- Where most dependent type theories have types like these...
--
-- \Pi (a : A) -> B{a}
-- \Sigma (a : A) -> B{a}
--
-- ...we write them this way:
--
-- D@s[-a : -rst.!rs.A].B{a}
-- D@s(a : !rs.A).B{a}
--
-- This way we (might, hopefully) have a pair of dual connectives
-- here, with De Morgan rules like this:
--
-- -rst.D@s[-a : A].B{a}
-- D@s(a : -rst.A).-rst.B{a}

-- TODO: Figure out the rules for these dependent connectives.
--
-- TODO: Add a boolean type 2@s and its dual -2@s to represent strong
-- access to data. The type @st[...] seems to only represent that a
-- choice has been taken, not which choice it was. (Actually,
-- exponentials may give us some way to get this kind of strong
-- access, right? Since they support intuitionistic logic and all...)
--
-- TODO: Above, in the introduction of all our notation, list
-- exponentials, dependent connectives, the -rst.A and maybe
-- "<NegIf rst j> A" notations for negation, and (if we add them)
-- booleans.



Almost all rules for in-between connectives @st[] and @rs() remain
correct if we use @r[] and @r() in their place. The exceptions are
these and their duals:

  @st[]
  @rs()

  @st[]
  @rs(@st[] @st[])

  @rs()
  @st[@rs() @rs()]

  @st[@rs(R U) @rs(T V)]
  @rs(@st[R T] @st[U V])

The same is true in reverse; most rules for single-stage connectives
@s[] and @s() work with @st[] and @rs() too. However, the switch rule
isn't reachable.

The additive rule and the @rs(@s[ medial rule plug together nicely for
a theorem purely at the additive level, which we call "@rs(->@st["
above:

  @rs(A B)
  @s[@rs(@rs() @s[]) @rs(A B)]
  @rs(@s[@rs() A] @s[@s[] B])
  @s[@rs(@rs() @s[]) @st[A B]]
  @st[A B]


Future directions (TODO):

- Add exponentials. Like our atoms and connectives, exponentials will
  also need to be annotated with particular stages, perhaps like so:

  !rs.@s[R S]
  @s[!rs.R ?st.S]

  Will ?st.R be identical with !st.R? Probably not. Binary additives
  carry boolean (or nonconstructive there-exists-a-boolean)
  information across stages, and exponentials almost do the same for
  natural numbers, but the information is specifically about how many
  times a resource is replicated over @s[] or @s(), for a specific
  `s`.

  TODO: Now that we've added exponentials, turn the above TODO into
  documentation.

- Add quantifiers over all stages, per the notes on quantifiers above.

- Integrate this with the dependent typing of Era's module system.
  This will probably require Pi/Sigma quantifiers where a variable
  ranges over some type, so we get to figure out whether it means
  anything (and what it means) to use each of our propositions as a
  type. Is @st[@s() @s()] like a (there-exists-a-)boolean type that's
  (nonconstructively) observable in stage `s`, and if so, what does it
  mean for `t` to appear in that type?

  TODO: Now that we've started to work on dependent connectives,
  update the above TODO.

- Write a Penknife library that uses this kind of system (maybe an
  unsound variant) to do practical staged programming. This will
  probably require quantifiers-over-stages and exponentials. These
  features are important because I suspect any !-qualified proposition
  with no free variables is a type whose inhabitants are serializable
  values. Free variables represent something like the ability to point
  to memory in a particular stage: e.g. some OOP object may be stored
  in variables and passed to other objects, but not stored in files
  and passed to other Web servers.
{'fraction_non_alphanumeric': 0.1229102581249164, 'fraction_numerical': 0.0018724087200748963, 'mean_word_length': 3.1879025483057966, 'pattern_counts': {'":': 0, '<': 62, '<?xml version=': 0, '>': 58, 'https://': 0, 'lorem ipsum': 0, 'www.': 1, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '470879', 'n_tokens_mistral': 5033, 'n_tokens_neox': 4807, 'n_words': 2303}