parks-two-sides-that-do-not-join.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The sides differ in a datum, so no join makes one term of them and the
# firing writes 'diverged' (#1996). No line of the text named either side,
# since each morphs to itself, so the line writes them as the terms they are.
# Under '--partial' the site the join stands at is parked instead of failing
# the run.
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.c
    join:
      on: 𝛿1
      left: $.a
      right: $.b
location: 'Q.y'
partial: true
input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ ⟦ Δ ⤍ 01- ⟧ ⟧, b ↦ ⟦ φ ↦ ⟦ Δ ⤍ 02- ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'
result: '⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ ⟦ Δ ⤍ 01- ⟧ ⟧, b ↦ ⟦ φ ↦ ⟦ Δ ⤍ 02- ⟧ ⟧, λ ⤍ L_fork ⟧.φ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝔻(ξ.c):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)
      𝕄(ξ.a):
        morphed 𝑛·1·1 := 01-:Δ:φ
      𝕄(ξ.b):
        morphed 𝑛·1·2 := 02-:Δ:φ
      diverged 𝑛·1·1 vs 𝑛·1·2  # they differ at .φ.Δ, and the join names no otherwise