linear_logic_o3_mini_high_feb_2025.py

# Generated by o3-mini-high, as of Feb 2025, so may have some inaccuracies.


class Linear:
    """
    A class that simulates a linear (single‑use) resource.

    Each Linear object wraps a value and tracks whether it has been consumed.
    Optionally, a resource may be marked as "unrestricted" (via the exponentials)
    so that it can be duplicated.
    """

    def __init__(self, value, consumed=False, unrestricted=False):
        self.value = value
        self.consumed = consumed
        self.unrestricted = unrestricted

    def consume(self):
        """Consume the resource if it is linear; if unrestricted, do not mark it consumed."""
        if not self.unrestricted:
            if self.consumed:
                raise RuntimeError("Resource already consumed!")
            self.consumed = True
        return self.value

    def clone(self):
        """
        For an unrestricted resource (one created by an exponential), produce a duplicate.
        (For linear resources, cloning is not allowed.)
        """
        if self.unrestricted:
            return Linear(self.value, consumed=False, unrestricted=True)
        else:
            raise RuntimeError("Cannot clone a linear (restricted) resource.")

    # ---------------------------
    # Multiplicative connectives
    # ---------------------------
    def __mul__(self, other):
        """
        Tensor (⊗): combine two resources.

        If the resource is linear, its use consumes it; if unrestricted, it is not consumed.
        """
        val1 = self.consume() if not self.unrestricted else self.value
        val2 = other.consume() if not other.unrestricted else other.value
        return Linear((val1, val2))

    def __rshift__(self, func):
        """
        Linear implication (–o): apply a rule (a function) to the resource.

        The resource is consumed (if linear) and its value is passed to func;
        the result of func is wrapped as a new Linear resource.
        """
        val = self.consume() if not self.unrestricted else self.value
        return Linear(func(val))

    def __xor__(self, other):
        """
        Par (⅋): multiplicative disjunction.

        Both operands are used (consumed if linear) and the result is a ParResource.
        Later the environment (or a caller) can choose which branch to use.
        """
        val1 = self.consume() if not self.unrestricted else self.value
        val2 = other.consume() if not other.unrestricted else other.value
        return ParResource(val1, val2)

    # ---------------------------
    # Additive connectives
    # ---------------------------
    def __and__(self, other):
        """
        With (&): additive conjunction.

        Both resources are provided but when used, the consumer must choose one branch.
        """
        val1 = self.consume() if not self.unrestricted else self.value
        val2 = other.consume() if not other.unrestricted else other.value
        return WithResource(val1, val2)

    def __or__(self, other):
        """
        Plus (⊕): additive disjunction.

        Both resources are combined, but the choice of branch is understood to be made
        by the "producer" of the resource (though in our simulation the choice is deferred).
        """
        val1 = self.consume() if not self.unrestricted else self.value
        val2 = other.consume() if not other.unrestricted else other.value
        return PlusResource(val1, val2)

    # ---------------------------
    # Exponential modalities
    # ---------------------------
    def of_course(self):
        """
        Of course (!) marks the resource as unrestricted.

        This allows the resource to be duplicated (using .clone()) and reused.
        """
        if self.consumed:
            raise RuntimeError("Cannot convert a consumed resource to unrestricted.")
        return Linear(self.value, consumed=False, unrestricted=True)

    def why_not(self):
        """
        Why not (?) is simulated similarly to of_course().
        """
        if self.consumed:
            raise RuntimeError("Cannot convert a consumed resource to unrestricted.")
        return Linear(self.value, consumed=False, unrestricted=True)

    def __str__(self):
        if self.consumed and not self.unrestricted:
            return "Linear(consumed)"
        elif self.unrestricted:
            return f"Linear(unrestricted, {self.value})"
        else:
            return f"Linear({self.value})"

    def __repr__(self):
        return self.__str__()


# ---------------------------
# Helper classes for non-tensor connectives
# ---------------------------
class ParResource(Linear):
    """
    Represents a resource formed by the par (⅋) connective.

    It holds two alternatives, one of which can later be chosen.
    """

    def __init__(self, left, right):
        # We treat the stored pair as a linear resource.
        super().__init__((left, right))

    def choose(self, option):
        """
        Choose one branch (0 or 1) from the par resource.
        """
        if option not in (0, 1):
            raise ValueError("Par choice must be 0 or 1")
        return Linear(self.value[option])

    def __str__(self):
        return f"Par({self.value[0]}, {self.value[1]})"


