Lambda calculus done in Racket

[Lawrence Bottorff]

I found these blowing down the sidewalk today

; TRUE = λx.λy.x
(define mytrue
  (lambda (t) (lambda (f) t)))

and 

; FALSE = λx.λy.y
(define myfalse
  (lambda (t) (lambda (f) f)))

Two problems, I don't understand them and AFAICT, they don't work. I traced them back to this post on stackoverflow. Can anyone get me started here?

LB

[Ricardo Gabriel Herdt]

Hi,

The idea is that you can encode an expression

"if B then P else Q"

as a λ-term BPQ. So if B is true, you get P, otherwise Q.

For an overview of λ-calculus I suggest reading this:

https://ecee.colorado.edu/ecen5533/fall11/reading/lambda_types.pdf

The encoding of boolean expressions is described on (book) page 16.

Regards,

Ricardo

Am 17.02.2020 18:12 schrieb Lawrence Bottorff:
> I found these blowing down the sidewalk today
>
> ; TRUE = λx.λy.x
> (define mytrue
> (lambda (t) (lambda (f) t)))
>
> and
>
> ; FALSE = λx.λy.y
> (define myfalse
> (lambda (t) (lambda (f) f)))
>
> Two problems, I don't understand them and AFAICT, they don't work. I

> traced them back to this [1] post on stackoverflow. Can anyone get me
> started here?
>
> LB
>
> --
> You received this message because you are subscribed to the Google
> Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it,
> send an email to racket-users...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/CAFAhFSXjQq2WWei8zvVY38cQmPd9Yb9sd95zCsszWY_aO3xPkA%40mail.gmail.com
> [2].
>
>
> Links:
> ------
> [1]
> https://stackoverflow.com/questions/40288602/the-code-of-the-build-in-scheme-procedure-pair
> [2]
> https://groups.google.com/d/msgid/racket-users/CAFAhFSXjQq2WWei8zvVY38cQmPd9Yb9sd95zCsszWY_aO3xPkA%40mail.gmail.com?utm_medium=email&utm_source=footer

[George Neuner]

In addition to Ricardo's good answer:

The definition of TRUE above is one of the combinators of the S-K-I combinator calculus, which is a simple to understand subset of the untyped lambda calculus.  Programs in S-K-I are expressed as sequences of 3 simple combinators, and computation is done by repeated expansion, application and reduction until an irreducible form - the result - is reached.

https://en.wikipedia.org/wiki/SKI_combinator_calculus

George

[John Clements]

I’m sure many other people have something like this, but here’s “Lab 5” from my currently-running PL course:

https://www.brinckerhoff.org/clements/2202-csc430/Labs/lab5.html

It introduces church numeral encodings and also this kind of true-false encoding as small programming challenges in Racket. It assumes that you already know how to program in Racket. It doesn’t go deep.

John

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAFAhFSXjQq2WWei8zvVY38cQmPd9Yb9sd95zCsszWY_aO3xPkA%40mail.gmail.com.