Basic Mathematics - 2021-08-29

user21820

09:12

@F.Zer It doesn't really matter, because if you paste here it gets truncated anyway past the first few lines. If you really want to separate it, just use pastebin and post a link here.

@Node.JS I am in agreement with points (2) and (3) of the answer posted at that thread. Also, you need to learn very basic FOL first, including what precisely variables and quantifiers mean, before you even attempt to express statements about more complicated things like context-free grammars. If you learn basic FOL properly, you will never again need to ask others how to express something, regardless of which area of mathematics it is in. But if you do not, you will always be unsure how to.

Prithu biswas

10:35

Given a∈ℕ
	Given b∈ℕ
		Given c∈ℕ
			If a+c<b+c
				a<b ∨ b<a ∨ a=b
				If a=b
					a+c<a+c
					¬(a+c<a+c)
					⊥
					a<b
				If a<b ∨ b<a
					If a<b
						a<b
					If b<a
						b+c<a+c
						a+c<b+c
						a+c<a+c
						¬(a+c<a+c)
						⊥
						a<b
					a<b
				a<b
			a+c<b+c ⇒ a<b
		∀z(a+z<b+z ⇒ a<b)
	∀y∀z(a+z<y+z ⇒ a<y)
∀x∀y∀z(x+z<y+z ⇒ x<y)

@user21820 Is this proof correct?

user21820

12:18

@Prithubiswas That's right! Note that for convenience you can shorten multiple nested ∀-subcontexts, such as "Given a,b,c∈ℕ:" for your case.

Also note that it will be very convenient later to have non-strict inequality lemmas like ∀a,b,c∈ℕ ( a ≤ b ⇒ a+c ≤ b+c ) and ∀a,b,c∈ℕ ( a < b ≤ c ⇒ a < c ) and ∀a,b,c∈ℕ ( a ≤ b < c ⇒ a < c ) and ∀a,b,c∈ℕ ( a ≤ b ≤ c ⇒ a ≤ c ), where "x ≤ y" is short for "x < y ∨ x = y". You don't have to show me your proofs as I'm sure they're all straightforward for you. These lemmas make it very easy to prove statements like the one you want:

Given a,b,c∈ℕ:
  If a+c < b+c:
    a < b ∨ b ≤ a.
    If a < b:
      a < b.
    If b ≤ a:
      b+c ≤ a+c < b+c.
      b+c < b+c.
      ⊥.
      a < b.
    a < b.

Additionally, note that there are benefits to proving lemmas in the larger ℝ, because it supports subtraction, so from a+c < b+c you can immediately get a = a+0 = a+(c+(−c)) = (a+c)+(−c) < (b+c)+(−c) = b+(c+(−c)) = b+0 = b. @F.Zer: Can you please post your complete list of the axiomatizations of ℤ,ℚ,ℝ, so that Prithu can refer to them instead of my scattered chat messages? =)

Naturally, not all facts about a smaller structure can be proven by proving it in a larger structure.

For example, (PA−1) is outright false if you change "ℕ" to "ℚ". For another example, (PA1) happens to be true if you change "ℕ" to "ℚ", but even if you prove ∀k∈ℚ ∃m∈ℚ ( k = m·2 ∨ k = m·2+1 ) it is such a trivial result that you cannot easily go back to (PA1).

F. Zer

12:35

@user21820 Of course ! Let me clean my list of axiomatisations a bit, and I will post them. First, I will post Q10 lemma as I have it nearly ready to paste.

