implicational-logic-graph 0.1.0

A package for working with graphs representing minimal implicational logic models

Implicational Logic Graph

A Python package for working with graphs representing minimal implicational logic models. This library provides tools for constructing and manipulating type systems based on combinatory logic, with support for transactional graph operations.

Features

• 🎯 Type System: Build complex type expressions using variables and applications (function types)
• 🧩 Combinators: Work with S and K combinators from combinatory logic
• 📊 Graph Structure: Represent type transformations as nodes and edges in a directed graph
• 🔄 Transactional Operations: Safely modify graphs with automatic rollback on failure
• ✅ Validation: Ensure graph consistency with built-in validation
• 🚀 Performance: Optimized data structures for O(1) lookups and efficient traversal

Installation

Using Poetry (recommended)

poetry add implicational-logic-graph

Using pip

pip install implicational-logic-graph

From source

git clone https://github.com/yourusername/implicational-logic-graph.git
cd implicational-logic-graph
poetry install

Quick Start

from implicational_logic_graph import var, app, node, Graph, Combinator

# Create type variables
A = var("A")
B = var("B")

# Create a function type: A -> B
func_type = app(A, B)

# Create a graph with nodes
graph = Graph()
with graph.connect() as conn:
    conn.add_node(node(A))
    conn.add_node(node(B))

print(f"Graph has {graph.node_count()} nodes")

Core Concepts

Types

The library provides a type system for minimal implicational logic:

• Variable: Atomic type variables (e.g., A, B, C)
• Application: Function types representing input_type -> output_type

from implicational_logic_graph import var, app

# Simple type variables
A = var("A")
B = var("B")
C = var("C")

# Function type: A -> B
simple_function = app(A, B)

# Complex type: (A -> B) -> C
complex_function = app(app(A, B), C)

# Nested type: A -> (B -> C)
nested_function = app(A, app(B, C))

print(simple_function)    # Output: A -> B
print(complex_function)   # Output: (A -> B) -> C
print(nested_function)    # Output: A -> B -> C

Combinators

Combinators represent transformations between types. The library includes the S and K combinators from combinatory logic:

from implicational_logic_graph import S, K, var

A = var("A")
B = var("B")
C = var("C")

# S combinator: (A -> B -> C) -> (A -> B) -> A -> C
s_comb = S(A, B, C)
print(s_comb)  # Output: S: (A -> B -> C) -> (A -> B) -> A -> C

# K combinator: A -> B -> A
k_comb = K(A, B)
print(k_comb)  # Output: K: A -> B -> A

# Custom combinator
from implicational_logic_graph import Combinator
identity = Combinator(name="I", type=app(A, A))
print(identity)  # Output: I: A -> A

Graph Elements

Nodes

Nodes represent types in the graph:

from implicational_logic_graph import node, var, app

A = var("A")
B = var("B")

# Create nodes
node_a = node(A)
node_b = node(B)
node_func = node(app(A, B))

print(node_a)      # Output: Node(A)
print(node_func)   # Output: Node(A -> B)

Edges

Edges represent combinator transformations between types:

from implicational_logic_graph import edge, node, Combinator, var, app

A = var("A")
B = var("B")

# Create nodes
n1 = node(A)
n2 = node(B)

# Create a combinator that transforms A to B
comb = Combinator(name="f", type=app(A, B))

# Create an edge
e = edge(n1, n2, comb)
print(e)  # Output: A --[f: A -> B]--> B

Graph Operations

Creating and Modifying Graphs

from implicational_logic_graph import Graph, var, node, edge, Combinator, app

# Create an empty graph
graph = Graph()

# Create types and nodes
A = var("A")
B = var("B")
C = var("C")

n_a = node(A)
n_b = node(B)
n_c = node(C)

# Use transactional connections to modify the graph
with graph.connect() as conn:
    conn.add_node(n_a)
    conn.add_node(n_b)
    conn.add_node(n_c)

print(f"Nodes: {graph.node_count()}")  # Output: Nodes: 3

# Add edges
comb_ab = Combinator(name="f", type=app(A, B))
comb_bc = Combinator(name="g", type=app(B, C))

with graph.connect() as conn:
    conn.add_edge(edge(n_a, n_b, comb_ab))
    conn.add_edge(edge(n_b, n_c, comb_bc))

print(f"Edges: {graph.edge_count()}")  # Output: Edges: 2

Querying Graphs

# Get node by UID
node_retrieved = graph.get_node(n_a.uid)

# Get node by type
node_by_type = graph.get_node_by_type(A)

# Check if node exists
exists = graph.has_node(n_a.uid)

# Get outgoing edges from a node
outgoing = graph.get_outgoing_edges(n_a.uid)
print(f"Outgoing from A: {len(outgoing)}")

# Get incoming edges to a node
incoming = graph.get_incoming_edges(n_c.uid)
print(f"Incoming to C: {len(incoming)}")

# Iterate over all nodes
for n in graph.nodes():
    print(f"Node: {n.type}")

