Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 24 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
name: Go Test

on:
push:
branches: [ main ]
pull_request:
branches: [ main ]

jobs:
test:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4

- name: Set up Go
uses: actions/setup-go@v5
with:
go-version: '1.21'

- name: Install dependencies
run: go mod download

- name: Run tests
run: go test -v ./...
34 changes: 33 additions & 1 deletion GUIDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -414,7 +414,39 @@ Schönfinkel now provides us with the methodology of how to move the the argumen

As far as our implementation goes, we can treat `U` as a constant as it has no meaning that is compatible with our tree definition. Maybe some day I will come back and implement the conversion of first-order logic to combinatory logic and vice versa.

The modern-day interpretation of this section is probably that combinatory logic is useful as an encoding mechanism to get as little syntax overhead as possible (and first-order logic is one such example). I find systems that build on top of the system (like the [Church encoding](https://en.wikipedia.org/wiki/Church_encoding)) much more interesting. Church encoding can be found in [combinator.go](./church.go) and [combinator_test.go](./church_test.go).
The modern-day interpretation of this section is probably that combinatory logic is useful as an encoding mechanism to get as little syntax overhead as possible (and first-order logic is one such example). I find systems that build on top of the system (like the [Church encoding](https://en.wikipedia.org/wiki/Church_encoding)) much more interesting. Church encoding can be found in [combinator.go](./combinator.go) and [combinator_test.go](./combinator_test.go).

### Fixed-point Combinator

A [fixed-point combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator) is a combinator that can be used to implement recursion in a system that doesn't have it built-in. The most famous of these is the **Y Combinator**.

The Y combinator has the property that:

$$Yf = f(Yf)$$

This means that $Yf$ is a fixed point of $f$. In our SKI basis, we can define $Y$ as:

$$Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))$$

(Note: $S(S(KS)K)$ is $Z$ in the Schönfinkel basis, or $B$ in the BCKW basis).

Because $Yf$ expands infinitely, our reduction engine will eventually hit a loop detector or timeout when attempting to fully reduce it. You can see this in action in `TestY` in [combinator_test.go](./combinator_test.go).

### Universal Combinator

A [universal combinator](https://en.wikipedia.org/wiki/Universal_combinator) is a combinator that can represent any other combinator through a specific encoding. Similar to [John Tromp's Binary Lambda Calculus](https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861), we can define an encoding for SKI terms and a universal combinator $U$ to execute them.

Our encoding represents each SKI combinator as a higher-order combinator:
- $enc(S) = \lambda s k i a. s$ (represented as `A` in our implementation)
- $enc(K) = \lambda s k i a. k$ (represented as `B` in our implementation)
- $enc(I) = \lambda s k i a. i$ (represented as `C` in our implementation)
- $enc(MN) = \lambda s k i a. a \ enc(M) \ enc(N)$ (represented as `D` in our implementation)

The universal combinator $U$ is defined such that it decodes these terms and applies the resulting SKI combinators:

$$U = Y (\lambda u e. e \ S \ K \ I \ (\lambda m n. u \ m \ (u \ n)))$$

In our `Universal` basis, you can transform encoded terms back into their SKI counterparts. For example, `ASKII` will reduce to `S`. You can find these examples in `TestUniversal` in [combinator_test.go](./combinator_test.go).

## Section 6

Expand Down
4 changes: 2 additions & 2 deletions TODO.md
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
1. Get [Y Combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator) example
1. Create a Universal Combinator given some encoding, similar to [Tromp's Binary Lambda Calculus universal machine](https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861).
1. [x] Get [Y Combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator) example
1. [x] Create a Universal Combinator given some encoding, similar to [Tromp's Binary Lambda Calculus universal machine](https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0987d861).
55 changes: 54 additions & 1 deletion combinator.go
Original file line number Diff line number Diff line change
Expand Up @@ -56,10 +56,60 @@ var (
Schonfinkel = Basis{I, K, T, Z, S}
)

// Fixed-point (https://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combinator)
var (
Y = Combinator{
Name: "Y",
Arguments: []string{"f"},
Definition: "S(K(SII))(S(S(KS)K)(K(SII)))f",
}
)

// SK and SKI (https://en.wikipedia.org/wiki/SKI_combinator_calculus)
var (
SK = Basis{S, K}
SKI = Basis{S, K, I}
SKI = Basis{S, K, I, Y}
)

// Universal Combinator (https://en.wikipedia.org/wiki/Universal_combinator)
// Based on a higher-order encoding of SKI terms.
var (
// Encoded S: λs k i a. s
ES = Combinator{
Name: "A",
Arguments: []string{"s", "k", "i", "a"},
Definition: "s",
}

// Encoded K: λs k i a. k
EK = Combinator{
Name: "B",
Arguments: []string{"s", "k", "i", "a"},
Definition: "k",
}

// Encoded I: λs k i a. i
EI = Combinator{
Name: "C",
Arguments: []string{"s", "k", "i", "a"},
Definition: "i",
}

// Encoded Application: λm n s k i a. a m n
EA = Combinator{
Name: "D",
Arguments: []string{"m", "n", "s", "k", "i", "a"},
Definition: "amn",
}

// Universal Combinator U: Y (λu e. e S K I (λm n. u m (u n)))
U = Combinator{
Name: "U",
Arguments: []string{"e"},
Definition: "Y(S(K(S(S(S(SI(KS))(KK))(KI))))(S(KK)(S(S(KS)(S(K(S(KS)))(S(KK))))K)))e",
}

Universal = Basis{S, K, I, Y, ES, EK, EI, EA, U}
)

// BCKW (https://en.wikipedia.org/wiki/B,_C,_K,_W_system)
Expand Down Expand Up @@ -95,6 +145,9 @@ var (
Arguments: []string{"x"},
// Note the use of other combinators in the definition
// makes Iota "improper"
//
// i x = x S K
// i = S (S I (K S)) (K K)
Definition: "xSK",
},
}
Expand Down
40 changes: 40 additions & 0 deletions combinator_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -121,3 +121,43 @@ func TestFullyImproperCombinators(t *testing.T) {
})
}
}

func TestY(t *testing.T) {
// Use a small frame limit locally for this test to avoid stack overflow
oldMax := MaxFrames
MaxFrames = 100
defer func() { MaxFrames = oldMax }()

_, err := SKI.Transform(context.Background(), "Yf")
if err == nil {
t.Error("expected error")
}
if err.Error() != "loop detected" {
t.Errorf("expected error loop detected, got %s", err.Error())
}
}

func TestUniversal(t *testing.T) {
tests := []struct {
expr string
expected string
}{
{"ASKII", "S"},
{"BSKII", "K"},
{"CSKII", "I"},
}

basis := Universal

for _, tc := range tests {
t.Run(tc.expr, func(t *testing.T) {
actualResult, err := basis.Transform(context.Background(), tc.expr)
if err != nil {
t.Fatalf("Transform failed: %v", err)
}
if tc.expected != actualResult {
t.Errorf("transformed %s incorrectly, expected %s but got %s", tc.expr, tc.expected, actualResult)
}
})
}
}