implicational-logic-graph 0.2.0
A package for working with graphs representing minimal implicational logic models
Requires Python: <4.0,>=3.10

# 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.

[![Python 3.10+](https://img.shields.io/badge/python-3.10+-blue.svg)](https://www.python.org/downloads/)
[![License](https://img.shields.io/badge/license-MIT-green.svg)](LICENSE)

## 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)

```bash
poetry add implicational-logic-graph
```

### Using pip

```bash
pip install implicational-logic-graph
```

### From source

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

## Quick Start

```python
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`

```python
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:

```python
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:

```python
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:

```python
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

```python
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

```python
# 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

```python
# 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:

```python
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:

```python
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:

```python
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:

```python
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:

```python
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

```bash
# Clone the repository
git clone https://github.com/carlosFerLo/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

```bash
# 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](LICENSE) file for details.

## Acknowledgments

- Based on concepts from combinatory logic and type theory
- Inspired by minimal implicational logic models
- Built with [Pydantic](https://pydantic-docs.helpmanual.io/) for data validation

## Citation

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

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