fabricates-a-formation-of-two-sides-of-different-shapes.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The two sides of a join are formations of different shapes: the left one
# binds 'φ' and 'ke', the right one 'φ' alone. No join makes one term of them,
# but the block names 'L_join' under 'otherwise', so the firing fabricates a
# formation holding every attribute of both sides, each of them a copy of
# 'L_join' that holds the symbol the condition came down to, not the 42 that
# symbol is dataized to (#2026), and asks for that attribute the copies of
# both sides the formation holds under 'left🌵' and 'right🌵' (#2029), and
# writes 'fabricated' in place of 'diverged', with that formation in its
# comment (#2024). The
# program asks that formation for 'ke', which the left side binds alone, so
# its copy asks the right side for 'ke' too, through the 'φ' of that side.
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.c
    join:
      on: 𝛿1
      left: $.a
      right: $.b
      otherwise: L_join
location: 'Q.y'
input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ Φ.hx, ke ↦ Φ.ty ⟧, b ↦ ⟦ φ ↦ Φ.zu ⟧, λ ⤍ L_fork ⟧.ke ⟧'
result: '⟦ λ ⤍ L_join, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ρ.left🌵.ke, right🌵 ↦ ρ.right🌵.ke ⟧'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝛿1·1 := 𝔻(𝜎1:λ)  # 𝔻(ξ.c)
      fabricated 𝑛·1·1 := ⟦ φ ↦ Φ.hx, ke ↦ Φ.ty ⟧ and Φ.zu:φ  # ⟦ left🌵 ↦ ⟦ φ ↦ Φ.hx, ke ↦ Φ.ty ⟧, right🌵 ↦ Φ.zu:φ, φ ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧, ke ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.ke, right🌵 ↦ ρ.right🌵.ke ⟧ ⟧