implica 0.4.0

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

Parsing Types from Strings

You can also create types by parsing string representations using type_from_string():

import implica as imp

# Parse simple variables
A = imp.type_from_string("A")
print(A)  # Output: A

# Parse function types
func = imp.type_from_string("A -> B")
print(func)  # Output: A -> B

# Parse nested types with right-associativity
nested = imp.type_from_string("A -> B -> C")
print(nested)  # Output: A -> B -> C
# This is equivalent to: A -> (B -> C)

# Parse with explicit parentheses
left_assoc = imp.type_from_string("(A -> B) -> C")
print(left_assoc)  # Output: (A -> B) -> C

# Parse complex nested types
complex = imp.type_from_string("((A -> B) -> C) -> (D -> E)")
print(complex)  # Output: ((A -> B) -> C) -> D -> E

# Multi-character variable names
person_func = imp.type_from_string("Person -> String")
print(person_func)  # Output: Person -> String

# Variables with numbers and underscores
data_type = imp.type_from_string("data_1 -> result_2")
print(data_type)  # Output: data_1 -> result_2

# Unicode characters are supported
greek = imp.type_from_string("α -> β -> γ")
print(greek)  # Output: α -> β -> γ

Parsing rules:

• The arrow operator -> is right-associative: A -> B -> C is parsed as A -> (B -> C)
• Use parentheses to override associativity: (A -> B) -> C
• Variable names can contain letters, numbers, and underscores
• Whitespace is ignored: A->B and A -> B are equivalent
• Unicode characters in variable names are supported

Error handling:

import implica as imp

# Empty string raises ValueError
try:
    imp.type_from_string("")
except ValueError as e:
    print(f"Error: {e}")  # Error: Type string cannot be empty

# Mismatched parentheses
try:
    imp.type_from_string("(A -> B")
except ValueError as e:
    print(f"Error: {e}")  # Error: Mismatched parentheses

# Invalid characters
try:
    imp.type_from_string("A @ B")
except ValueError as e:
    print(f"Error: {e}")  # Error: Invalid character '@' at position 2

# Missing operand
try:
    imp.type_from_string("A ->")
except ValueError as e:
    print(f"Error: {e}")  # Error: Unexpected end of input

Use cases:

• Parse type expressions from configuration files or user input
• Create types dynamically from strings
• Simplify type construction with readable syntax
• Testing and debugging with human-readable type representations

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

Example 11: Using type_from_string for Dynamic Type Creation

Parse types from strings for flexible, dynamic type construction:

import implica as imp

# Create a graph
graph = imp.Graph()

# Define type expressions as strings (e.g., from a config file or user input)
type_strings = [
    "Person",
    "String",
    "Int",
    "Person -> String",  # Get name
    "Person -> Int",     # Get age
    "(Person -> String) -> (Person -> Int) -> Person",  # Complex transformation
]

# Parse and add all types to the graph
nodes = []
for type_str in type_strings:
    parsed_type = imp.type_from_string(type_str)
    node = imp.node(parsed_type)
    nodes.append(node)

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

print(f"Created graph with {graph.node_count()} nodes from string definitions")
# Output: Created graph with 6 nodes from string definitions

# You can also build a type library from a configuration
type_library = {
    "identity": "A -> A",
    "const": "A -> B -> A",
    "compose": "(B -> C) -> (A -> B) -> A -> C",
    "apply": "(A -> B) -> A -> B",
}

print("\n=== Type Library ===")
for name, type_str in type_library.items():
    parsed = imp.type_from_string(type_str)
    print(f"{name:10} : {parsed}")

# Output:
# identity   : A -> A
# const      : A -> B -> A
# compose    : (B -> C) -> (A -> B) -> A -> C
# apply      : (A -> B) -> A -> B

# Validate type strings from user input
def validate_and_parse_type(user_input: str) -> tuple[bool, str, object]:
    """
    Validate and parse a type string from user input.
    Returns (is_valid, message, parsed_type)
    """
    try:
        parsed = imp.type_from_string(user_input)
        return True, f"Valid type: {parsed}", parsed
    except ValueError as e:
        return False, f"Invalid type: {e}", None

# Test validation
test_inputs = [
    "A -> B",
    "(A -> B) -> C",
    "A ->",  # Invalid
    "Person -> (Address -> String)",
    "A @ B",  # Invalid
]

print("\n=== Type Validation ===")
for test in test_inputs:
    is_valid, message, parsed = validate_and_parse_type(test)
    status = "✓" if is_valid else "✗"
    print(f"{status} '{test:30}' : {message}")