class WithResource(Linear):
    """
    Represents a resource formed by the additive conjunction (with, &) connective.

    The consumer is expected to choose one branch to use.
    """

    def __init__(self, left, right):
        super().__init__((left, right))

    def choose(self, option):
        """
        Choose one branch (0 or 1) from the with resource.
        """
        if option not in (0, 1):
            raise ValueError("With choice must be 0 or 1")
        return Linear(self.value[option])

    def __str__(self):
        return f"With({self.value[0]}, {self.value[1]})"


class PlusResource(Linear):
    """
    Represents a resource formed by the additive disjunction (plus, ⊕) connective.

    In this simulation, the producer makes a (deferred) choice; later the consumer
    can extract one branch.
    """

    def __init__(self, left, right):
        super().__init__((left, right))

    def select(self, option):
        """
        Select one branch (0 or 1) from the plus resource.
        """
        if option not in (0, 1):
            raise ValueError("Plus selection must be 0 or 1")
        return Linear(self.value[option])

    def __str__(self):
        return f"Plus({self.value[0]}, {self.value[1]})"


# ---------------------------
# Demonstration of Practical Usage
# ---------------------------
if __name__ == "__main__":
    print("=== Multiplicative Connectives ===")
    # Create two linear resources.
    a = Linear("p")
    b = Linear("q")

    # Tensor: combine a and b (both are consumed)
    tensor_resource = a * b
    print("Tensor (p ⊗ q):", tensor_resource)

    # Linear implication: apply a rule to the tensor.
    # For example, a rule that takes a tuple (p, q) and produces "r"
    def rule_pq_to_r(resource_tuple):
        p_val, q_val = resource_tuple
        print(f"Rule applied: combining '{p_val}' and '{q_val}' produces 'r'")
        return "r"

    # Note: tensor_resource is consumed by >>.
    r_resource = tensor_resource >> rule_pq_to_r
    print("After linear implication (r):", r_resource)

    # Demonstrate par (⅋)
    # Reset resources for demonstration:
    a = Linear("p")
    b = Linear("q")
    par_resource = a ^ b
    print("Par (p ⅋ q):", par_resource)
    # Later the environment chooses which branch to use:
    chosen_from_par = par_resource.choose(0)
    print("Chosen branch from par (choice 0):", chosen_from_par)

    print("\n=== Additive Connectives ===")
    # With: additive conjunction
    a = Linear("p")
    b = Linear("q")
    with_resource = a & b
    print("With (p & q):", with_resource)
    # The consumer chooses one branch:
    chosen_from_with = with_resource.choose(1)
    print("Chosen branch from with (choice 1):", chosen_from_with)

    # Plus: additive disjunction
    a = Linear("p")
    b = Linear("q")
    plus_resource = a | b
    print("Plus (p ⊕ q):", plus_resource)
    # The consumer selects one branch (in practice, the producer’s choice is fixed):
    selected_from_plus = plus_resource.select(0)
    print("Selected branch from plus (choice 0):", selected_from_plus)

    print("\n=== Exponential Modalities ===")
    # Of course: mark a resource as unrestricted so it can be cloned.
    token = Linear("TOKEN_123")
    token_unrestricted = token.of_course()
    print("Unrestricted token:", token_unrestricted)
    # Now the unrestricted token can be cloned and used repeatedly:
    token_copy1 = token_unrestricted.clone()
    token_copy2 = token_unrestricted.clone()
    print("Cloned token copy1:", token_copy1)
    print("Cloned token copy2:", token_copy2)

    # Why not: simulated the same as of_course in our example.
    another_token = Linear("TOKEN_ABC")
    token_unrestricted2 = another_token.why_not()
    print("Unrestricted token (why not):", token_unrestricted2)

    # Trying to reuse a linear (non-unrestricted) resource causes an error.
    try:
        a = Linear("sensitive")
        # Consume it via an implication:
        _ = a >> (lambda x: x + "_used")
        # A second use will raise an error.
        _ = a >> (lambda x: x + "_again")
    except RuntimeError as e:
        print("\nExpected error on reusing a linear resource:", e)