Lambda Calculus via C# (8) Undecidability of Equivalence

[LINQ via C# series]

[Lambda Calculus via C# series]

All the previous parts demonstrated what lambda calculus can do – defining functions to model the computing, applying functions to execute the computing, implementing recursion, encoding data types and data structures, etc. Lambda calculus is a powerful tool, and it is Turing complete. This part discuss some interesting problem that cannot be done with lambda calculus – asserting whether 2 lambda expressions are equivalent.

Assuming f1 and f2 are 2 functions, they are equivalent if for ∀x, there is f1 x ≡ f2 x. For example, the following 2 functions can alpha-convert to each other:

f1 := λx.Add x 1
f2 := λy.Add y 1

Apparently they are equivalent. And they are both equivalent to:

f3 := λx.Add 1 x

because Add is commutative. Undecidability of equivalence means, in lambda calculus, there is no function can takes 2 lambda expressions as input, and returns True/False to indicate whether those 2 lambda expressions are equivalent or not. Alonzo Church has a proof using normal form. An intuitive proof can be done by viewing equivalence problem as another version of halting problem. Actually, Alonzo Church’s publish on equivalence is earlier (April 1936) than Alan Turing’s publish on halting problem (May 1936). To make it simple, this part discusses the undecidability of halting problem first, then discuss the undecidability of equivalence.

Halting problem

The halting problem is the problem of determining, when running an arbitrary program with an input, whether the program halts (finish running) or does not halt (run forever). For example:

No general algorithm can solve the halting problem for all possible program-input pairs. To prove this, first define a simple function Sequence.

Sequence := λa.λb.b

When applying Sequence, the reduction strategy matters. In normal order, both its first argument is never reduced. In this part, applicative order is always assumed - the same reduction strategy as C#. So Sequence can be viewed as - reduce (run) a then reduce (run) b sequentially, and return the reduction result of b. When applying Sequence with Ω and another lambda expression. It reduces forever in applicative order:

  Sequence Ω x
≡ Sequence (ω ω) x
≡ Sequence ((λx.x x) (λx.x x)) x
≡ Sequence ((λx.x x) (λx.x x)) x
≡ ...

Because Ω does not halt, Sequence Ω does not halt either. In C#:

public static partial class Functions<T1, T2>
{
    public static readonly Func<T1, Func<T2, T2>> 
        Sequence = value1 => value2 => value2;
}

Assume an IsHalting function exists, which takes 2 parameters f and x, and returns True/False if function f halts/does not halt with parameter x:

IsHalting := λf.λx.If (/* f halts with x */) (λx.True) (λx.False)

Then an IsNotHalting function can be defined to test whether function f does not halt with argument f (itself):

IsNotHalting := λf.If (IsHalting f f) (λx.Sequence Ω False) (λx.True)

When a certain function f does not halt with itself, by definition IsNotHalting f returns True:

  IsNotHalting f
≡ If (IsHalting f f) (λx.Sequence Ω False) (λx.True))
≡ If (False) (λx.Sequence Ω False) (λx.True))
≡ True

Remember the If function is lazy, here λx.Sequence Ω False is never reduced. When f halts with itself, the application reduces to Sequence Ω False:

  IsNotHalting f
≡ If (IsHalting f f) (λx.Sequence Ω False) (λx.True))
≡ If (True) (λx.Sequence Ω False) (λx.True))
≡ Sequence Ω False
≡ Sequence (ω ω) False
≡ Sequence ((λx.x x) (λx.x x)) False
≡ Sequence ((λx.x x) (λx.x x)) False
≡ ...

As fore mentioned, Sequence Ω does not halt. So in this case, IsNotHalting f never returns False.

In C# IsHalting and IsNotHalting functions can be represented as:

internal static class Halting<T, TResult>
{
    // IsHalting = f => x => True if f halts with x; otherwise, False
    internal static readonly Func<Func<T, TResult>, Func<T, Boolean>>
        IsHalting = f => x => throw new NotImplementedException();