3 white edges from a vertex ⇒ black triangle.
  ∀ a,x,y,z ∈ V ( ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ a ≠ x ∧ a ≠ y ∧ a ≠ z ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ⇒ c(x,y) ∧ c(y,z) ∧ c(z,x) )
    ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) )
    ∀x,y,z∈V ( ¬c(x,y) ∧ ¬c(y,z) ⇒ c(z,x) )
    Given a,x,y,z ∈ V:
      ¬c(y,a) ∧ ¬c(y,x)
      c(y,x)
      ¬c(z,a) ∧ ¬c(a,x)
      c(z,x)
      ¬c(y,a) ∧ ¬c(a,z)
      c(y,z)
      c(x,y) ∧ c(y,z) ∧ c(z,x)
    ∀ a,x,y,z ∈ V ( ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ a ≠ x ∧ a ≠ y ∧ a ≠ z ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ⇒ c(x,y) ∧ c(y,z) ∧ c(z,x) )

user21820

@Prithubiswas: For your interest, F.Zer picked white+black while you picked red+green. =)

F. Zer

@user21820 Is my proof of the lemma closer to what you'd expect ?

user21820

@F.Zer Ehh you missed the "If ..." lol.

F. Zer

@user21820 Ouch.

3 white edges from a vertex ⇒ black triangle.
  ∀ a,x,y,z ∈ V ( ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ a ≠ x ∧ a ≠ y ∧ a ≠ z ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ⇒ c(x,y) ∧ c(y,z) ∧ c(z,x) )
    ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) )
    ∀x,y,z∈V ( ¬c(x,y) ∧ ¬c(y,z) ⇒ c(z,x) )
    Given a,x,y,z ∈ V:
      If ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ a ≠ x ∧ a ≠ y ∧ a ≠ z ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z:
        ¬c(y,a) ∧ ¬c(y,x)
        c(y,x)
        ¬c(z,a) ∧ ¬c(a,x)
        c(z,x)
        ¬c(y,a) ∧ ¬c(a,z)
        c(y,z)
        c(x,y) ∧ c(y,z) ∧ c(z,x)

user21820

And of course, for a complete proof at that level (intended for those exercises) you would have to included a proof of your "∀x,y,z∈V ( ¬c(x,y) ∧ ¬c(y,z) ⇒ c(z,x) )". I'm not asking you do to it, since clearly you can.

F. Zer

12:44

@user21820 Good. I have only included "∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ) " as a lemma. Is that sufficient ?

user21820

Isn't that a condition?

F. Zer

@user21820 This is a standalone lemma.

@user21820 I am not doing it inside the main proof.

I mean, I can't prove "c(x,y) ∧ c(y,z) ∧ c(z,x)" without it.

Sorry, I have to rush out of my house. I will post my list of axiomatisations, when I come back. See you !

user21820

Err...

Jul 13 at 13:44, by user21820

(Q9) ∀x,y,z∈G ( x*(y*z) = (x*y)*z ) ∧ ∀x,y∈G ( x*i(x) = y*i(y) ) ∧ ∀x∈G ( x*(x*i(x)) = x ) ⇒ ∀x,y∈G ( (i(y)*y)*x = x ), where (infix) * : G^2→G and i : G→G.
(Q10) ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ) ⇒ ∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x ) ∨ ∃v,w,x,y,z∈V ∀t∈V ( t = v ∨ t = w ∨ t = x ∨ t = y ∨ t = z ), where c : V^2→Bool.

It's right there as the second condition.

F. Zer

@user21820 Of course. Perhaps, I am not explaining this issue in a correct way. Will try again when I come back.

user21820

Ah I know what you're thinking. Of course I'm assuming you're doing that lemma under those conditions. Why wouldn't you?

F. Zer

12:48

@user21820 That's right !

@user21820 No, I am not doing that lemma under those conditions. That's why I added it.

user21820

No wonder, sorry my eyes skipped your "standalone lemma", because I didn't think it should be outside.

F. Zer

Good.

See you later !

user21820

See you!

Prithu biswas

@user21820 To be honest , I never knew that you can use "tab" and "space" to travel between contexts.

user21820

=O Then how did you indent without using tab and space?

Prithu biswas

12:57

@user21820 In all my past proofs , I did it manually.

user21820

Ahh good that you found out before starting on longer proofs!

