#cs

I'd welcome advice on how to handle "free variables" when working out if a λ-term is legal using the "premise / conclusion" process

I'm not sure how to handle the type for the "free variable" y in this exercise

working out so far
https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-6.html

image attached to illustrate which variable

I should have ended up with the empty context justifies...

∅ ⊢ ....

#maths #cs

@jonmsterling

I think I've cracked it.

The type of

λxyz.(xz)(yz)

is

( A → (E → F)) → (C → E) → C → F

I was previously trying to infuse information about what gets applied to what in the final type and mistakenly doing stuff like (AB)

Now I realise the "dependency" info all goes into the "input" types as above.

#maths #cs

I've zoomed into what I think is the root of my misunderstanding.

Let's try to work out the type of this simplified example.

λxy.xy

Here's my thinking:

We're not given any types so we assign variables. Let's say x:A and y:B.

But since x is applied to y we can say more about the type of x. It must be an arrow type from B to an unknown C.

So the type of xy is C.

So the type of the full λ-term is

λxy.xy : (B →C)→ B → C

Is this correct?

1/2

#maths #cs

What's the type of the following term?

λxyz . (xz)(yz)

If we say

x: A
y: B
z: C

The type of the term is I think

A → B → C → (AC)(BC)

But something tells me this is not using the fact that B and A must be arrow types themselves.

#maths #cs

CS degrees now have one of the highest rates of unemployment.

https://www.newsweek.com/computer-science-popular-college-major-has-one-highest-unemployment-rates-2076514

#CS #economics #unemployment

If you want a nice and quick interactive (check you actually understand) tutorial on λ-calculus basics...

this is quite nice and can be done in about an hour, or less if you're quicker than I am

https://lambdaexplorer.com

#maths #cs

Is it not allowed to have self-referencing in types?

Eg unification arrives at

B == (A ->B)-> C

Where A B C are type variables.

I'm assuming this is not allowed and is one way to decide if a lambda-term is not simply typeable.

#maths #cs

λ-calculus beginner question

The textbook says

xx

can't be simply typed.

Reasoning is that the first x has an "arrow/function" type, eg A → B. That means the second x must have type A, which is contradicts A → B.

---

My question: Why can't both x have type A → A ? So the second x is A→A such that the type of xx is

λa. a→a

My brain tells me this works. Is it because this type is not a "simple" type?

#maths #cs

I frequently advocate that the undergrads and the fresh graduates of #EE and #CS, study the classics. I had often been tarred and feathered on various social media for that advocacy, by those very youngsters.

Their revulsion of the classics is abnormal, if not abhorrent. Many intellectual fields demand the practitioners to possess a modicum of historical background. Students of law are required to read some very ancient legal documents. Students of literature, linguistics, music, warfare, history, and loads of other fields habitually study the classics.

I am not saying that today's EE and CS novices should begin their study of some subject with a centuries-old tome inked with a quill on velum. I am simply suggesting that, after they had studied the textbook their professor prescribed, they should explore the classic texts and the seminal papers in that subject, so as to broaden their knowledge and perspective—especially if they intend to specialise in that subject in the future.

I do feel that I am fighting a losing battle, however. The young folk I have worked with in #IT over the past couple of decades do not even read textbooks any longer, not since they left the uni.

I've struggled for 2 days with this exercise

Find a λ-term M such that

Mxyz = xyzM (beta equivalence)

If anyone wants to comment / help please do so here or at stackexchange

https://cs.stackexchange.com/questions/173015/method-to-solve-to-mxyz-β-xyzm-λ-term-m

--

M := xyz feels like cheating and not aligned to the course content on the fixed point theorem and fixed point combinators

#maths #cs

Now this is an interesting challenge.

Solve for lambda expression M where the following beta=equivalence holds.

Mxyz = xyzM

The usual exercise is to have M = ..

---

I'm thinking I might play with

L := \ab. axyzb

so LM(id) = L(id)M

...

#maths #cs