    // IsNotHalting = f => If(IsHalting(f)(f))(_ => Sequence(Ω)(False))(_ => True)
    internal static readonly Func<SelfApplicableFunc<TResult>, Boolean>
        IsNotHalting = f =>
            If(Halting<SelfApplicableFunc<TResult>, TResult>.IsHalting(new Func<SelfApplicableFunc<TResult>, TResult>(f))(f))
                (_ => Functions<TResult, Boolean>.Sequence(OmegaCombinators<TResult>.Ω)(False))
                (_ => True);
}

Here since f can be applied with itself, it is represented with the SelfApplicableFunc<TResult> function type.

It is interesting when IsNotHalting is applied with argument IsNotHalting (itself). Assume IsNotHalting halts with IsNotHalting, in another word:

  IsHalting IsNotHalting IsNotHalting
≡ True

then there is:

  IsNotHalting IsNotHalting
≡ If (IsHalting IsNotHalting IsNotHalting) (λx.Sequence Ω False) (λx.True)
≡ If (True) (λx.Sequence Ω False) (λx.True)
≡ Sequence Ω False
≡ Sequence (ω ω) False
≡ Sequence ((λx.x x) (λx.x x)) False
≡ Sequence ((λx.x x) (λx.x x)) False
≡ ...

So IsNotHalting IsNotHalting is reduced to Sequence Ω False, and is then reduced forever, which means actually IsNotHalting does not halt with IsNotHalting.

On the other hand, Assume IsNotHalting does not halt with IsNotHalting, in another word:

  IsHalting IsNotHalting IsNotHalting
≡ False

then there is:

  IsNotHalting IsNotHalting
≡ If (IsHalting IsNotHalting IsNotHalting) (λx.Sequence Ω False) (λx.True)
≡ If (False) (λx.Sequence Ω False) (λx.True)
≡ True

So IsNotHalting IsNotHalting is reduced to True, which means IsNotHalting halts with IsNotHalting.

Therefore, if IsHalting exists, it leads to IsNotHalting with the following properties:

  • If IsNotHalting halts with IsNotHalting, then IsNotHalting does not halt with IsNotHalting
  • If IsNotHalting does not halt with IsNotHalting, then IsNotHalting halts with IsNotHalting.

This proves IsNotHalting and IsHalting cannot exist.

Equivalence problem

After understanding the halting problem, the equivalence problem becomes very easy to prove. Assume an AreEquivalent function exists:

AreEquivalent := λa.λb.If (/* a and b are equivalent */) (λx.True) (λx.False)

which takes 2 lambda expression as parameter, and returns True/False if they are/are not equivalent. Now define the following 2 functions:

GetTrue1 := λf.λx.λy.Sequence (f x) True
GetTrue2 := λf.λx.λy.True

Given arbitrary function f and its argument x:

  GetTrue1 f x
≡ λy.Sequence (f x) True

  GetTrue2 f x
≡ λy.True

For specified f and x:

  • if f halts with x, then, ∀y, (GetTrue1 f x y) and (GetTrue2 f x y) both always returns True. That is, partially applied functions GetTrue1 f x and GetTrue2 f x are equivalent.
  • if f does not halt with x, then, ∀y, (GetTrue1 f x y) never returns True, and (GetTrue2 f x y) always returns True. That is, partially applied functions (GetTrue1 f x) and (GetTrue2 f x) are not equivalent.

Now halting problem and equivalence problem are connected. IsHalting function can be directly defined by AreEquivalent function:

IsHalting := λf.λx.AreEquivalent (GetTrue1 f x) (GetTrue2 f x)

The partial application (GetTrue1 f x) and (GetTrue2 f x) can be substituted as:

IsHalting := λf.λx.AreEquivalent (λy.Sequence (f x) True) (λy.True)

In C#:

internal static class Equivalence<T, TResult>
{
    // IsEquivalent = f1 => f2 => True if f1 and f2 are equivalent; otherwise, False
    internal static readonly Func<Func<T, TResult>, Func<Func<T, TResult>, Boolean>>
        IsEquivalent = f1 => f2 => throw new NotImplementedException();