# Iterate over all edges
for e in graph.edges():
    print(f"Edge: {e}")

Graph Validation

# Validate graph consistency
try:
    graph.validate()
    print("Graph is valid!")
except ValueError as e:
    print(f"Graph validation failed: {e}")

Usage Examples

Example 1: Simple Type Chain

Build a chain of type transformations:

from implicational_logic_graph import (
    Graph, var, app, node, edge, Combinator
)

# Create graph
graph = Graph()

# Define types
types = [var(name) for name in ["A", "B", "C", "D"]]
nodes = [node(t) for t in types]

# Add nodes
with graph.connect() as conn:
    for n in nodes:
        conn.add_node(n)

# Create transformation chain: A -> B -> C -> D
with graph.connect() as conn:
    for i in range(len(nodes) - 1):
        comb = Combinator(
            name=f"f{i}",
            type=app(types[i], types[i + 1])
        )
        conn.add_edge(edge(nodes[i], nodes[i + 1], comb))

print(f"Created chain with {graph.node_count()} nodes and {graph.edge_count()} edges")

# Query the chain
a_node = graph.get_node_by_type(var("A"))
outgoing = graph.get_outgoing_edges(a_node.uid)
print(f"A has {len(outgoing)} outgoing edge(s)")

Example 2: Complex Type Structure

Work with higher-order functions:

from implicational_logic_graph import (
    Graph, var, app, node, edge, S, K
)

# Create graph
graph = Graph()

# Define type variables
A = var("A")
B = var("B")
C = var("C")

# Create complex types
# Type 1: A
# Type 2: B
# Type 3: A -> B
# Type 4: (A -> B) -> C
t1 = A
t2 = B
t3 = app(A, B)
t4 = app(t3, C)

nodes = [node(t) for t in [t1, t2, t3, t4]]

# Add nodes
with graph.connect() as conn:
    for n in nodes:
        conn.add_node(n)

# Add S and K combinators as edges
s_comb = S(A, B, C)
k_comb = K(A, B)

# Note: You would connect these based on your specific logic model
print(f"Created graph with {graph.node_count()} nodes")
print(f"S combinator type: {s_comb.type}")
print(f"K combinator type: {k_comb.type}")

Example 3: Transactional Rollback

Demonstrate automatic rollback on failure:

from implicational_logic_graph import (
    Graph, var, node, edge, Combinator, app
)

graph = Graph()

A = var("A")
B = var("B")
n_a = node(A)
n_b = node(B)

# Add initial nodes
with graph.connect() as conn:
    conn.add_node(n_a)
    conn.add_node(n_b)

print(f"Initial nodes: {graph.node_count()}")  # Output: 2

# Try to add invalid edge (will fail and rollback)
try:
    with graph.connect() as conn:
        # This will succeed
        C = var("C")
        n_c = node(C)
        conn.add_node(n_c)

        # This will fail (trying to add duplicate node)
        conn.add_node(n_a)  # Already exists!
except RuntimeError as e:
    print(f"Transaction failed: {e}")

# Graph remains unchanged
print(f"Nodes after failed transaction: {graph.node_count()}")  # Output: 2
print(f"Has C: {graph.get_node_by_type(var('C')) is not None}")  # Output: False

Example 4: Building a Proof Tree

Create a structure representing logical derivations:

from implicational_logic_graph import (
    Graph, var, app, node, edge, Combinator
)

# Create a graph representing a proof
graph = Graph()

# Axioms (base types)
P = var("P")
Q = var("Q")
R = var("R")

# Derived types (implications)
PQ = app(P, Q)      # P -> Q
QR = app(Q, R)      # Q -> R
PR = app(P, R)      # P -> R (conclusion)

# Create nodes for each type in the proof
nodes_dict = {
    "P": node(P),
    "Q": node(Q),
    "R": node(R),
    "P->Q": node(PQ),
    "Q->R": node(QR),
    "P->R": node(PR),
}

# Add all nodes
with graph.connect() as conn:
    for n in nodes_dict.values():
        conn.add_node(n)

# Add inference rules as edges
with graph.connect() as conn:
    # Modus Ponens: P, P->Q ⊢ Q
    mp1 = Combinator(name="MP1", type=app(P, Q))
    conn.add_edge(edge(nodes_dict["P"], nodes_dict["Q"], mp1))

    # Modus Ponens: Q, Q->R ⊢ R
    mp2 = Combinator(name="MP2", type=app(Q, R))
    conn.add_edge(edge(nodes_dict["Q"], nodes_dict["R"], mp2))

    # Composition: P->Q, Q->R ⊢ P->R
    comp = Combinator(name="Comp", type=app(P, R))
    conn.add_edge(edge(nodes_dict["P"], nodes_dict["R"], comp))

print(f"Proof tree has {graph.node_count()} types")
print(f"Proof tree has {graph.edge_count()} inference rules")

# Validate the proof structure
graph.validate()
print("Proof structure is valid!")

Example 5: Exploring Graph Structure