@F.Zer: By the way, it's mechanical to translate the elegant proof and its key lemma into pure FOL as you did, but it doesn't yield the shortest proof! We can cut some bits that aren't actually needed. For example, we can actually delete "a ≠ x ∧ a ≠ y ∧ a ≠ z" from the conditions of that lemma since you never used them. You also didn't use "x ≠ y ∧ x ≠ z ∧ y ≠ z", but you should keep them there and change the conclusion of your lemma to "⊥", which is only possible under conditions∧¬conclusion!

@Prithubiswas: So, the idea behind programming-friendly editors is that you can tab/space to indent and then the editor helps you keep the same indent on subsequent lines.

This is because indentation is a fundamental feature of good programming languages.

It's a pity programming came too late to change the way mathematics proofs are written and the attitude towards more formal proofs.

Prithu biswas

Given a∈ℕ
	Given b∈ℕ
		If a<b
			a+1<b ∨ b<a+1 ∨ a+1=b
			If a+1<b
				a+1<b ∨ a+1=b
			If b<a+1 ∨ a+1=b
				If b<a+1
					Let c∈ℕ such that a+c=b
					a+c<a+1
					c<1 [Lemma]
					c=0 ∨ c=1 ∨ 1<c
					If c=0
						c=0
					If c=1 ∨ 1>c
						If c=1
							1<1
							⊥
							c=0
						If 1<c
							c<1
							1<1
							⊥
							c=0
						c=0
					c=0
					a+c=b
					a+0=b
					a=b
					a<b
					a<a
					⊥
					a+1<b ∨ a+1=b
				If a+1=b
					a+1<b ∨ a+1=b
				a+1<b ∨ a+1=b
			a+1<b ∨ a+1=b
		a<b ⇒ a+1<b ∨ a+1=b

@user21820 Is this correct?

Avra

Hello all,

Sorry if this sounds bizarre. "We wish to implement a dictionary by using direct addressing on a huge array. At the start, the array entries may contain garbage, and initializing the entire array is impractical because of its size. Describe a scheme for implementing a direct address dictionary on a huge array. Each stored object should use O(1) space; the operations SEARCH, INSERT, and DELETE should take O(1) time each; and the initialization of the data structure should take O(1) time. (Hint: Use an additional stack, whose size is the number of keys actually stored in the dicti…

Problem: can you please help explaining the wording of the question in your own words? No solution is needed!

user21820

@Prithubiswas: I'll answer Avra's question first because it takes less time to answer. =)

Prithu biswas

@user21820 Sure.

Avra

13:07

Thanks

user21820

@Avra The question is slightly wrong because it must also state the assumption that each object can be encoded using O(1) words. It is also vague, and I'm not sure if it's because it expects you to figure out what you can do... Anyway here is a precise solvable version:

Avra

@user21820. Thank you very much. If you can just say in English what the question is all about, that would be enough please.

user21820

You have an array of cells A[1..M] where M is extremely large, where each cell can store 1 word. You want to implement a map data structure that supports init : Void→Void and search : Nat→Object and insert : Nat×Object→Void and delete : Nat→Void each taking O(1) time. It must guarantee that after you call init(), it behaves as if it has an internal function F that is initially empty and is modified as follows:

(1) Each search(k) does not change F and returns F(k) if k∈Dom(f) and returns null otherwise.

(2) Each insert(k,x) changes F to ( Dom(F)⋃{k} i ↦ i = k ? x : F(i) ) and returns null (nothing).

(3) Each delete(k) changes F to ( Dom(F)∖{k} i ↦ F(i) ) and returns null.

Dom(F) denotes the domain of F.

It must also guarantee that there is some fixed constant c > 0 such that you can perform at least c·M operations before it starts failing to satisfy the guarantees.

This last guarantee is what "each stored object should use O(1) space" can be interpreted to mean. There is no way to "just say what the question is about", because it is vague whether deliberately or not. So I'm giving you a specific precise version that can be solved.