# Output:
# ✓ 'A -> B'                      : Valid type: A -> B
# ✓ '(A -> B) -> C'               : Valid type: (A -> B) -> C
# ✗ 'A ->'                        : Invalid type: Unexpected end of input
# ✓ 'Person -> (Address -> String)' : Valid type: Person -> Address -> String
# ✗ 'A @ B'                       : Invalid type: Invalid character '@' at position 2

# Build a type inference system
def infer_result_type(func_type_str: str, input_type_str: str) -> str:
    """
    Given a function type and an input type, infer the result type.
    Returns the result type as a string, or an error message.
    """
    try:
        func_type = imp.type_from_string(func_type_str)
        input_type = imp.type_from_string(input_type_str)

        # Check if func_type is an application
        if not isinstance(func_type, imp.Application):
            return f"Error: {func_type_str} is not a function type"

        # Check if input matches function's input type
        if func_type.input_type.uid != input_type.uid:
            return f"Error: Type mismatch. Expected {func_type.input_type}, got {input_type}"

        return str(func_type.output_type)
    except ValueError as e:
        return f"Error: {e}"

# Test type inference
print("\n=== Type Inference ===")
print(f"Apply 'A -> B' to 'A': {infer_result_type('A -> B', 'A')}")
# Output: B

print(f"Apply 'Person -> String' to 'Person': {infer_result_type('Person -> String', 'Person')}")
# Output: String

print(f"Apply 'A -> B -> C' to 'A': {infer_result_type('A -> B -> C', 'A')}")
# Output: B -> C

print(f"Apply 'A -> B' to 'C': {infer_result_type('A -> B', 'C')}")
# Output: Error: Type mismatch. Expected A, got C

# Parse types from a domain-specific language
dsl_program = """
    define Input
    define Output
    define Processor = Input -> Output
    define Chain = Processor -> Processor -> Processor
"""

print("\n=== Parsing DSL ===")
for line in dsl_program.strip().split('\n'):
    line = line.strip()
    if line.startswith("define "):
        parts = line[7:].split(" = ")
        type_name = parts[0].strip()

        if len(parts) == 1:
            # Simple type definition
            print(f"{type_name}: <primitive type>")
        else:
            # Complex type definition
            type_expr = parts[1].strip()
            parsed = imp.type_from_string(type_expr)
            print(f"{type_name}: {parsed}")

# Output:
# Input: <primitive type>
# Output: <primitive type>
# Processor: Input -> Output
# Chain: Processor -> Processor -> Processor

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
• type_from_string(type_str: str) -> BaseType: Parse a type from a string representation
• 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

Utilities Module (implica.utils)

Parsing Functions:

• tokenize(type_str: str) -> list[str]: Tokenize a type string into tokens
  • Returns a list of tokens: variable names, '(', ')', and '->'
  • Raises ValueError if invalid characters are found
• parse_type(tokens: list[str]) -> tuple[BaseType, list[str]]: Parse tokens into a type
  • Uses recursive descent parsing with right-associativity for arrows
  • Returns the parsed type and any remaining tokens
  • Raises ValueError if tokens cannot be parsed
• parse_primary(tokens: list[str]) -> tuple[BaseType, list[str]]: Parse a primary type
  • Handles variables and parenthesized types
  • Returns the parsed type and remaining tokens
  • Raises ValueError if tokens cannot be parsed

Note: These functions are primarily used internally by type_from_string(), but are exposed for advanced use cases where you need direct control over the parsing process.

Example:

from implica.utils import tokenize, parse_type

# Tokenize a type string
tokens = tokenize("(A -> B) -> C")
print(tokens)  # Output: ['(', 'A', '->', 'B', ')', '->', 'C']

# Parse the tokens
type_result, remaining = parse_type(tokens)
print(type_result)  # Output: (A -> B) -> C
print(remaining)    # Output: []

# Custom parsing workflow
def parse_and_validate(type_str: str) -> bool:
    """Check if a string is a valid type expression."""
    try:
        tokens = tokenize(type_str)
        result, remaining = parse_type(tokens)
        return len(remaining) == 0  # Valid if no tokens remain
    except ValueError:
        return False

print(parse_and_validate("A -> B"))      # Output: True
print(parse_and_validate("A ->"))        # Output: False
print(parse_and_validate("(A -> B) -> C"))  # Output: True

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}
}