Navigate and analyze the graph:

from implicational_logic_graph import (
    Graph, var, app, node, edge, Combinator
)

# Build a diamond-shaped graph
#     A
#    / \
#   B   C
#    \ /
#     D

graph = Graph()

A, B, C, D = var("A"), var("B"), var("C"), var("D")
n_a, n_b, n_c, n_d = node(A), node(B), node(C), node(D)

with graph.connect() as conn:
    conn.add_node(n_a)
    conn.add_node(n_b)
    conn.add_node(n_c)
    conn.add_node(n_d)

    # A -> B, A -> C
    conn.add_edge(edge(n_a, n_b, Combinator("f1", app(A, B))))
    conn.add_edge(edge(n_a, n_c, Combinator("f2", app(A, C))))

    # B -> D, C -> D
    conn.add_edge(edge(n_b, n_d, Combinator("g1", app(B, D))))
    conn.add_edge(edge(n_c, n_d, Combinator("g2", app(C, D))))

# Analyze the structure
print("=== Graph Analysis ===")
print(f"Total nodes: {graph.node_count()}")
print(f"Total edges: {graph.edge_count()}")

# Find all paths from A
print("\nFrom A:")
for e in graph.get_outgoing_edges(n_a.uid):
    print(f"  -> {e.dst_node.type} via {e.combinator.name}")

# Find all paths to D
print("\nTo D:")
for e in graph.get_incoming_edges(n_d.uid):
    print(f"  <- {e.src_node.type} via {e.combinator.name}")

# Check connectivity
print("\nNode connectivity:")
for n in graph.nodes():
    incoming = len(graph.get_incoming_edges(n.uid))
    outgoing = len(graph.get_outgoing_edges(n.uid))
    print(f"  {n.type}: {incoming} in, {outgoing} out")

API Reference

Types Module (types)

• var(name: str) -> Variable: Create a type variable
• app(input_type: BaseType, output_type: BaseType) -> Application: Create a function type
• Variable: Atomic type variable
• Application: Function application type

Combinator Module (combinator)

• S(A, B, C) -> Combinator: Create S combinator
• K(A, B) -> Combinator: Create K combinator
• Combinator: Generic combinator with name and type

Graph Elements Module (graph_elements)

• node(type: BaseType) -> Node: Create a node
• edge(src: Node, dst: Node, comb: Combinator) -> Edge: Create an edge
• Node: Graph node representing a type
• Edge: Graph edge representing a transformation

Graph Module (graph)

• Graph(): Create a new empty graph
• graph.connect() -> Connection: Create a transactional connection
• graph.validate() -> bool: Validate graph consistency
• graph.has_node(uid: str) -> bool: Check if node exists
• graph.get_node(uid: str) -> Node: Get node by UID
• graph.get_node_by_type(type: BaseType) -> Optional[Node]: Get node by type
• graph.get_outgoing_edges(uid: str) -> list[Edge]: Get outgoing edges
• graph.get_incoming_edges(uid: str) -> list[Edge]: Get incoming edges
• graph.nodes() -> Iterator[Node]: Iterate over nodes
• graph.edges() -> Iterator[Edge]: Iterate over edges
• graph.node_count() -> int: Get number of nodes
• graph.edge_count() -> int: Get number of edges

Connection Module (connection)

• Connection: Transactional graph modification context
• conn.add_node(node: Node) -> Connection: Queue node addition
• conn.add_edge(edge: Edge) -> Connection: Queue edge addition
• conn.remove_node(uid: str) -> Connection: Queue node removal
• conn.remove_edge(uid: str) -> Connection: Queue edge removal
• conn.commit(): Apply all queued operations
• conn.rollback(): Discard all queued operations

Development

Setup

# Clone the repository
git clone https://github.com/yourusername/implicational-logic-graph.git
cd implicational-logic-graph

# Install dependencies
poetry install

# Run tests
poetry run pytest

# Run tests with coverage
poetry run pytest --cov=src/implicational_logic_graph

Running Tests

# Run all tests
poetry run pytest

# Run specific test file
poetry run pytest tests/test_graph.py

# Run with verbose output
poetry run pytest -v

# Run with coverage report
poetry run pytest --cov=src/implicational_logic_graph --cov-report=html

Contributing

Contributions are welcome! Please feel free to submit a Pull Request.

1. Fork the repository
2. Create your feature branch (git checkout -b feature/amazing-feature)
3. Commit your changes (git commit -m 'Add some amazing feature')
4. Push to the branch (git push origin feature/amazing-feature)
5. Open a Pull Request

License

This project is licensed under the MIT License - see the LICENSE file for details.

Acknowledgments

• Based on concepts from combinatory logic and type theory
• Inspired by minimal implicational logic models
• Built with Pydantic for data validation

Citation

If you use this library in your research, please cite:

@software{implicational_logic_graph,
  author = {Carlos Fernandez},
  title = {Implicational Logic Graph},
  year = {2024},
  url = {https://github.com/yourusername/implicational-logic-graph}
}