## Table: Formalization of Fault-Tolerant (FT) Logic Gates
### Overview
The image displays a two-column technical table titled "FT Gates" and "Formalization." It provides symbolic representations and corresponding formal logical definitions for five fundamental digital logic gates within a fault-tolerant (FT) framework. The table is structured with clear horizontal dividers separating each gate entry.
### Components/Axes
* **Column 1 Header:** "FT Gates"
* **Column 2 Header:** "Formalization"
* **Structure:** A table with five data rows, each dedicated to one logic gate.
* **Visual Elements:** Each row in the first column contains a standard logic gate symbol (AND, OR, NAND, NOR, XOR) with labeled input lines (e.g., 1, 2, n, -1, -2). The second column contains formal logical expressions and code-like definitions.
### Detailed Analysis
The table is transcribed row-by-row below. All text is in English, with formal logical notation.
**Row 1: AND Gate**
* **FT Gates Column:** Symbol for an AND gate with two inputs labeled "1" and "2".
* **Formalization Column:**
* `⊢ ∀ p L1 L2.`
* `AND_FT_gate p L1 L2 = FTree p (AND (gate_list L))`
**Row 2: OR Gate**
* **FT Gates Column:** Symbol for an OR gate with two inputs labeled "1" and "2".
* **Formalization Column:**
* `⊢ ∀ p L.`
* `OR_FT_gate p L = FTree p (OR (gate_list L))`
**Row 3: NAND Gate**
* **FT Gates Column:** Symbol for a NAND gate (AND gate with a circle at the output) with two inputs labeled "-1" and "-2".
* **Formalization Column:**
* `⊢ ∀ p L1 L2.`
* `NAND_FT_gate p L1 L2 =`
* `FTree p (AND (gate_list(compl_list p L1 ++ L2)))`
**Row 4: NOR Gate**
* **FT Gates Column:** Symbol for a NOR gate (OR gate with a circle at the output) with two inputs labeled "-1" and "-2".
* **Formalization Column:**
* `⊢ ∀ p L.`
* `NOR_FT_gate p L =`
* `FTree p (NOT (gate_list L))`
**Row 5: XOR Gate**
* **FT Gates Column:** Symbol for an XOR gate with two inputs labeled "1" and "2".
* **Formalization Column:**
* `⊢ ∀ p A B.`
* `XOR_FT_gate p A B =`
* `FTree p (OR [AND [NOT A; B]; AND [A; NOT B]])`
### Key Observations
1. **Consistent Pattern:** Each formalization begins with a turnstile symbol (`⊢`), indicating a theorem or definition, followed by universal quantification (`∀`).
2. **Common Structure:** All definitions use a core function `FTree p (...)`, suggesting a common "Fault-Tolerant Tree" constructor parameterized by `p`.
3. **Input Handling:** Gates with two explicit inputs (AND, NAND, XOR) use parameters `L1` and `L2` or `A` and `B`. Gates with a list input (OR, NOR) use a single list parameter `L`.
4. **Logical Composition:** The formalizations define complex gates using more basic operations:
* NAND is defined as an AND applied to a list that includes a complemented input (`compl_list`).
* NOR is defined as a NOT applied to an OR.
* XOR is defined using the canonical sum-of-products form: `(NOT A AND B) OR (A AND NOT B)`.
5. **Input Labeling:** The NAND and NOR gate symbols use negative numbers (`-1`, `-2`) for inputs, which may visually denote inverted inputs or a specific fault-tolerant encoding scheme.
### Interpretation
This table serves as a formal specification for implementing fault-tolerant versions of standard logic gates. The notation appears to be from a formal verification or hardware description language context.
* **Purpose:** It bridges the gap between intuitive gate symbols and their rigorous mathematical/computational definitions, which is crucial for designing reliable systems where faults must be tolerated.
* **Relationships:** The table shows a clear hierarchy. The AND and OR gates are defined most directly. The NAND and NOR gates are then defined in terms of AND/OR and NOT operations. The XOR gate is built from NOT, AND, and OR. This reflects the functional completeness of the set {AND, NOT} or {OR, NOT}.
* **Notable Pattern:** The use of `gate_list` and list concatenation (`++`) suggests that these definitions are designed to operate on lists of signals or wires, which is common in structural hardware descriptions. The parameter `p` likely represents a proof, policy, or property context required for the fault-tolerant construction.
* **Anomaly/Inference:** The XOR definition is the only one that explicitly uses a nested list structure (`[...]`) and does not directly use a `gate_list` wrapper on its arguments `A` and `B`. This might indicate that `A` and `B` are treated as atomic signals in this definition, whereas `L`, `L1`, and `L2` in other gates are lists of signals.