(By initially empty function I mean the function with empty domain.)

A could initially be in a complete mess; you cannot assume anything about the initial state of its cells. Obviously, you cannot initialize all of them during init() either because that would not take O(1) time.

To make clear why the problem is not trivial, consider that if you perform init() then insert(k,x) then search(m) for some arbitrary k,m, the search should return null iff k ≠ m because you haven't inserted anything other than x at 'index' k. But how can you tell when x must be stored somewhere in the big mess? So you must clearly have some checking mechanism as per the given hint. I figured it out just now so it is solvable. =)

@Prithubiswas Yes it's correct! Good job you proved a key theorem of PA−.

I presume you are working on the PA− exercises now?

Avra

13:36

@user21820. Thank you very much for your time.

user21820

@Avra You're welcome!

Avra

@user21820. Do you know what "garbage" here means in the question please?

user21820

@Prithubiswas: I found @F.Zer's proof of that same lemma here. You might want to try figuring out why your proof is quite a bit longer than that. =)

@Avra "garbage" means "trash" or "rubbish" and I explained it here.

Avra

@user21820. Usually, the stack once created, it would have constant size even though it's very large. The dictionary on the other hand has also fixed size. Both practically are initiallized to Nil in Java and other programming languages

This seems a theoretical question not practical

user21820

@Avra That's false. A stack cannot take constant size.

Avra

13:44

But since the dictionary takes constant size, should not the stack in the question please have constant size though as you said it can take any size?

user21820

@Avra It's practical in some applications where you cannot guarantee the initial state and don't want to have a long initialization. I don't think you really know how compilers and programming languages work, which is why you think it's not practical.

@Avra I never said the dictionary takes constant size. Nothing in what I wrote above implies that.

Avra

@user21820. Yes. I am just trying to tell you how I understand it. Yes, your answer is clear. This is how I tried to think about the question. Once we initialize a dictionary, which is basically an array, we should give it a size, say $M$, which is constant, please correct me if I am wrong?

user21820

@Avra You're wrong. A dictionary is not basically an array. A dictionary, or map data structure, is a specification of behaviour, such as I precisely defined above. It does not require using an array nor does it tell you how you must use it. Furthermore, if you just store the dictionary in the naive manner in an array, you would need to initialize the entire array otherwise you cannot tell which cells are empty.

So that method fails to satisfy the "O(1) time" requirement for init().

Avra

So this question is more under the hood details

It's about initialization

user21820

Yes, and this isn't an idle theoretical issue; for instance C's memset takes time linear in the size of the block being set, because you literally need to set every single memory cell.

So if you want to avoid doing that, you need a clever solution.

Avra

13:51

Wow!

This is related to compilers probably please?

user21820

No. This is a rather basic CS problem, and you should be able to solve it if you want to be able to develop other useful data structures in the future.

Avra

Thanks!

user21820

Compilers are far more complicated, and low-level compilers don't bother to optimize this, which is why C doesn't care to provide such an array feature as required by your problem.

Neither does Java by the way.

I'm not sure about Python; new versions might if you know how to use it well. (I don't.)

If you need any hints, I can drop you some, but you should try and see if you can figure it out on your own first.

Avra

That's fine! This much more than I expected

user21820

@Avra: You can imagine the A[1..M] as a gigantic room of shelves after shelves of small cells, each of which can hold a single paper sheet (representing a word), and initially every cell already has some arbitrary paper sheet in it. And you are the only one in the room and have to store data that people tell you to store. Each person has an id k and can ask you to store/update their data x (i.e. insert(k,x)) or erase their data (i.e. delete(k)) or recall their data (i.e. search(k)).

Prithu biswas

13:59

@user21820
Mine:
1. Two "triple case split".
2.Use of a lemma proven previously.
FZers:
1. One "Triple case split".
2. No lemma needed.

user21820

