takes-the-answer-of-a-firing-with-the-same-operands.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps what a firing answered by the λ
# function and the operands it brought down, beside the formation it fired.
# Here 'a' and 'b' fire two formations, since one reads 'x' and the other
# reads 'y', so the memo of formations misses the second. Yet both bring the
# same datum down, and an entry answers from its operands alone. Before #1661
# the firing under 'b' minted '𝜎2' for the very value '𝜎1' already named. Now
# it brings its operand down, finds the firing already answered and takes
# '𝜎1', minting nothing.
symbolic: |
  - λ: L_dataized
    dataize:
      𝛿1: $.target
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
deep: true
partial: true
acyclic: plausible
input: >
  ⟦ dataized(target) ↦ L_dataized:λ,
    a ↦ Φ.dataized( target ↦ Φ.x ),
    b ↦ Φ.dataized( target ↦ Φ.y ),
    x ↦ ⟦ Δ ⤍ 01- ⟧,
    y ↦ ⟦ Δ ⤍ 01- ⟧ ⟧
result: >
  ⟦ dataized(target) ↦ L_dataized:λ,
    a ↦ 𝜎1:λ,
    b ↦ 𝜎1:λ,
    x ↦ 01-:Δ,
    y ↦ 01-:Δ ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.a):
      𝑛·0·1 := Φ.dataized( target ↦ Φ.x )
      𝔼(L_dataized):
        𝔻(Φ.a🌵0):
          𝛿·1·1 := 01-
        𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.target)
        𝑛·1·1 := 𝜎1:λ  # 𝑛
        𝑛·1·2 := 𝜎1:λ  # 𝕄(𝑛·1·1)
    𝕄(Φ.b):
      𝑛·0·2 := Φ.dataized( target ↦ Φ.y )
      𝔼(L_dataized):
        𝔻(Φ.a🌵1):
          𝛿·2·1 := 01-
        𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.target)
        𝑛·2·1 := 𝑛·1·2  # 𝑛
        𝑛·2·2 := 𝑛·1·2  # 𝕄(𝑛·2·1)