Combinatory logic

Qwerp-Derp

09:00

Hello!

Zgarb

Hi

Are you checking the implementaton of L now?

Qwerp-Derp

09:28

Yeah

But I got (L (x L)) instead

  (Y (C (B S (C (B B I) I)) I) x)
= (C (B S (C (B B I) I)) I (Y (C (B S (C (B B I) I)) I)) x)
= (B S (C (B B I) I) I x (Y (C (B S (C (B B I) I)) I)))
= (S (C (B B I) I) (I x) (Y (C (B S (C (B B I) I)) I)))
= (S (C (B B I) I) x (Y (C (B S (C (B B I) I)) I)))
= (C (B B I) I (Y (C (B S (C (B B I) I)) I)) (x (Y (C (B S (C (B B I) I)) I))))
= (B B I (Y (C (B S (C (B B I) I)) I)) I (x (Y (C (B S (C (B B I) I)) I))))
= (B (I (Y (C (B S (C (B B I) I)) I))) I (x (Y (C (B S (C (B B I) I)) I))))
= (I (Y (C (B S (C (B B I) I)) I)) (I (x (Y (C (B S (C (B B I) I)) I)))))

@Zgarb?

Zgarb

Hmm.

Qwerp-Derp

I'm not sure if I borked something

Zgarb

  (C (B S (C (B B I) I)) I (Y (C (B S (C (B B I) I)) I)) x)
= (B S (C (B B I) I) (Y (C (B S (C (B B I) I)) I))) I x)

Second and third rows

No wait

= (B S (C (B B I) I) (Y (C (B S (C (B B I) I)) I)) I x)

There, had one closing paren too many.

You had (C (1) I (2) x), and did ((1) I x (2)), while the correct derivation is ((1) (2) I x)

@Qwerp-Derp BTW, how you could derive the implementation of L yourself is this. Take the property you want, say L x = L x x. Make a lambda term with an extra function argument that evaluates to the result: λf.λx.f x x. Apply fixpoint combinator: Y (λf.λx.f x x) is the function you're looking for (see why?). Then translate the lambda term to combinators using these rules.

Sherlock9

09:45

So exactly what is combinatory logic? What are we logically combining?

Zgarb

Combinatory logic

Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments. == Combinatory logic in mathematics == Combinatory logic was originally intended as a 'pre-logic' that would...

3

Sherlock9

Ah thanks

You may want to pin that or put in the chat description

Zgarb

room topic changed to Combinatory logic: S K I and other stuff. See Wiki article. (no tags)

room topic changed to Combinatory logic: S K I and other stuff. en.wikipedia.org/wiki/Combinatory_logic (no tags)

Qwerp-Derp

10:03

What

@Zgarb Whoa it's that easy?

Well now i have to learn lambda calculus

Zgarb

The hard part is coming up with a fixed-point combinator, which fortunately has been done for us. ;)

Qwerp-Derp

Ooh what about a challenge where you have to determine if the statement evaluates to an endpoint?

That could be a nice challenge

Qwerp-Derp

10:21

OK yeah cool it all works out

  (Y (C (B S (C (B B I) I)) I) x)
= (C (B S (C (B B I) I)) I (Y (C (B S (C (B B I) I)) I)) x)
= (B S (C (B B I) I) (I (Y (C (B S (C (B B I) I)) I))) x)
= (B S (C (B B I) I) (Y (C (B S (C (B B I) I)) I)) x)
= (S (Y (C (B S (C (B B I) I)) I)) (C (B B I) I) x)
= (Y (C (B S (C (B B I) I)) I) x (C (B B I) I x))
= (Y (C (B S (C (B B I) I)) I) x (B B I (I x)))
= (Y (C (B S (C (B B I) I)) I) x (B x I))
= (Y (C (B S (C (B B I) I)) I) x (I x))
= (Y (C (B S (C (B B I) I)) I) x x)

Cheers @Zgarb!

Zgarb

10:56

@Qwerp-Derp That's unfortunately undecidable. :P

Qwerp-Derp

Oh yeah the N thing right?

Zgarb

Yeah

Qwerp-Derp

But is completely impossible to determine if a statement is normal, even with normal programming languages and such?

Zgarb

Yes, because combinatory logic is Turing complete

Qwerp-Derp

Wouldn't it just boil down to if the statement was a subsection of a generated statement after going through the combinators and left-association?

Zgarb

11:02

You can have infinite derivations that never enter a loop.

Qwerp-Derp

@Zgarb ? Provide an example

(L x x) is generated from (L x), and you can check if L x is in L x x, which it is, and know that (L x) is not normal because it'll generate infinite copies of itself

The same goes for Y

Zgarb

Take a term T that satisfies T x = T (K x)

Then T x doesn't occur in the result

Qwerp-Derp

Oh

Zgarb

It's a simple example, but they can be arbitrarily complex.

Qwerp-Derp

13:21

Ooh, what about a challenge where you have to generate a new combinator?

Zgarb

Like what we did with L?

Qwerp-Derp

Yeah, but it's a code-golf thing

Or maybe a code-challenge

If an optimal solution is hard to achieve

How hard is it to achieve an optimal solution?

Zgarb

Optimal in terms of length? Possibly undecidable.

Qwerp-Derp

Yeah... is it undecidable? But the lambda thing...

Or is that not optimal?

Zgarb

It's not necessarily optimal.

Qwerp-Derp

13:25

So given something like (L x) -> (L x x), generate the optimal statement for L, while only using S and K (as well as parens).

That would be the challenge, but I need test cases.

And that's hard.

Zgarb

I don't think you can require optimality.

Qwerp-Derp

It would be a metagolf

And the task would be to generate as short a solution as possible, regardless of optimality.

I really want to top my "There can be only 1" metagolf... this might be the chance

Would that be a good challenge? I need testcases, though, and that's hard

Zgarb

It may be a bit obscure.

How about a golf: "translate a lambda term to a combinatorial term using these rules"

Qwerp-Derp

Hmmm... it might end up a flop like my other metagolf challenges.

Zgarb

Metagolfs are hard.

Qwerp-Derp

13:37

That's true

Can you give some testcases?

Zgarb

For the metagolf?

Qwerp-Derp

Yup

I think there are arbitrarily many already, I can just do "scramblers"

S a b c = S b c a for example

S a b c d = S b c d a

And so on and so forth

Zgarb

Okay: L x -> S (K x), L x -> x x, L x -> x L

The scramblers are good!

Qwerp-Derp

That would be pretty complex to do

So the statement on the other side of the = must only have:

- the name of the combinator itself

- lowercase "stand-ins"

- brackets

- S and K

I think we should change it so that it can take arbitrary numbers as input

So something like S 1 2 3... n -> S n 1 2 3...

Where n is a number as a stand-in

Zgarb

Maybe. Also, I'm not sure whether you should allow self-reference. The challenge is pretty complex as it is.

Qwerp-Derp

13:48

Oh yeah

Zgarb

So just L 1 2 3 4 -> 4 (1 3 1) 1 or so.

Qwerp-Derp

But your examples have self-reference

Zgarb

Yeah, but that was before I realized it. :P

Qwerp-Derp

But basic stuff like S and K are allowed in the other side right? It shouldn't be too complex...

Zgarb

I'm torn on that. Maybe you should try to write a reference solution without them, and see how complex it becomes.

Qwerp-Derp

13:59

Hmmm...

I think S and K should be all right, though - it shouldn't be too hard.

Zgarb

Probably not. But note that then you can construct a term with no normal form.

Qwerp-Derp

That's true.

Transcript for