How are concepts like 'reasoning' and 'inference' defined?

#Philosophy has definitions that go way back (e.g., in #epistemology and #PhilMind). Now #computerScience are realizing a need for definitions.

This #openAccess #CS review takes a crack at them: https://doi.org/10.48550/arXiv.2504.15909 (corrected URL)

#игры #CS Тарелочницы в КС! Геймеры, будьте бдительны! Играл сейчас с девочкой. А она оказалась внезапно с курской области, сидит в компьютерном клубе. Надо продлить, чтобы со мной сыграть еще одну катку. Но у неё денег нет. Сказал, что не дам. Обиделась. Я, говорит биснесвоман, веб студией заведую. Так просто получилось. А ты меня обижаешь сейчас.

Играет хуево, катку слила. Не советую.

Returning #Blind #CS #Student – Seeking Advice on LaTeX & #Accessible #Math Tools

Hi everyone! I’m a blind student returning to college to pursue a B.S. in Computer Science through Colorado Christian University Online. This is my third attempt at college due to chronic illness, but I’m excited to be back and determined to make it work.

I’m looking for advice on two fronts:

1. LaTeX on #Windows

I’ve recently started learning LaTeX and find it a more accessible way to write papers—especially when paired with Zotero for citations. My main machine is a Windows 11 Pro mini PC, and I also have a Raspberry Pi running Arch Linux ARM.

So far, I’ve tried:

Overleaf – nice interface, but the PDF viewer isn’t very screen reader-friendly and the editor has some issues too (JAWS/NVDA repeat lines).
VS Code with LaTeX Workshop – most accessible option I've tried
TeXnicCenter – only briefly.

Question: What LaTeX editors or workflows do you use on #Windows, and how accessible have you found them?

2. Relearning College-Level Math

I’ll be starting with calculus early next year. It’s been a long time since high school, and chronic illness has affected my memory and cognition. I used to use a Perkins Brailler for math, but arthritis/lupus (still being diagnosed) makes that painful now.

Question: Can anyone recommend accessible resources for relearning math—especially for someone doing everything online?

Any tips for doing math, science, or programming fully online as a blind student would be incredibly appreciated.

Thanks in advance! I’m happy to share what I learn along the way.

Feel free to boost or tag others who might have insights.

#BlindTech #Accessibility #LaTeX #STEM #DisabilityInSTEM #MathAccessibility #JAWS #NVDA ##ScreenReader Zotero #ChronicIllness #OnlineLearning @mastoblind @main

I've posted a longer version of this on stack exchange if anyone wants to help.

https://cs.stackexchange.com/questions/173005/should-i-be-able-to-find-a-beta-reduced-solution-to-m-lambda-zy-xmy

#cs #maths

anyone know of a blog/video/article I can read about solving this kind of thing

M = λxy. xMy

using the 'fixed point theorem' and the so-called "Y fixed-point combinator".

the textbook I'm following doesn't have a completed worked example

I think I get the theory but finding an expression for M seems undoable

#cs #maths

“Getting A Cease and Desist Letter From WaffleHouse” - This is a fun and interesting story of how a teenage #CS student hacked Waffle House’s website for what he thought was a good, disaster/weather cause (I agree) and got a cease-and-desist letter from the company’s legal department. The story has a happy, syrupy ending. #Weather #hacking #disasters

https://jack.bio/blog/wafflehouse

As an #EE, I learned cope with \(\infty\).
As a #CS, I learned to fear it.

Learning C about argv and argc and learning that #Linux is written in C and knowing that Linux is open source, can I look at the code written for the binaries (ls, mkdir, cd etc.)? #coding #programming #cs

Can I ask ...

To show two λ-terms are NOT β-convertible

All I need to do is show they reduce to different β-normal-forms ?

To me, that's intuitively correct, but the textbook doesn't explicitly say so.

--

example

(λx. xx)y → y y

(λxy. yx)xx → x x

so (λx. xx)y and (λxy. yx)xx are not β-convertible

#cs #maths