tells-two-symbols-of-one-datum-apart-between-firings.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps an answer by the operands a firing
# brought down, and a symbol is an operand of its own: every symbol dataizes
# to the one manufactured datum, so two firings over two symbols come down to
# the same bytes, yet they stand for two values nobody worked out. A memo
# keyed on the bytes would answer the second firing with the symbol the first
# one minted and make the two values one; this one keys on the symbol, so each
# firing mints a symbol of its own. The two firings are the two 'morph'
# operands of 'L_pair', each fired by the dispatch of φ off its call.
symbolic: |
  - λ: L_dataized
    dataize:
      𝛿1: $.target
    𝑛: Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
  - λ: L_pair
    morph:
      𝑛1: $.x
      𝑛2: $.y
    𝑛: ⟦ φ ↦ ⟦ x ↦ 𝑛1, y ↦ 𝑛2 ⟧ ⟧
location: 'Q.@'
acyclic: plausible
input: >
  ⟦ bytes(φ) ↦ ⟦⟧,
    dataized(target) ↦ L_dataized:λ,
    pair(x, y) ↦ L_pair:λ,
    φ ↦ Φ.pair(
      Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ,
      Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ ).φ ⟧
result: '⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧'
protocol: |
  𝕄(Φ.φ):
    𝑛·0·1 := Φ.pair( x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ )
    𝑛·0·2 := 𝑛·0·1( y ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ )
    𝔼(L_pair):
      𝕄(ξ.x):
        𝑛·1·1 := Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎1:λ ) )
        𝔼(L_dataized):
          𝔻(ξ.target):
            𝕄(ξ.target):
              𝑛·2·1 := Φ.bytes( φ ↦ 𝜎1:λ )
              morphed 𝑛·2·2 := 𝑛·2·1
            boxed 𝑛·2·3 := 𝑛·2·2.φ
            𝛿·2·1 := 𝔻(𝜎1:λ)
          𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.target)
          𝑛·2·4 := Φ.bytes( φ ↦ 𝜎3:λ )  # 𝑛
          𝕄(𝑛·2·4):
            𝑛·2·5 := Φ.bytes( φ ↦ 𝜎3:λ )
            morphed 𝑛·2·6 := 𝑛·2·5
          𝑛·2·7 := 𝑛·2·6  # 𝕄(𝑛·2·4)
        morphed 𝑛·1·2 := 𝜎3:λ
      𝑛1·1 := 𝑛·1·2  # 𝕄(ξ.x)
      𝕄(ξ.y):
        𝑛·1·3 := Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎2:λ ) )
        𝔼(L_dataized):
          𝔻(ξ.target):
            𝕄(ξ.target):
              𝑛·3·1 := Φ.bytes( φ ↦ 𝜎2:λ )
              morphed 𝑛·3·2 := 𝑛·3·1
            boxed 𝑛·3·3 := 𝑛·3·2.φ
            𝛿·3·1 := 𝔻(𝜎2:λ)
          𝛿1·3 := 𝛿·3·1  # 𝔻(ξ.target)
          𝑛·3·4 := Φ.bytes( φ ↦ 𝜎4:λ )  # 𝑛
          𝕄(𝑛·3·4):
            𝑛·3·5 := Φ.bytes( φ ↦ 𝜎4:λ )
            morphed 𝑛·3·6 := 𝑛·3·5
          𝑛·3·7 := 𝑛·3·6  # 𝕄(𝑛·3·4)
        morphed 𝑛·1·4 := 𝜎4:λ
      𝑛2·1 := 𝑛·1·4  # 𝕄(ξ.y)
      𝑛·1·5 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧:φ  # 𝑛
      𝕄(𝑛·1·5):
        morphed 𝑛·1·6 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧:φ
      𝑛·1·7 := 𝑛·1·6  # 𝕄(𝑛·1·5)
    morphed 𝑛·0·3 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