Interaction calculus in C

interaction.c

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

// Raw dog Interaction Calculus demo in C
// Demonstrates superpositions (SUP), lambdas, apps, global scoping via env
// Uses function pointers for reduction rules and term kinds

typedef enum {
    TERM_VAR,
    TERM_ERA,   // Erasure *
    TERM_LAM,
    TERM_APP,
    TERM_SUP    // Superposition &label{ t0, t1 }
} TermKind;

typedef struct Term Term;

struct Term {
    TermKind kind;
    char* name;         // for VAR or LAM
    int label;          // for SUP
    Term* left;         // APP left, SUP t0, LAM body
    Term* right;        // APP right, SUP t1
    // For global scoping simulation
    void* env;          // opaque env pointer
};

// Constructor helpers
Term* make_var(const char* name) {
    Term* t = malloc(sizeof(Term));
    t->kind = TERM_VAR;
    t->name = strdup(name);
    t->left = t->right = NULL;
    t->label = 0;
    t->env = NULL;
    return t;
}

Term* make_era() {
    Term* t = malloc(sizeof(Term));
    t->kind = TERM_ERA;
    t->name = NULL;
    t->left = t->right = NULL;
    t->label = 0;
    t->env = NULL;
    return t;
}

Term* make_lam(const char* name, Term* body) {
    Term* t = malloc(sizeof(Term));
    t->kind = TERM_LAM;
    t->name = strdup(name);
    t->left = body;
    t->right = NULL;
    t->label = 0;
    t->env = NULL;
    return t;
}

Term* make_app(Term* left, Term* right) {
    Term* t = malloc(sizeof(Term));
    t->kind = TERM_APP;
    t->name = NULL;
    t->left = left;
    t->right = right;
    t->label = 0;
    t->env = NULL;
    return t;
}

Term* make_sup(int label, Term* t0, Term* t1) {
    Term* t = malloc(sizeof(Term));
    t->kind = TERM_SUP;
    t->name = NULL;
    t->label = label;
    t->left = t0;
    t->right = t1;
    t->env = NULL;
    return t;
}

// Simple printer
void print_term(Term* t) {
    if (!t) { printf("NULL"); return; }
    switch (t->kind) {
        case TERM_VAR: printf("%s", t->name); break;
        case TERM_ERA: printf("*"); break;
        case TERM_LAM: printf("λ%s.", t->name); print_term(t->left); break;
        case TERM_APP: printf("("); print_term(t->left); printf(" "); print_term(t->right); printf(")"); break;
        case TERM_SUP: printf("&%d{", t->label); print_term(t->left); printf(","); print_term(t->right); printf("}"); break;
    }
}

// Basic reduction rules via function pointer style (for extensibility)
typedef Term* (*Reducer)(Term*);

// Example reduction: APP-SUP interaction (superposition distributes over application)
Term* reduce_app_sup(Term* app) {
    if (app->kind != TERM_APP) return app;
    if (app->left->kind == TERM_SUP) {
        Term* sup = app->left;
        // ( &L {a,b}  c )  ->  &L { (a c), (b c) }
        Term* new_left = make_app(sup->left, app->right);  // shallow, demo only
        Term* new_right = make_app(sup->right, app->right);
        Term* new_sup = make_sup(sup->label, new_left, new_right);
        // Free old? In real: proper GC, here demo leak ok
        return new_sup;
    }
    return app;
}

// DUP-SUP like for global lambda scoping simulation
Term* global_dup_sup(Term* t) {
    if (t->kind == TERM_SUP) {
        printf("Duplicating superposition globally: ");
        print_term(t);
        printf("\n");
    }
    return t;
}

// Test harness
void run_test(const char* name, Term* t, Reducer reducer) {
    printf("\n=== %s ===\nInput: ", name);
    print_term(t);
    printf("\n");
    Term* reduced = reducer(t);
    printf("Reduced: ");
    print_term(reduced);
    printf("\n");
}

int main() {
    printf("Interaction Calculus Demo in raw C - Superpositions + Lambdas\n\n");

    // Test 1: Simple superposition
    Term* var_x = make_var("x");
    Term* var_y = make_var("y");
    Term* sup1 = make_sup(42, var_x, var_y);
    run_test("Basic SUP", sup1, global_dup_sup);

    // Test 2: APP on SUP -> distribution
    Term* var_z = make_var("z");
    Term* app_sup = make_app(sup1, var_z);  // reuse sup1 (shallow demo)
    run_test("APP-SUP distribution", app_sup, reduce_app_sup);

    // Test 3: Lambda with global scope sim
    Term* body = make_app(make_var("f"), make_sup(7, make_var("a"), make_var("b")));
    Term* lam_global = make_lam("f", body);
    printf("\n=== Global Lambda with SUP ===\n");
    print_term(lam_global);
    printf("\n");

    // Clean up omitted for brevity (real code needs free_term recursive)

    printf("\nThis shows C can directly implement SUP rules, global lambdas via env/closures, and reductions.\n");
    printf("Function pointers allow extensible rule application for full Interaction Calculus.\n");
    printf("SupGen-like brute force synthesis could extend this with search over term rewrites.\n");

    return 0;
}