I don't want to ask if the attached derivation is correct - that's a boring request.
Is there an online tool I can use to check for me?
The few tools I have found don't do second-order λ2 terms.
I don't want to ask if the attached derivation is correct - that's a boring request.
Is there an online tool I can use to check for me?
The few tools I have found don't do second-order λ2 terms.
Advice welcome...
I just learned that in simply-typed λ-calculus, you can't type
λx . xx
but with λ2, you can, as follows
λx : (Πα : ∗. α →α) . x(σ →σ)(xσ)
---
I'm still trying to get my head around the fact that each x has different (type) arguments.
Feels like cheating. Feels like whatever is chosen for x at the λ, should be set in stone for the remainder of the scope of λ.
1/2
@enobacon
A very nice "engineer's demonstration" with no understanding of the underlying mathematics. (e.g. a catenary isn't a parabola). Brilliant stuff!
#FFS #maths #mathematics #cosh #exponential #FakeNews #light #caustic #engineering
I simply cannot believe that I've spotted an error in one of Grant's splendid maths videos.
Sadly, though, it's not a maths error, so who gives a monkey's.
#GrantSanderson #3Blue1Brown #maths #mathematics #English
Sanity check needed :
✢ If a term M is legal in λ2,
✢ And if a term N is also legal in the same context,
✢ Then MN is also legal, right?
---
This seems intuitively obvious but I can't actually find a definition / lemma in my textbook to confirm it.
The Subterm Lemma seems to be the opposite of what I'm seeking. It says that if MN is legal, then the sub terms M and N are legal too.
Science models of the world are useful, but we know they're wrong (they're only models)
New Books in Physics and Chemistry: Grace Lindsay, "Models of the Mind: How Physics, Engineering and Mathematics Have Shaped Our Understanding of the Brain" (Bloomsbury, 2021)
Episode webpage: https://newbooksnetwork.com
Media file: https://traffic.megaphone.fm/NBNK9061519438.mp3?updated=1742396295
"It is important to point out that the mathematical formulation of the physicist’s often crude experience leads in an uncanny number of cases to an amazingly accurate description of a large class of phenomena. This shows that the mathematical language has more to commend it than being the only language which we can speak; it shows that it is, in a very real sense, the correct language." – Eugene Wigner (1902-1995)
#quote #mathematics #math #maths
Very occasionally there's a comment that I really like in the other place. (This was on a pointless argument on whether "the average" always meant the mean).
my brain isn't working
did I get the type on the last line right?
---
if x was x:β then the type would be β→...
but here x is x:Πα:*.(α→α) and naively that means the type is Πα:*.(α→α) →...
I'm partly worried that α should be σ but then I remember that α is bound so irrelevant outside the scope of the Π
I'm begrudgingly impressed by overleaf - an online latex editor and previewer.
They managed to include useful latex packages, have good documentation and tutorials, have a UI that isn't too complicated and headache-inducing.
I still use offline lyx for my projects, but overleaf is good for generating small snippets of typeset maths.
Begrudging? Well, I wanted to create an online version of lyx (no latex code) but never managed to find time.
"My enthusiasm for mathematics was based principally perhaps on my horror of hypocrisy [...]. In my opinion, hypocrisy wasn’t possible in mathematics and, in my youthful simplicity, I thought the same went for all the sciences in which I had heard it said they were applied." – Stendhal (1783-1842)
#quote #mathematics #math #maths
Why am I asking?
previously I worked out the type of
λxyz. xz(yz)
as
(B → (A → C)) → (B → A) → B → C
where x:A, y:B, z:C
---
now I want to parameterise the types of x,y,z to make a λ2-term and it seems easier if I can do the funny types
λα,β,γ:*. λx:(β → (α→γ)) . λy:(β→α) . λz:β. xz(yz) : Παβγ:*.(β → (α→γ)) → (β→α) → β → γ
If I wasn't allowed to have non-trivial types for x, y, z then the "algebra" on the RHS would be really convoluted
---
2/2
Is it normal to do this kind of thing?
λα,β:* . x:α→β, y: α . xy : Πα,β:*. (α→β) →α →β
That is, to have non-trivial types for objects like x?
--
To make that clearer ...
So instead of just doing x:α, y:β we do things like x:α→β→β and y:β→α
---
1/2
Here's the question for July 9th from the AMS Daily Epsilon of Math Calendar
@DailyEpsilon
Thanks
---
I previously struggled to find a T such that
Πα:*.α : T
which appears to ask for a 'type of a type'
with some help, I used the formation rule to say T must be *
---
The reason I'm struggling a little with this kind of expression again is I have a more challenging (to me) exercise where I have to find an inhabitant for α and β given the context
α : ∗
β : ∗
x : α →Πα:*.α
f : (α →α) →α
looking at x is why I'm thinking " what is the type of Πα:*.α ?"
@DaniLaura
Looks like stuff I used to do on the BBC Micro.
#JustSaying #maths #art
Is this correct?
---
In the context β:*, the type of
Πγ:*.γ
is
β → β
---
"In mathematics it is new ways of looking at old things which seem to be the most prolific sources of far-reaching discoveries. A particular fact may have been known for centuries, and it may have been sterile or of only minor interest all that time, when suddenly some original mind glimpses it from a new angle and perceives the gateway to an empire." – Eric Temple Bell (1883-1960)
#quote #mathematics #math #maths