aygp-dr/fixed-point-explorer

Y combinator and fixed-point recursion exploration across Scheme dialects with formal verification

Fixed Point Explorer

Overview

Fixed Point Explorer is a multi-implementation exploration of the Y combinator and fixed-point recursion patterns in Scheme. The project demonstrates how recursive functions can be built without explicit self-reference, using the Y combinator as a foundation.

Features

• ✨ Portable Y combinator implementation working across multiple Scheme dialects
• 🎯 Pure functional implementations of classic recursive algorithms
• 🔧 Support for GNU Guile, Chez Scheme, and Racket
• 📊 Performance benchmarks and comparisons
• 🧪 Comprehensive test suite with edge case coverage
• 📚 Literate programming approach with Org-mode
• 🔍 Formal verification capabilities (Lean 4 support)

Quick Start

Prerequisites

Check that you have the required dependencies:

gmake deps

Running Tests

# Run all tests
gmake test

# Run tests for specific implementation
gmake test-guile    # Primary implementation
gmake test-chez
gmake test-racket

Interactive REPL

# Start Guile REPL with project loaded
gmake repl-guile

# In the REPL, try:
(load "src/portable/fibonacci.scm")
(fib 10)  ;; => 55
(test-fibonacci)

Project Structure

fixed-point-explorer/
├── src/
│   ├── portable/         # Cross-implementation code
│   │   ├── y-combinator.scm
│   │   ├── fibonacci.scm
│   │   └── list-ops.scm
│   ├── guile/           # Guile-specific extensions
│   ├── chez/            # Chez-specific optimizations
│   └── racket/          # Racket-specific typed versions
├── test/
│   ├── test-framework.scm
│   └── integration/     # Cross-implementation tests
├── scripts/
│   ├── deps.sh          # Dependency checking
│   └── setup.sh         # Tool installation
├── lib/geiser/          # Emacs integration
├── docs/                # Documentation
└── Makefile             # Build automation

Examples

Basic Y Combinator Usage

;; Load the Y combinator
(load "src/portable/y-combinator.scm")

;; Define a recursive function using Y combinator
(define CONTINUE-fact
  (lambda (f)
    (lambda (n)
      (if (= n 0) 
          1 
          (* n (f (- n 1)))))))

(define factorial (Y-explicit CONTINUE-fact))
(factorial 5)  ;; => 120

Fibonacci with Memoization

(load "src/portable/fibonacci.scm")

;; Basic fibonacci
(fib 20)  ;; => 6765

;; Memoized version for better performance
(define memo-fib (make-memoized-fib))
(memo-fib 100)  ;; Computes quickly

List Operations

(load "src/portable/list-ops.scm")

;; All list operations implemented using Y combinator
(append-y '(1 2 3) '(4 5 6))         ;; => (1 2 3 4 5 6)
(map-y (lambda (x) (* x 2)) '(1 2 3)) ;; => (2 4 6)
(filter-y even? '(1 2 3 4 5 6))      ;; => (2 4 6)
(foldr-y + 0 '(1 2 3 4 5))           ;; => 15

Theoretical Background

The Y combinator, discovered by Haskell Curry, enables recursion in languages that don’t have built-in recursion. Its type signature is:

Y : ∀α. ((α → α) → (α → α)) → (α → α)

This project explores practical applications of this theoretical construct across different Scheme implementations.

Implementation Details

Guile (Primary Implementation)

GNU Guile 3.0+ is the primary development platform. All portable code is tested first on Guile.

• Uses string-contains for implementation detection
• Supports performance timing with (ice-9 time)
• Compatible with Geiser for interactive development

Cross-Implementation Compatibility

The portable code avoids implementation-specific features:

• No format in core modules (for maximum compatibility)
• Simple list-based memoization instead of hash tables
• Explicit module loading with load instead of module systems

Performance

Run benchmarks with:

gmake benchmark

Example output (times vary by system):

• Guile: fib(30) in ~0.8s
• Chez: fib(30) in ~0.3s
• Racket: fib(30) in ~1.2s

Development

Building from Source

1. Clone the repository
2. Tangle the literate source (if using SETUP.org):

   # In Emacs: C-c C-v t on SETUP.org
       

3. Run tests:

   gmake test
       

Contributing

1. Ensure all tests pass: gmake test
2. Follow the existing code style
3. Add tests for new functionality
4. Update documentation as needed

Formal Verification (Optional)

For formal verification with Lean 4:

# Install Lean 4 (FreeBSD with Linux compatibility)
gmake setup

# Or manual installation
gmake -f Makefile.lean lean-install

License

This project is licensed under the MIT License. See LICENSE for details.

Acknowledgments

• Y combinator theory from Haskell Curry’s work on combinatory logic
• Inspired by “The Little Schemer” and SICP
• Scheme community for maintaining excellent implementations

Resources

• Fixed-point combinator (Wikipedia)
• SETUP.org - Literate programming source
• Type Specifications - Formal type documentation

—