Combinatory Logic

Jobs
#1

Hi,

Would anyone be able to tutor me in Combinatory Logic? That is, using the functionally complete Agda code below:

K : A → B → A
K = λ a b → a

S : (A → B → C) → (A → B) → A → C
S = λ f g x → f x (g x)

I : A → A
I {A} = S K (K {B = A})

I would be willing to pay £10 per hour to anyone who can help at all.

Thanks,

Luke McCartney

1 Like
#9

If I were to start at ski (or encodings like church/ De Bruijn indexing )today, I think about repeated beta reduction in stlc and try to see how I can minimise the duplication of steps in the process , construct self reducer /self interpreter … so that I can keep it relatable to everyday algebraic manipulations. At the same time I d build in a language like nix [^1] / hvm [^2]
feel free to DM , if you need further help, set aside the 1/10/100 gbp /minimum wage debate for a moment
[^1]: I can let you access my nix code , for a start if you are in sr.ht.
[^2]: GitHub - HigherOrderCO/HVM: A massively parallel, optimal functional runtime in Rust
helpful talks-
https://gergo.erdi.hu/talks/2017-02-fomega-eval/FOmegaEval.pdf
videos -
discourse has a limit on number of links per post

2 Likes
#10

Ben Lyn’s Zurihac 2023 presentation features a small bootstrapped implementation based on a superset of those combinators:

As a first step you could reduce the set of combinators used down to just S and K, then go from there…

5 Likes
#11

I installed the Rust runtime but am not entirely sure how it relates.

An example I have, which may be useful is this. Given the ‘twice’ function:

tw : (A → A) → A → A
tw = λ f n → f (f n)

This can be reduced to S, K and I as follows:

λ f n → f (f n)
= λ f → λ n → f (f n)
= λ f → S (λ n → f) (λ n → f n)
= λ f → S (K f) f
= S (λ f → S (K f) (λ f → f)
= S (S (λ f → S) (λ f → (K f)) I
= S (S (K S) K) I

Not sure if this helps. But it (still) doesn’t make much sense to me.

#12

Okay, I’ve installed and got the Rust Runtime installed but I’m not sure how it’s relevant.

  • I’ll check out the helpful talks.
  • What would the Nix code help with?

Thanks,

Luke

#13

This is great. I’ll check it out.

Thanks,

Luke

#14

If you are only after s k i
you can watch

( sharing now) thanks to the url limit.
then you ll be curious about lambda calculus/ church rosser theorems/ fixed points , if you want to go anywhere with it and then end somewhere here (pfa- yup it builds, I ve written it).
I d still suggest , stick to the algebra you already know and systems you already know, relate that to lambda calculus, y-comb. , ski is just a case for that. Rest depends on your intention of learning .
Best

image
image1024×768 146 KB

2 Likes
#15

This is really useful, the cardboard SKI calculus in particular.

Have you got any more links that may be of used?

Thanks,

Luke

#16

You may be interested in Hindley and Selden’s “lambda calculus and combinators: an introduction”

http://pds14.egloos.com/pds/200901/16/93/Lambda-Calculus_and_Combinators.pdf

#17

That link is dead, can you host it on GDrive or something instead please?

#18

@lukemccartney the link works for me. I’ve uploaded a copy to my GDrive that should be world readable: Lambda-Calculus and Combinators — J. ROGER HINDLEY & JONATHAN P. SELDIN.pdf - Google Drive

1 Like
#19

That’s great. Thanks so much!

#20

I gave this presentation about combinatory logic, hope you find it helpful: SKI School: The Combinator Calculus Demystified.

1 Like
#21

This will also be useful, thanks!

#22

Maybe chapter four of my monograph Haskell for mathematicians is useful to you (it is literate Haskell with only base as dependency so you can start playing around instantly), although as an Agda user you may already be beyond that. There are of course far more comprehensive texts about logic, some of which linked to by others above. I’m happy to have an occasional conversation about logic, even without fee. I am inclined towards the constructive aspect of logic.

BTW what significance does it have that S and K are are the lambda terms for return and ap of the reader monad?

1 Like
#23

Hi,

I’m not sure I understand your question:

K : A → B → A
K = λ a b → a

S : (A → B → C) → (A → B) → A → C
S = λ f g x → f x (g x)

Are functionally complete, that is, they together can create any function.

What is the reader monad? And what do you mean by return and ap?

#24

The reader monad is a structure on the family of types of the form R x = r → x for some arbitrary but fixed type r. One part of the monad structure is a family of functions x → R x for any type x. In Haskell it is denoted by the polymorphic function return. It so happens for the reader monad that this family of functions is implemented by the same lambda term as K. (Where A = x and B = r). Further any monad has an operation called ap in Haskell that has the type R (b → c) → R b → R c which for the reader monad happens to be implemented by the lambda term S. This may be just a coincidence. I do not know whether there is a deeper connection between S and K be functionally complete and monad structure.
Monads are interesting for the logician because they describe the free algebras for some algebraic theory.

#25

I do not know whether there is a deeper connection between S and K being functionally complete and monadic structure.

If by “functionally complete”, you mean Turing-complete then yes - the Applicative instance for the partially-applied function type (->) r :

instance Applicative ((->) r) where
    pure  = \ a b -> a
    (<*>) = \ f g x -> f x (g x)

…is Turing-complete (I think Ben Lynn also makes some comments about the Applicative-S-K connection in his presentation at Zurihac 2023). Therefore all computable functions can be defined (albeit very verbosely!) using pure and (<*>) for the Applicative reader type Reader r a = (->) r a .

Getting back on-topic - while Raymond Smullyan’s book To Mock a Mockingbird (1985), as mentioned earlier:

https://discourse.haskell.org/t/combinatory-logic/8380/14

…goes well beyond the S and K combinators, its memorable presentation of combinatory logic makes it a worthy addition to the collection of “offline” resources.

1 Like
#26

Hey,

Thanks for the literature, I’ll DM you about arranging a talk about logic!

Luke

#27

Does anyone know a website or service where two people can explore Haskell programs together? There is Chris Done’s tryhaskell but it would be good when two clients see exactly the same. It would not be so much of a disadvantage not to have access to many libraries except base.