@Avra: Obviously, the "you" in this story are lazy and do not want to go through the room to initialize it, so you have to figure out a good way of storing their data so that you only have to modify O(1) paper sheets to initialize the room, and also only look at O(1) paper sheets for every person's request.

@Prithubiswas Yea it just so happened that you applied the discreteness axiom (the last one of PA−) to a different inequality rather than the given one, so missing the shorter proof. But it's good that you found that lemma on your own without me telling you about it!

F. Zer

@user21820 I have the list of axiomatisations ready. Is this good time to post those ?

Avra

@user21820. Wow! Thanks.

user21820

@F.Zer Yes post them and ping Prithu so that we can all refer to it. Also, it might be a good time to dump your lemmas and theorems in some never-expire pastebin and link from here, because it's getting harder to find lemmas that you have proven before!

If you want formatted title, post just the title first.

F. Zer

@user21820 Thank you :-)

user21820

14:08

Formatting is mostly disabled in a multi-line message, except quotes using ">".

F. Zer

PA- axioms:

Add the type ℕ and the symbols of PA, namely the constant-symbols 0,1 and the 2-input function-symbols +,· and the 2-input predicate-symbol < (ℕ is a discrete ordered semiring).
[closure] ∀x,y∈ℕ (x+y∈ℕ).
[closure] ∀x,y∈ℕ (x⋅y∈ℕ).
[ring] ∀x,y∈ℕ (x+y=y+x).
[ring] ∀x,y∈ℕ (x⋅y=y⋅x).
[ring] ∀x,y,z∈ℕ (x+(y+z)=(x+y)+z).
[ring] ∀x,y,z∈ℕ (x⋅(y⋅z)=(x⋅y)⋅z).
[ring] ∀x,y,z∈ℕ (x⋅(y+z)=x⋅y+x⋅z).
[ring] ∀x∈ℕ (x+0=x).
[ring] ∀x∈ℕ (x⋅1=x).
[order] ∀x∈ℕ (¬x<x).
[order] ∀x,y∈ℕ (x<y∨y<x∨x=y).
[order] ∀x,y,z∈ℕ (x<y∧y<z⇒x<z).

ℤ axioms:

Add the type ℤ, reuse the symbols and operations of PA, add the unary operation – and the binary operation – (ℤ is an ordered ring containing ℕ).
We can axiomatize ℕ,ℤ,ℚ,ℝ this way and it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that satisfies the axiomatizations here.
[closure] ∀x,y∈ℤ (x+y∈ℤ).
[closure] ∀x,y∈ℤ (x⋅y∈ℤ).
[closure] ∀x,y∈ℤ (x–y∈ℤ).
[ring] ∀x,y∈ℤ (x+y=y+x).
[ring] ∀x,y∈ℤ (x⋅y=y⋅x).
[ring] ∀x,y,z∈ℤ (x+(y+z)=(x+y)+z).

ℚ axioms:

Add the type ℚ, ℚ[≠0] = { x : x∈ℚ ∧ x≠0 }, reuse the symbols and operations of PA and add the binary operation / (ℚ is an ordered field containing ℤ).
We can axiomatize ℕ,ℤ,ℚ,ℝ this way and it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that satisfies the axiomatizations here.
[closure] ∀x,y∈ℚ (x+y∈ℚ).
[closure] ∀x,y∈ℚ (x⋅y∈ℚ).
[closure] ∀x,y∈ℚ (x-y∈ℚ).
[closure] ∀x∈ℚ ∀y∈ℚ[≠0] (x/y∈ℚ).
[ring] ∀x,y∈ℚ (x+y=y+x).

ℝ axioms:

Add the type ℝ and ℝ[≠0] = { x : x∈ℝ ∧ x≠0 }, the symbols of PA, namely the constant-symbols 0,1, the unary operation − : ℝ→ℝ, the binary operations +,·,- : ℝ^2→ℝ, the binary operation / : ℝ×ℝ[≠0] → ℝ and the 2-input predicate-symbol < (ℝ is an ordered field).
Add the type ℝ, ℝ[≠0] = { x : x∈ℝ ∧ x≠0 }, reuse the symbols and operations of PA and add the binary operation / (ℝ is an ordered field containing ℚ).
We can axiomatize ℕ,ℤ,ℚ,ℝ this way and it is non-trivial to actually construct ℤ,ℚ,ℝ in the base system (PA plus Set Theory) and extend the operations on ℕ to them in the manner that sa…

user21820

@F.Zer: Thank you very much! @Prithubiswas: You can refer to these if you would like to prove anything involving ℕ,ℤ,ℚ,ℝ later!

F. Zer

@user21820 You're very welcome !

@user21820 Yes, looking up proved lemmas is starting to complicate. I can also clean them up and maybe post a pastebin (or something similar).

user21820

Yes thank you for collating the whole (current) lot!

F. Zer

Glad to do it :-)

@user21820 I didn't reply to one of your recent comments. Maybe that is my current approach, but I am used to make everything "self-contained" (standalone). Do you think perhaps writing the lemma in this way would be good ?

∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ) ∧ ∀ a,x,y,z ∈ V ( ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ⇒ c(x,y) ∧ c(y,z) ∧ c(z,x) )

I am used to do that (self-contain) when programming, I should say.

user21820

14:26

@F.Zer Well, it's not a good habit even in programming! For example, if writing Javascript sometimes you have a function that uses an inner function that allows you to use closure features. Similarly here by putting the lemma at the innermost subcontext possible you get to actually conclude "⊥" in the lemma (similar to how closures let you use stuff that isn't valid outside).

In Java you also have inner classes for similar reasons.

Since probably nobody is interested in the lemma outside of the proof of that specific problem, there is no clear reason to put it in the global context.

(Don't tell me you haven't used closures or inner classes before! =P)

F. Zer

@user21820 Fortunately, I did use closures before :-)

@user21820 Sorry, I didn't clarify. I do that when doing functional programming. I don't use other paradigms. There, everything is self-contained.

@user21820 A function (in Haskell) only depends on its parameters. There is nothing "outside" I could take advantage of. You probably know this, but I am just saying.

So, that's why my brain is wired that way.

user21820

@F.Zer Even in purely functional programming, you can instantiate functions inside a function by some "where" mechanism, can't you?

F. Zer

@user21820 Good point. Let me think a bit about it.

user21820

@F.Zer: For example, the definition of a fixed-point operator:

proc fix(proc F) { return D(D) where D = proc(proc X) { return F( proc(obj t) { return X(X)(t); } ); }; }.

Obviously you can move the D outside, but can't many functional languages do it inside like I wrote?

F. Zer

14:42

@user21820 I don't know what's a fixed-point operator. Could you post a simpler function so I can translate it into a functional language ? :-)

user21820

@F.Zer That's the simplest useful purely functional operator that uses something twice in its definition and that something is practically useless elsewhere.

F. Zer

@user21820 Also, which language is this one ? Is it C ?

user21820

@F.Zer It's in pseudo-code.

"proc" stands for "procedure".

Like "function" but I don't like calling something a function when it possibly does not halt.

The fixed-point operator satisfies the property that F(fix(F)) has the same behaviour as fix(F). In other words, fix(F) is a fixed-point of F.

This can be used to implement recursion in a language that supports first-class procedures.

F. Zer

@user21820 Interesting. Never heard of it.

@user21820 How would you call that function and what would be the output, in that case ?

What's type does fix has ?

Can I call F(1), for example ?

user21820

No, as written above, fix requires a proc F as input, and returns some proc.

F. Zer

14:50

@user21820 Understood.

user21820

