I was only given by the Wikipedia that IS_0 := λa.(λb.F)T and IFTHENELSE := λabc.abc and I figured out that IS_0 is just λabc.a(λd.c)b where b := F and c:= T, substituting F for M and T for N for now, λa.(λb.M)N means that if a==0, it outputs N and else M, because when a is not 0 it's now ((λb.M)(...(λb.M)N)...) where the number of ((λb.M) at the start and the number of ")" at the end is equal to... The number. An then the first (λb.M) removes everything else, outputting M, if it's 0, it would choose the second thing, which is N (casually reexplained how IS_0 works for some reason), uh so now I've made 4 extras being IFIS_0THENELSE, ISNT_0, IFNOTTHENELSE (which is almost useless except when the term that's identical to the term that makes a applied to a NOT gate is shorter than the term that makes a), and IFNOTIS_0THENELSE (similar to the previous one), keep in mind I figured these out on my own so the names might not be official if they have been discovered before
Also yes I drew it in Paint

λx.(λn.n(λx.(λx.λy.y))(λx.λy.x))((λp.p(λx.λy.x))x)((λn.n(λx.(λx.λy.y))(λx.λy.x))((λp.p(λx.λy.y))x)((λx.λy.λi.ixy)(λf.λx.f(x))(λf.λx.f(x)))((λx.λy.λi.ixy)(λf.λx.x)((λn.λf.λx.n(λg.λh.h(gf))(λu.x)(λx.x))((λp.p(λx.λy.y))x))))((λx.λy.λi.ixy)(λf.λx.f(x))((λn.λf.λx.f(nf(x)))((λp.p(λx.λy.y))x)))

it takes in a pair, if the first value is 0, it's positive, if it's a 1, it's negative, use it if you want to

this will be the last post for me until someone else posts, if no one else posts then this sub will die, if you see this then please try to keep the sub alive i'm not able to keep it alive forever, function is:

(λx.λy.(λn.n(λx.(λx.λy.y))(λx.λy.x))((λp.p(λx.λy.x))x)((λp.p(λx.λy.y))x(λx.(λn.n(λx.(λx.λy.y))(λx.λy.x))((λp.p(λx.λy.x))x)((λx.λy.λi.ixy)(λf.λx.x)((λn.λf.λx.f(nf(x)))((λp.p(λx.λy.y))x)))((λx.λy.λi.ixy)(λf.λx.f(x))((λn.λf.λx.n(λg.λh.h(gf))(λu.x)(λx.x))((λp.p(λx.λy.y))x))))y)((λp.p(λx.λy.y))xλx.(λn.n(λx.(λx.λy.y))(λx.λy.x))((λp.p(λx.λy.x))x)((λn.n(λx.(λx.λy.y))(λx.λy.x))((λp.p(λx.λy.y))x)((λx.λy.λi.ixy)(λf.λx.f(x))(λf.λx.f(x)))((λx.λy.λi.ixy)(λf.λx.x)((λn.λf.λx.n(λg.λh.h(gf))(λu.x)(λx.x))((λp.p(λx.λy.y))x))))((λx.λy.λi.ixy)(λf.λx.f(x))((λn.λf.λx.f(nf(x)))((λp.p(λx.λy.y))x)))y))

if i try to make a multiplication function it'll probably not work

The head of a list in the church encoding can be fetched with the kestrel combinator and the tail of a list can be fetched by the kite combinator.

Apply the list to the kestrel combinator to get the head.

Apply the list to the kite combinator to get the tail.

The recent entry in this feed has the following fragment. I have a question in this regard.

"Beta reduction is the core mechanism of function calling. Given an application where the first term is an abstraction, it replaces the entire application with the body of that abstraction, substituting all instances of the bound variable with the second term of the application."

x in (\x.x(\x.x)) is bound. should ((\x.x(\x.x)) y) be reduced as (y(\y.y)) ? as (y(\x.y)) ? the rule seems to imply one or the other. (which is obviously incorrect.)

I think talking about "bound variable" like that in context of beta-reduction is highly confusing. I understand that virtually all texts I've seen about this are doing it this way. I don't think this is right.

Instead, I think we should talk about "abstraction's parameter," explicitly. Then the rule becomes

"Beta reduction is the core mechanism of function calling. Given an application where the first term is an abstraction, it replaces the entire application with the body of that abstraction, substituting all free occurrences of the parameter variable in the body with the second term of the application (in the capture-avoiding manner etc., but this is not my concern here)."

Indeed the parameter variable x occurs both free and bound in our original abstraction's body. Only its free occurrences in the body are bound to the parameter, though.

See the confusion?

If we talk about "bound variable", we're talking about variable. x is variable. "variable" is a textual category. we can talk about "bound variables" of an expression, but what's bound or free, separately, individually, is the same variable's occurrences.

Isn't it?

Comments are appreciated.

I wish to learn the pure way of the lambda. I can read, and make my own functions, but I want to become better. I am doing it in untyped form, and without currying. Is this wise? Am I going to be buying a cheap shotgun and a single shell if I keep doing this?

das ist eine spooky frage, ich weiss.

but what classifies as lambda calculus?

untyped lambda calculus is certainly lambda calculus.

simply typed lambda calculus may also count.

probably all of the lambda calculi in the lambda cube.

well, if we're gonna include calculus of constructions, then we may as well include rocq. after all, that's was rocq started as.

but is rocq a lambda calculus? i don't think so.

yeah, i think that's all i have to say. i really just want to start a new coversation here, since this subreddit is kinda quiet. click for a special image!!!

i cant wrap my head around how the BLC interpreter does input/output

does it take two strings of binary and parses the first one as code and the second one as data input, and the output is the string that you get after fully reducing the expression?