    // IsHalting = f => x => IsEquivalent(_ => Sequence(f(x))(True))(_ => True)
    internal static readonly Func<Func<T, TResult>, Func<T, Boolean>>
        IsHalting = f => x => Equivalence<T, Boolean>.IsEquivalent(_ => Functions<TResult, Boolean>.Sequence(f(x))(True))(_ => True);
}

If the above AreEquivalent function can be defined, then IsHalting can be defined. It is already approved that IsHalting cannot exist, so AreEquivalent cannot exist either. This demonstrates equivalence problem is just another version of halting problem. So, lambda expressions’ equivalence is undecidable. The undecidability is actually a very general topic in computability theory and mathematical logic. The undecidability of halting problem and lambda calculus’ undecidability of equivalence are examples of Rice's theorem, and also examples of Kurt Gödel's incompleteness theorems.

52 Comments

  • Thanks for informative post

  • فیلتر پرس :خرید و فروش دستگاه فیلترپرس ، پارچه فیلتر پرس ، صفحه فیلتر پرس ، قیمت و هزینه مناسب (مستقیم از تولید کننده)،بهترین قطعات با کیفیت و ارائه خدمات تضمین شده در زمینه لوازم جانبی و مواد و تجهیزات مصرفی دستگاه فیلتر پرس ، با فیلتر پرس صفا به آسودگی به تجارت خود بپردازید !

  • شرکت تهویه نوین ایرانیان با بهره گیری از کادری مجرب و حرفه ای، متشکل از مهندسین با تجربه و نیروهای متخصص بر آن است تا در مسیر تحقق مشتری مداری گامهایی مؤثرتر بردارد. در این راستا با ارائه محصولاتی با کیفیت، عملکردی مطلوب، هزینه ای بهینه و نیز خدمات پس از فروش، در پی جلب رضایت مشتریان گرامی است.

    https://tahvienovin.com

  • شرکت آمینا گروپ فروش شما را با کمک تبلیغات به بیش از 50درصد افزایش می دهد. ما با تبلیغات در سایت های پر بازدید و معتبر، بهینه سازی و طراحی سایت برای گوگل سبب افزایش برندینگ شما می شویم. خدمات ما شامل تبلیغات در فضای مجازی، تبلیغات در فضای شهری، سئو و بهینه سازی سایت، پشتیبانی و نگهداری و طراحی وب سایت می باشد.
    https://amina-group.com

  • This article is really fantastic and thanks for sharing the valuable post.

  • awesome post. I’m a normal visitor of your web site and appreciate you taking the time to maintain the nice site. I’ll be a frequent visitor for a long time.

  • awesome post. I’m a normal visitor of your web site and appreciate you taking the time to maintain the nice site. I’ll be a frequent visitor for a long time.

  • Great Article it its really informative and innovative keep us posted with new updates. its was really valuable. 

  • Thanks for writing such a good article, I stumbled onto your blog and read a few post. I like your style of writing...

  • Great Post !! Very interesting topic will bookmark your site to check if you write more about in the future.

  • Very interesting topic will bookmark your site to check if you Post more about in the future.

  • If you are looking to buy home appliances in installments, you can refer to our store site.

  • if you are looking for signal in digital currency you can check our site every day.

  • این دوربین مدار بسته از خانواده دوربین های مدار بسته بی سیم می باشد بیشتر خصوصیات آن با دوربین های بی سیم مشابه است و به دلیل ظاهر کوچک و زیبایی که دارد به آن دوربین مدار بسته Babycam می گویند. به این دوربین مدار بسته، عروسکی نیز گفته می شود.

  • Thank you very much, your article is very good and helpful. will come to your website again

  • Keep up the good writing.











  • Thanks for sharing this valuable article with us . I would like to share my site with you.

  • Thanks for sharing, this is a fantastic blog post. Thanks Again. Want more.

  • Your work is very good and I appreciate you and hopping for some more informative posts

  • Great article Lot’s of information to Read…Great Man Keep Posting and update to People..Thanks

  • Very helpful information. Thanks for sharing this with us.

  • Really nice style and perfectly written content material in this. Material on this page is very efficient I’ve ever had. We do not need anything else. Thank you so much for the information.

  • Thanks for sharing.I found a lot of interesting information here. A really good post, very thankful and hopeful that you will write many more

  • This post is really astounding one! I was delighted to read this, very much useful. Many thanks

  • This article is really fantastic and thanks for sharing the valuable post.

  • that is what i was looking for


  • https://ma-study.blogspot.com/

  • This particular papers fabulous, and My spouse and i enjoy each of the perform that you have placed into this. I’m sure that you will be making a really useful place. I has been additionally pleased. Good perform!

  • Pretty good post. I just stumbled upon your blog and wanted to say that I have really enjoyed reading your blog posts. Any way I'll be subscribing to your feed and I hope you post again soon. Big thanks for the useful info.

  • I got too much interesting stuff on your blog. I guess I am not the only one having all the enjoyment here! Keep up the good work.

  • Really impressed! Everything is very open and very clear clarification of issues. It contains truly facts. Your website is very valuable. Thanks for sharing.

  • Betting professionals who want to use Sports Toto are encouraged to have a regular game review process. If you learn to know how Toto works by referring to the reviews of good regulators, you will be able to get a good position on betting sports as a permanent player.

  • از پرطرفدار ترین قهوه ها، میتونیم به قهوه فرانسه اشاره کنیم. چون به روش فرانسوی دم میشه به آن قهوه فرانسه میکن. اصولا همیشه برای دم کردن یک فنجون قهوه، قهوه آسیاب و پودر شدرو داخل ظرف میریختن و مانند قهوه ترک بهش آب جوش اضافه میکردن و دم میکردن. کشور فرانسه برای اولین بار یک ابزار جدید برای دم کردن قهوه ساخت که فرنچ پرس نام گرفت. و روند دم آوری قهوه رو سریع و کوتاه کرد.

  • دوست داری ناخناتو زیبا کنی ولی بلد نیستی؟
    یا نمیدونی چه طرحو مدل یا رنگی مده؟؟؟؟
    فقط کافیه با ما همراه باشی با کلی آموزش زیبایی و مراقبت از ناخن....
    برای مشاهده و خرید انواع لاک ژل در رنگ بندی و مدل‌های مختلف کلیک کن

  • What an amazing post! Thank you so much.

  • برخی از بازی های  شرکت بلیزارد بصورت رایگان دردسترس گیمرها و کاربران نخواهد بود. و این کاربران برای استفاده از بازی  گیم تایم یا همان گیم کارت خریداری کنند. یکی از این بازی ها،‌ بازی محبوب و پرطرفدار ورلدآف وارکرافت است. به شارژ ماهیانه بازی وارکرافت در سرورهای بازی بلیزارد  گیم تایم می گویند ، که در فروشگاه جت گیم موجود می باشد.

    خرید گیم تایم 60 روزه ازفروشگاه جت گیم:

    در واقع گیم تایم 60 روزه نمونه ای جدید است از گیم تایم ها برای استفاده دربازی World of Warcraft  . که در ادامه بیشتر در مورد این محصول و نحوه استفاده از آن توضیح می دهیم .

    شما با خرید گیم تایم 60 روزه در مدت زمان آن گیم تایم ( 60 روز ) به امکاناتی در بازی World of Warcraft درسترسی پیدا خواهید کرد که این امکانات شامل موارد زیر میباشند :

    1 - اجازه لول آپ کردن تا لول 50 ( بدون گیم تایم فقط می توانید تا لول 20 بازی کنید )

    2 - اجازه  چت کردن با دیگران درون بازی ( بدون گیم تایم نمی توانید در بازی  چت کنید )

    3 - دسترسی به بازی World of Warcraft Classic

    در نتیجه برای بازی در World of Warcraft حتمآ به تهیه گیم تایم نیاز دارید.

    نکته 1 : گیم تایم یا همان زمان بازی ورد اف وارکرفت برای توانایی انلاین بازی کردن استفاده می شود و بدون گیم تایم امکان بازی کردن بازی محبوب ورد اف وارکرفت را نخواهید داشت.

    نکته 2 : درصورتی که گیم تایم نداشته باشید امکان بازی ورد اف وارکرفت کلاسیک را ندارید و شما میتوانید جهت خرید این محصول از وبسایت ما اقدام نمایید

  • Some Blizzard games will not be available to gamers and users for free. And these users to buy game time or the same game card. One of these games is محب the popular World of Warcraft game. The monthly charge of Warcraft game on Blizzard Game Time game servers, which is available in the Jet Game store.

    Buy 60-day game time from Jet Game store:

    In fact, 60-day game time is a new example of game time for use in World of Warcraft. In the following, we will explain more about this product and how to use it.

    By purchasing 60 days of game time during that game time (60 days), you will get access to features in World of Warcraft, which include the following:

    1 - Allow to roll up to level 50 (without game time you can only play up to level 20)

    2 - Allow to chat with others in the game (without game time you can not chat in the game)

    3 - Access to the game World of Warcraft Classic

    Therefore, to play in World of Warcraft, you definitely need to provide game time.

    Tip 1: Game Time or Word F Warcraft is used for the ability to play online, and without game time, you will not be able to play the popular Word F Warcraft game.

    Tip 2: If you do not have game time, you will not be able to play the classic Word of Warcraft, and you can purchase this product from our website, your Jet Game Store.

  • گیم تایم 60 روزه در حال حاضر تنها گیم تایمی است که از طرف کمپانی blizzard برای بازیکنان گیم ، ورد اف وارکرافت ارائه شده است. در گذشته گیم تایم هایی مانند 30 روزه و 180 روزه هم موجود بود اما به دلیل سیاست های جدید این کمپانی و خط مشی که در نظر گرفته است، تنها گیم تایمی که در حال حاضر امکان فراهم کردن آن برای گیمر های عزیز، گیم تایم 60 روزه می باشد. در ادامه توضیحات جالبی در مورد گیم تایم برای شما جمع آوری کرده ایم که خواندنشان خالی از لطف نیست.

    کاربرد گیم تایم دو ماهه

    در حال حاضر گیم تایم 2 ماهه در تمامی زمینه های world of warcraft کاربرد دارد. اما اگر می خواهید که یک سری تجربه های جذاب و جدید را تجربه کنید باید این گیم تایم را خریداری کنید. این تجربه ها عبارتند از:
    استفاده از اکسپنشن های جدید
    بازی در مپ های جدید
    لول آپ به سبک جدید
    تغییر در شکل بازی

  • The assignment submission period was over and I was nervous, 바카라사이트추천 and I am very happy to see your post just in time and it was a great help. Thank you ! Leave your blog address below. Please visit me anytime.

  • Of course, your article is good enough, Keonhacai but I thought it would be much better to see professional photos and videos together. There are articles and photos on these topics on my homepage, so please visit and share your opinions.

  • Your writing is perfect and complete. However, I think it will be more wonderful if your post includes additional topics that I am thinking of. I have a lot of posts on my site similar to your topic. Would you like to visit once?

  • I'm writing on this topic these days, , but I have stopped writing because there is no reference material. Then I accidentally found your article. I can refer to a variety of materials, so I think the work I was preparing will work! Thank you for your efforts.

  • Of course, your article is good enough, Keonhacai but I thought it would be much better to see professional photos and videos together. There are articles and photos on these topics on my homepage, so please visit and share your opinions.

  • بانک های خازنی در صنعت کاربرد زیادی دارد؛ زیرا بیشتر انرژی موجود در صنعت از نوع موتوری است که سبب ایجاد مسائلی چون افزایش جریان و افزایش مقطع کابل و سیم ها می شود؛ از این رو برای کاهش این مشکلات بهترین گزینه اضافه کردن تابلو بانک خازن به مدار است.

    تجهیزاتی چون موتورها، سیم پیچ ها و ترانس ها هم از توان راکتیو و هم قدرت اکتیو استفاده می کنند. این قطعات در مصرف کننده های مختلفی مثل پروژکتورها، آسانسورها، ترانس های لامپ و ... به کار می روند که باعث افزایش مصرف توان راکتیو می شوند. راه حل کاهش مصرف توان راکتیو و انرژی در این وسایل استفاده از خاز موازی در مدار است. همچنین خازن ها جريان پيش فاز عناصر القايي را خثی کرده و سبب کاهش جریان مصرفی و کاهش افت ولتاژ در سیم ها می شوند.

    بهبود ضریب توان یکی دیگر از دلایل استفاده از تابلوهای بانک خازنی در صنعت است. تابلوهای بانک خازنی به دلیل داشتن قابلیت تنظیم و ثابت نگه داشتن ولتاژ می توانند از آسیب و خسارت به دستگاه ها و تجهیزات صنعتی جلوگیری کنند.

  • ✅ Venusbet <a href="https://lcbsbonsai.org/">Giriş</a> bahis ve casino sitesi Avrupa ülkeleri, dünya geneli ve Türkiye pazarında oldukça fazla tercih edilmektedir ve kullanıcıların çoğu bu siteyi bahis yapmak için tercih eder.

  • ☑ Türkiye’de hizmet veren çeşitli yabancı ve yerli bahis siteleri vardır, BTK tarafından bu sitelerin giriş yolu kapansa da en hızlı şekilde yeniden güncel giriş adresini kullanıcılara sunar.Venus bet lisans sahibi olan çok güvenilir bir şirkettir ve size tüm imkânları sunarak giriş yapmanızı sağlar.

  • خرید بازی دراگون فلایت جت گیم  سری بازی ورلد آف وارکرافت یکی از قدیمی ترین گیم هایی است که هم از نظر محبوبیت و هم از نظر شکل بازی نزدیک به دو دهه است که با ارائه انواع بسته های الحاقی برای دوستداران این گیم سرپا است و به کار خود ادامه می دهد .
    ورلد آف وارکرافت توسط شرکت بلیزارد ارائه شده و بدلیل سبک بازی و گرافیک بالا در سرتاسر جهان طرفداران زیادی را به خود جذب کرده است.
    این بازی محبوب دارای انواع بسته های الحاقی میباشد که جدید ترین آن که به تازگی رونمائی شده و در حال حاضر صرفا امکان تهیه پیش فروش آن فراهم میباشد دراگون فلایت است
    این بازی که از نظر سبک بازی با سایر نسخه ها متفاوت بوده و جذابیت خاص خود را دارد که در ادامه به آن می پردازیم . همچنین برای تهیه نسخه های این گیم جذاب می توانید به سایت جت گیم مراجعه نمائید. در ادامه بیشتر در مورد بازی و سیستم مورد نیاز بازی می پردازیم
    تهیه از سایت جت گیم

  • When I read an article on this topic, casinosite the first thought was profound and difficult, and I wondered if others could understand.. My site has a discussion board for articles and photos similar to this topic. Could you please visit me when you have time to discuss this topic?

  • Piabet’e üye olduktan sonra sitenin çeşitli bölümlerine bahis oynayarak, yaptığınız seçimin ne kadar önemli olduğunu ölçebilirsiniz. Bu web sitesinde sıkıcı bir zaman geçirmeyeceğinize söz veriyoruz. Bilgisayarınıza veya mobil cihazınıza herhangi bir şey indirmeden web sitesinde oynayabilir ve bahis oynayabilirsiniz.
    https://piabetgiris1.com/

  • Bir bahis sitesinin güvenli olduğunun birçok göstergesinden biri, web sitesinin altında belirtilen resmi bir lisansın bulunmasıdır. İkinci teknik, web sitesinin komut dosyası olup olmadığını kontrol etmektir, çünkü komut dosyasıyla yazılmış web siteleri güvenilirlikten yoksundur ve genellikle insanlar tarafından kâr amacıyla oluşturulur.

  • Your writing is perfect and complete. slotsiteHowever, I think it will be more wonderful if your post includes additional topics that I am thinking of. I have a lot of posts on my site similar to your topic. Would you like to visit once?

  • The article in this site is excessively lengthy however its truly astonishing and Enlightening.

Add a Comment

As it will appear on the website

Not displayed

Your website