You can just expand the definition to see how it works. fix(F) returns D(D) where D = proc(proc X) { return F( proc(obj t) { return X(X)(t); } ); }, and D(D) returns F( proc(obj t) { return D(D)(t); } ). If F(Y) and F(Z) have the same (input-output) behaviour for every Y,Z with the same behaviour (✻), then F( proc(obj t) { return D(D)(t); } ) has the same behaviour as F(D(D)). Thus fix(F) has the same behaviour as F(fix(F)).

So it is a fixed-point operator that can be applied to any F that satisfies the stated condition (✻).

I like this big snowflake ✻. SE chat will never crush it into mush.

F. Zer

This is a little above my current level :-)

@user21820 That's good.

user21820

@F.Zer It's not above your level. Do you know javascript?

F. Zer

@user21820 My current mathematics level :-)

@user21820 Sure. I used JS a million times.

"If F(Y) and F(Z) have the same (input-output) behaviour for every Y,Z"

That's above my level.

user21820

Same input-output behaviour just means that on the same input they produce the same output (or both do not halt).

Javascript version: function fix(F) { var D=function(X) { return F( function(t) { return X(X)(t); } ); }; return D(D); };

F. Zer

15:03

@user21820 I still can't grasp when you explain in terms of such beautiful logic reasonings. I hope someday I'll be able to switch my mindset into that. It's currently out of my league.

user21820

Well, you can try actually running the JS version using pencil and paper.

F. Zer

@user21820 It seems so simple and clear. You start saying some definitions...and very soon I feel like someone stepping into a foreign country :-)

@user21820 I will do it.

user21820

Here is an example F: function F(Y) { return function(k) { if( k==0 ) return 0; return Y(k-1)+k; }; };

Try running fix(F)(k) for k∈{0,1,2,3,4}.

I just did (in browser console) and it works. =)

F. Zer

I will do that example now.

user21820

But you need to use your brain and pencil and paper otherwise you won't see how the magic happens.

It is natural for most people to feel like it is magic when they see it for the first time.

I think I had a bit of headache at first too.

F. Zer

15:12

@user21820 Someone is calling me. I will have to leave a moment and continue with this function when I come back. See you !

user21820

In case it isn't clear, the magic is that fix does not use recursion, nor does F, but fix(F) has the same behaviour as a recursive function that corresponds to F!! F is just a non-recursive function from functions to functions that satisfies (✻), but any fixed-point of F has the same behaviour as function s(k) { if( k==0 ) return 0; return s(k-1)+k; }!

@F.Zer See you! I'll be going soon so next time!

F. Zer

Take care !

F. Zer

17:16

@user21820 I've spent some time doing it but I realise that never ran a function "by hand". Could you give me a little hint ?

I mean, I've never done such complex functions in this style. I certainly executed foldTree from Haskell by hand.

Can I write the execution as a series of equalities ?

F. Zer

17:36

Mmm...I found something interesting. It seems I can't write your function in Haskell.

First, I rewrote it in a functional style (works):

const fix = F => {
    const D = X => F(
        t => X(X)(t)
    )
    return D(D)
};

Then, I translated to Haskell language:

fix' f = d d
  where
    d x = f (\t -> x x t)

I get the error: Couldn't match expected type ‘(t2 -> t3) -> t4’
              with actual type ‘p’
    because type variables ‘t2’, ‘t3’, ‘t4’ would escape their scope
  These (rigid, skolem) type variables are bound by
    the inferred type of d :: (t1 -> t2 -> t3) -> t4

I used fix' since fix was already taken.

user21820

I don't know Haskell so you'd have to use JS if you want me to help. Just run by hand; do what the computer is supposed to do. That's all.

F. Zer

@user21820 Good. I'll try and report back.

F. Zer

18:34

@user21820 Please, take a look at my question here: stackoverflow.com/questions/68975627/…

As I suspected, your function can't be translated to a purely functional language.

Transcript for

♦ $Mathematics$ Basic Mathematics

Transcript for

♦ Basic Mathematics

♦ $Mathematics$ Basic Mathematics