implica 0.3.4

A package for working with graphs representing minimal implicational logic models

Implica

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.

Import as imp for a clean, concise API!

Features

• 🎯 Type System: Build complex type expressions using variables and applications (function types)
• 🔍 Variable Extraction: Recursively extract all variables from any type expression
• 🧩 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
• 📦 Bulk Operations: Add multiple nodes or edges atomically with add_many_nodes and add_many_edges
• 🛡️ Idempotent Mutations: Use try_add_node and try_add_edge for safe, duplicate-tolerant operations
• ✅ 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 implica

Using pip

pip install implica

From source

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

Quick Start

import implica as imp

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

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

# Create a graph with nodes
graph = imp.Graph()
with graph.connect() as conn:
    conn.add_node(imp.node(A))
    conn.add_node(imp.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

import implica as imp

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

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

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

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

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

Extracting Variables from Types

Every type has a variables property that returns a list of all variables contained in that type. This is computed recursively and may include duplicate variables if they appear multiple times:

import implica as imp

# Simple variable returns itself
A = imp.var("A")
print(A.variables)  # Output: [Variable(name='A')]

# Application returns all variables from both input and output
B = imp.var("B")
func = imp.app(A, B)
print([v.name for v in func.variables])  # Output: ['A', 'B']

# Nested types return all variables recursively
C = imp.var("C")
nested = imp.app(imp.app(A, B), C)  # (A -> B) -> C
print([v.name for v in nested.variables])  # Output: ['A', 'B', 'C']

# Duplicates are included
same_var = imp.app(A, A)  # A -> A
print([v.name for v in same_var.variables])  # Output: ['A', 'A']

# Complex example with duplicates
complex = imp.app(imp.app(A, B), A)  # (A -> B) -> A
print([v.name for v in complex.variables])  # Output: ['A', 'B', 'A']

Use cases:

• Analyze which variables are used in a complex type expression
• Count occurrences of specific variables in a type
• Validate that certain variables are present or absent
• Generate variable lists for quantification or substitution operations

Combinators

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

import implica as imp

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

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

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

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

Graph Elements

Nodes

Nodes represent types in the graph:

import implica as imp

A = imp.var("A")
B = imp.var("B")

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

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

Edges

Edges represent combinator transformations between types:

import implica as imp

A = imp.var("A")
B = imp.var("B")

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

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

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

Graph Operations

Creating and Modifying Graphs

import implica as imp

# Create an empty graph
graph = imp.Graph()

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

n_a = imp.node(A)
n_b = imp.node(B)
n_c = imp.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 = imp.Combinator(name="f", type=imp.app(A, B))
comb_bc = imp.Combinator(name="g", type=imp.app(B, C))

with graph.connect() as conn:
    conn.add_edge(imp.edge(n_a, n_b, comb_ab))
    conn.add_edge(imp.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}")

Advanced Mutations

The library provides several mutation types for flexible graph modifications:

Bulk Mutations

Add multiple nodes or edges in a single atomic operation:

import implica as imp

graph = imp.Graph()

# Create multiple nodes
nodes = [imp.node(imp.var(f"T{i}")) for i in range(5)]

# Add all nodes atomically - if any fails, all are rolled back
with graph.connect() as conn:
    conn.add_many_nodes(nodes)

# Create multiple edges
A, B, C = imp.var("A"), imp.var("B"), imp.var("C")
combinators = [
    imp.Combinator("f1", imp.app(A, B)),
    imp.Combinator("f2", imp.app(B, C)),
]

# Add all edges atomically
with graph.connect() as conn:
    conn.add_many_edges(combinators)

Benefits:

• All-or-nothing semantics: if any operation fails, all are rolled back
• More efficient than individual additions
• Cleaner code for batch operations

Removal Operations:

The same bulk operations are available for removing nodes and edges:

# Remove multiple nodes at once
node_uids = [n.uid for n in nodes[:3]]
with graph.connect() as conn:
    conn.remove_many_nodes(node_uids)

# Remove multiple edges at once
edge_uids = [e.uid for e in some_edges]
with graph.connect() as conn:
    conn.remove_many_edges(edge_uids)

Idempotent Mutations

Use safe mutations that don't fail when items already exist or don't exist:

import implica as imp

graph = imp.Graph()

A = imp.var("A")
n_a = imp.node(A)

# Regular add would fail on duplicate
with graph.connect() as conn:
    conn.add_node(n_a)

# try_add_node won't fail if node exists
with graph.connect() as conn:
    conn.try_add_node(n_a)  # No error, even though n_a exists

# Same with edges
B = imp.var("B")
with graph.connect() as conn:
    conn.try_add_node(imp.node(B))

comb = imp.Combinator("f", imp.app(A, B))
with graph.connect() as conn:
    conn.try_add_edge(comb)  # Adds the edge

with graph.connect() as conn:
    conn.try_add_edge(comb)  # No error, edge already exists

# Safe removal operations
with graph.connect() as conn:
    conn.try_remove_node(n_a.uid)  # Removes the node

with graph.connect() as conn:
    conn.try_remove_node(n_a.uid)  # No error, node doesn't exist anymore

# Same with edges
with graph.connect() as conn:
    conn.try_remove_edge("some_edge_uid")  # No error even if edge doesn't exist

Use Cases:

• Building graphs from multiple sources where duplicates may occur
• Idempotent initialization routines
• Avoiding explicit existence checks before adding or removing elements
• Incremental graph construction without duplicate errors
• Cleanup operations that should be safe to run multiple times

Usage Examples

Example 1: Simple Type Chain

Build a chain of type transformations:

import implica as imp

# Create graph
graph = imp.Graph()

# Define types
types = [imp.var(name) for name in ["A", "B", "C", "D"]]
nodes = [imp.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 = imp.Combinator(
            name=f"f{i}",
            type=imp.app(types[i], types[i + 1])
        )
        conn.add_edge(imp.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(imp.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:

import implica as imp

# Create graph
graph = imp.Graph()

# Define type variables
A = imp.var("A")
B = imp.var("B")
C = imp.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 = imp.app(A, B)
t4 = imp.app(t3, C)

nodes = [imp.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 = imp.S(A, B, C)
k_comb = imp.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:

import implica as imp

graph = imp.Graph()

A = imp.var("A")
B = imp.var("B")
n_a = imp.node(A)
n_b = imp.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 = imp.var("C")
        n_c = imp.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(imp.var('C')) is not None}")  # Output: False

Example 4: Building a Proof Tree

Create a structure representing logical derivations:

import implica as imp

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

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

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

# Create nodes for each type in the proof
nodes_dict = {
    "P": imp.node(P),
    "Q": imp.node(Q),
    "R": imp.node(R),
    "P->Q": imp.node(PQ),
    "Q->R": imp.node(QR),
    "P->R": imp.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 = imp.Combinator(name="MP1", type=imp.app(P, Q))
    conn.add_edge(imp.edge(nodes_dict["P"], nodes_dict["Q"], mp1))

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

    # Composition: P->Q, Q->R ⊢ P->R
    comp = imp.Combinator(name="Comp", type=imp.app(P, R))
    conn.add_edge(imp.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:

import implica as imp

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

graph = imp.Graph()

A, B, C, D = imp.var("A"), imp.var("B"), imp.var("C"), imp.var("D")
n_a, n_b, n_c, n_d = imp.node(A), imp.node(B), imp.node(C), imp.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(imp.edge(n_a, n_b, imp.Combinator("f1", imp.app(A, B))))
    conn.add_edge(imp.edge(n_a, n_c, imp.Combinator("f2", imp.app(A, C))))

    # B -> D, C -> D
    conn.add_edge(imp.edge(n_b, n_d, imp.Combinator("g1", imp.app(B, D))))
    conn.add_edge(imp.edge(n_c, n_d, imp.Combinator("g2", imp.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")

Example 6: Bulk Operations

Add multiple nodes and edges efficiently:

import implica as imp

graph = imp.Graph()

# Create many type variables at once
type_vars = [imp.var(f"T{i}") for i in range(10)]
nodes = [imp.node(t) for t in type_vars]

# Add all nodes in a single transaction
with graph.connect() as conn:
    conn.add_many_nodes(nodes)

print(f"Added {graph.node_count()} nodes in one operation")

# Create a chain of transformations
combinators = []
for i in range(len(type_vars) - 1):
    comb = imp.Combinator(
        name=f"f{i}",
        type=imp.app(type_vars[i], type_vars[i + 1])
    )
    combinators.append(comb)

# Add all edges in a single transaction
with graph.connect() as conn:
    conn.add_many_edges(combinators)

print(f"Added {graph.edge_count()} edges in one operation")

# If any node or edge fails, all are rolled back atomically
try:
    with graph.connect() as conn:
        # This will fail because nodes[0] already exists
        conn.add_many_nodes([nodes[0], imp.node(imp.var("NEW"))])
except RuntimeError:
    print("Transaction rolled back - no new nodes added")

Example 7: Idempotent Operations

Use safe mutations that don't fail on duplicates:

import implica as imp

graph = imp.Graph()

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

# Add nodes normally
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 nodes again - won't fail!
with graph.connect() as conn:
    conn.try_add_node(n_a)  # Already exists, but no error
    conn.try_add_node(n_b)  # Already exists, but no error
    conn.try_add_node(imp.node(imp.var("C")))  # New node, will be added

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

# Same with edges
comb_ab = imp.Combinator("f", imp.app(A, B))

with graph.connect() as conn:
    conn.try_add_edge(comb_ab)  # Will be added

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

with graph.connect() as conn:
    conn.try_add_edge(comb_ab)  # Already exists, but no error

print(f"Edges after try_add: {graph.edge_count()}")  # Output: 1

# Useful for idempotent operations and avoiding duplicate checks
def ensure_basic_types(graph, type_names):
    """Ensure all basic types exist in the graph."""
    with graph.connect() as conn:
        for name in type_names:
            conn.try_add_node(imp.node(imp.var(name)))

# Can call this multiple times safely
ensure_basic_types(graph, ["A", "B", "C", "D"])
ensure_basic_types(graph, ["C", "D", "E", "F"])  # C and D won't cause errors

print(f"Final nodes: {graph.node_count()}")  # Output: 6 (A, B, C, D, E, F)

Example 8: Bulk Removal Operations

Remove multiple elements efficiently:

import implica as imp

graph = imp.Graph()

# Build a graph with multiple nodes and edges
types = [imp.var(f"T{i}") for i in range(10)]
nodes = [imp.node(t) for t in types]

with graph.connect() as conn:
    conn.add_many_nodes(nodes)

# Create edges
combinators = []
for i in range(len(types) - 1):
    comb = imp.Combinator(f"f{i}", imp.app(types[i], types[i + 1]))
    combinators.append(comb)

with graph.connect() as conn:
    conn.add_many_edges(combinators)

print(f"Initial: {graph.node_count()} nodes, {graph.edge_count()} edges")
# Output: Initial: 10 nodes, 9 edges

# Remove multiple edges at once
edge_uids = [graph.get_outgoing_edges(nodes[i].uid)[0].uid for i in range(3)]
with graph.connect() as conn:
    conn.remove_many_edges(edge_uids)

print(f"After edge removal: {graph.edge_count()} edges")
# Output: After edge removal: 6 edges

# Remove multiple nodes at once (and their connected edges)
node_uids = [nodes[i].uid for i in range(5)]
with graph.connect() as conn:
    conn.remove_many_nodes(node_uids)

print(f"After node removal: {graph.node_count()} nodes, {graph.edge_count()} edges")
# Output: After node removal: 5 nodes, 0 edges (edges were connected to removed nodes)

# Safe removal with try_remove (won't fail if already removed)
with graph.connect() as conn:
    conn.try_remove_node(nodes[0].uid)  # Already removed, no error
    conn.try_remove_edge("nonexistent_uid")  # Doesn't exist, no error

print(f"Final: {graph.node_count()} nodes")  # Output: Final: 5 nodes

Example 9: Safe Cleanup Operations

Use idempotent removal for cleanup tasks:

import implica as imp

def cleanup_temporary_nodes(graph, temp_node_uids):
    """
    Remove temporary nodes if they exist.
    This function is safe to call multiple times.
    """
    with graph.connect() as conn:
        for uid in temp_node_uids:
            conn.try_remove_node(uid)

graph = imp.Graph()

# Add some nodes
A, B, C = imp.var("A"), imp.var("B"), imp.var("C")
n_a, n_b, n_c = imp.node(A), imp.node(B), imp.node(C)

with graph.connect() as conn:
    conn.add_many_nodes([n_a, n_b, n_c])

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

# Clean up - safe to call multiple times
temp_uids = [n_a.uid, n_b.uid]
cleanup_temporary_nodes(graph, temp_uids)
print(f"After cleanup: {graph.node_count()}")  # Output: 1

# Call again - won't fail even though nodes are already removed
cleanup_temporary_nodes(graph, temp_uids)
print(f"After second cleanup: {graph.node_count()}")  # Output: 1

# Combine try_remove with try_add for flexible graph updates
def ensure_graph_state(graph, required_nodes, forbidden_nodes):
    """
    Ensure graph has required nodes and doesn't have forbidden ones.
    """
    with graph.connect() as conn:
        # Add required nodes (idempotent)
        for n in required_nodes:
            conn.try_add_node(n)

        # Remove forbidden nodes (idempotent)
        for uid in forbidden_nodes:
            conn.try_remove_node(uid)

# Can call this function repeatedly to maintain desired state
ensure_graph_state(
    graph,
    required_nodes=[imp.node(imp.var("X")), imp.node(imp.var("Y"))],
    forbidden_nodes=[n_c.uid]
)

print(f"Final state: {graph.node_count()} nodes")  # Output: 2 (X and Y)

Example 10: Analyzing Type Variables

Extract and analyze variables from complex type expressions:

import implica as imp

# Create a complex type expression
A = imp.var("A")
B = imp.var("B")
C = imp.var("C")

# ((A -> B) -> C) -> (A -> B)
inner = imp.app(A, B)
middle = imp.app(inner, C)
complex_type = imp.app(middle, inner)

print(f"Type: {complex_type}")
# Output: ((A -> B) -> C) -> A -> B

# Get all variables (including duplicates)
variables = complex_type.variables
print(f"All variables: {[v.name for v in variables]}")
# Output: ['A', 'B', 'C', 'A', 'B']

# Count unique variables
unique_vars = {v.name for v in variables}
print(f"Unique variables: {unique_vars}")
# Output: {'A', 'B', 'C'}

# Count occurrences
from collections import Counter
var_counts = Counter(v.name for v in variables)
print(f"Variable counts: {dict(var_counts)}")
# Output: {'A': 2, 'B': 2, 'C': 1}

# Check if a specific variable is used
def uses_variable(type_expr, var_name):
    """Check if a type expression uses a specific variable."""
    return any(v.name == var_name for v in type_expr.variables)

print(f"Uses A: {uses_variable(complex_type, 'A')}")  # Output: True
print(f"Uses D: {uses_variable(complex_type, 'D')}")  # Output: False

# Find all types in a graph that use a specific variable
graph = imp.Graph()

# Create various types
types_to_add = [
    imp.var("X"),
    imp.var("Y"),
    imp.app(A, B),
    imp.app(B, C),
    imp.app(A, imp.app(B, C)),
]

with graph.connect() as conn:
    for t in types_to_add:
        conn.add_node(imp.node(t))

# Find all nodes containing variable "B"
nodes_with_B = [
    n for n in graph.nodes()
    if any(v.name == "B" for v in n.type.variables)
]

print(f"\nNodes containing variable B:")
for n in nodes_with_B:
    print(f"  - {n.type}")
# Output:
#   - A -> B
#   - B -> C
#   - A -> B -> C

# Calculate the "complexity" of a type by counting its variables
def type_complexity(type_expr):
    """Calculate complexity as the total number of variables."""
    return len(type_expr.variables)

print(f"\nType complexities:")
for n in graph.nodes():
    print(f"  {n.type}: {type_complexity(n.type)}")
# Output:
#   X: 1
#   Y: 1
#   A -> B: 2
#   B -> C: 2
#   A -> B -> C: 3

API Reference

Core Module (implica.core)

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
  • name: str: The name of the variable
  • uid: str: Unique identifier (SHA256 hash)
  • variables: list[Variable]: Returns [self]
• Application: Function application type
  • input_type: BaseType: Input type of the function
  • output_type: BaseType: Output type of the function
  • uid: str: Unique identifier (SHA256 hash)
  • variables: list[Variable]: Returns all variables from input and output types (may include duplicates)

Combinators:

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

Graph Module (implica.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:

• 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:

• 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.add_many_nodes(nodes: list[Node]) -> Connection: Queue multiple node additions
• conn.add_many_edges(combinators: list[Combinator]) -> Connection: Queue multiple edge additions
• conn.try_add_node(node: Node) -> Connection: Queue node addition (no error if exists)
• conn.try_add_edge(combinator: Combinator) -> Connection: Queue edge addition (no error if exists)
• conn.remove_many_nodes(node_uids: list[str]) -> Connection: Queue multiple node removals
• conn.remove_many_edges(edge_uids: list[str]) -> Connection: Queue multiple edge removals
• conn.try_remove_node(node_uid: str) -> Connection: Queue node removal (no error if not exists)
• conn.try_remove_edge(edge_uid: str) -> Connection: Queue edge removal (no error if not exists)
• conn.commit(): Apply all queued operations
• conn.rollback(): Discard all queued operations

Mutations Module (implica.mutations)

• Mutation: Abstract base class for all mutations
• AddNode(node): Add a single node
• RemoveNode(node_uid): Remove a single node
• AddEdge(edge): Add a single edge
• RemoveEdge(edge_uid): Remove a single edge
• AddManyNodes(nodes): Add multiple nodes atomically
• AddManyEdges(edges): Add multiple edges atomically
• TryAddNode(node): Add a node or do nothing if it exists
• TryAddEdge(edge): Add an edge or do nothing if it exists
• RemoveManyNodes(node_uids): Remove multiple nodes atomically
• RemoveManyEdges(edge_uids): Remove multiple edges atomically
• TryRemoveNode(node_uid): Remove a node or do nothing if it doesn't exist
• TryRemoveEdge(edge_uid): Remove an edge or do nothing if it doesn't exist

Development

Setup

# 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

# 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/implica --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{implica,
  author = {Carlos Fernandez},
  title = {Implica: Implicational Logic Graph Library},
  year = {2025},
  url = {https://github.com/CarlosFerLo/implicational-logic-graph}
}