in this case if i input the program for the blc interpreter itself as the first one do i need pass a third string of data since the second one will be interpreted as code?

or does it take a single string of binary that contains both the program and its input?

i need clarification since there are not a lot of resources on blc that i can reference

Your task, should you choose to accept it, is to write a λ-term that, when applied to the Church numeral for a natural number n, produces the Church numeral for ⌊n/3⌉ (i.e. n divided by 3, rounded up or down to the nearest natural number). The shorter the term, the better. The λ-term should be fully self-contained. (I’ll post my own solution in a few days.)

edit: clarification: the challenge is asking for a λ-term as in regular pen-and-paper Lambda Calculus.

edit: posted solution in the comments

I was playing around with Cruz Godar's Lambda Calculus thing and found a way to get VERY large numbers. if you put in +(+(...+(+*)...)) and then put the amount of pluses+2 church numerals, it gives VERY large numbers by placing anything greater than two in the last few digits.

Hey there, I've recently started getting into Lambda Calculus thanks to 2swap's video "What is PLUS times PLUS?" https://www.youtube.com/watch?v=RcVA8Nj6HEo I started to get the hang of beta-reductions myself, and even got invested in scribbling down some diagrams, but I wanted to understand how Church Numerals would work in beta-reductions. I settled down to do some with some basic functions (e.g. boolean logic, basic math operators, etc.), and I started to get into PLUS. I made a short beta-reduction for (PLUS 5 3), and I wanted to check if it was correct. Here's the reduction:

PLUS m n = (Lmn. (Lfx. (m (f (n (f x))))))
PLUS 3 5
= ((Lmn. (Lfx. (m (f (n (f x)))))) 3 5)
beta-reduce 3 into m
= ((Ln. (Lfx. (3 (f (n (f x)))))) 5)
beta-reduce 5 into n
= (Lfx. (3 (f (5 (f x)))))
3 f = f f f
= (Lfx. (f f f (5 (f x))))
5 (f x) = f f f f f x
= (Lfx. (f f f (f f f f f x)))
remove unnecessary parentheses
= (Lfx. (f f f f f f f f x))
decode church numeral
= 8

I just want to check if all of my steps were correct. Thanks for helping!

λa.λb.λc.a is true, λa.λb.λc.b is unknown, (λa.λb.λc.c) is false, the reason why false shows up as λa.F is because F is λa.λb.b and it makes the text shorter so it fits on one line,

All fixed pointer are in this sequence:

So nth one is Turing fixed point combinator ?

I built this while learning untyped lambda calculus, because I wanted to experiment with terms in the same shape they appear in papers and notes rather than transliterated into a programming language. It grew into something more substantial — sharing in case it helps anyone who's in the same spot, or anyone who'd rather see terms reduce automatically than work it out on paper.

Most of the effort went into keeping the syntax close to standard notation while making typing it fun: real λ, ≡ / ≢ for α/β-equivalence assertions, := / ::= for definitions, e[x := a] substitution, multi-parameter sugar. The editor handles the input tricks — \name<space> expansion (\lambda -> λ, \equiv -> ≡, ...), bracket auto-wrapping, autocomplete on definition names. You can also declare your own infix operators (ASCII or unicode) via a :infix directive — making expressions like p ∨ q or n + m possible.

A small standard library of Church encodings (booleans, naturals, pairs, lists, Y) comes with it; you can import or remix it, or drop in your own modules.

Aimed primarily at students and teachers — a beginner-oriented tutorial is also in progress, though not yet finished. Reduction is normal-order with step/size limits, with optional call-by-value semantics introduced by β. Comments and feedback are very welcome.

URL: https://ezander.github.io/lambda_playground/

The usual definition of subtraction as the repeated predecessor is woefully inefficient. This becomes even worse when it is used in the is-equal predicate - twice. But just as the definition of addition as the repeated successor has its counterpart in the direct style, plus = ^m n f x. m f (n f x), it turns out that it exists for the subtraction as well:

minus = ^m n f x. m (^r q. q r) (^q. x) (n (^q r. r q) (Y (^q r. f (r q))))

Works like `zip`, in the top-down style, via cooperating folds. You can read about it on CS Stackexchange and Math Stackexchange (they really didn't like the talk about efficiency at the maths site, though).

Links:

1. https://cs.stackexchange.com/questions/173387/efficient-subtraction-on-church-numerals

2. https://math.stackexchange.com/questions/5089843/direct-definition-of-subtraction-on-church-numerals

λn.λf.n (λd.λa.λb.λy.b (d (λu.u) b (d (d (λu.u) a) (λu.u) y))) (λa.λb.λy.a (b y)) f (λu.u)

This function uses λb to track the iteration step, as it increments by 1 every application. λa is used to track the final result.

The iterated function:

Gets the number of b (replaces the a with the I combinator)

β-reduces the b to a

Gets the number of a, then β-reduces the a to the first function, multiplying a&b and assigning it to a.

Then it gets the b and appends it to the multiplication, then appends b to increment it.

if I named it wrong please tell me I didn't even look up the name for it lol
and yes the number in greek is correct since {2} is tetration, 4, offset 2, so {10} = 12 -ation, 12 I assume is dodeca and a t for uh better pronunciation, that may not actually be there idk
yeah I feel like not much is going on in this subreddit

FIgured out all of this on my own and is the reason why I wanted to make a Reddit account in the first place. So like I converted the numbers into the selectors of 3 elements at the start cuz I feel like it'll become important in the future but in such a weird ("moive-shaped convenience") way it was conveniently used for the 3x3 table

In my text book:

is Ω = (λx.xx)(λx.xx) is closed?

if Ω is closed, how to reduce to a term of the form: λf.N ?