Newest Questions

0 votes

0 answers

14 views

Exercise 6.4 of Type Theory and Formal Proof (Nederpelt) asks us to derive the following type, and also derive an inhabitant, in the context $Γ ≡S : *, Q : S →S →*$ $$(Πx,y : S. (Qxy → Qyx → ⊥)) → Πz :...

1 vote

0 answers

22 views

According to Wikipedia's entry on binary heaps: The Build-Max-Heap function that follows, converts an array A which stores a complete binary tree with n nodes to a max-heap by repeatedly using Max-...

0 votes

0 answers

52 views

In Church-style STLC, the syntax of typed $\beta$-normal form is: Then, I am wondering how to define $\eta$-longest $\beta$-normal form inductively.

-3 votes

0 answers

45 views

How to solve this type of problem step by step? Like how to change the statements into logic, and then how to decide who is Knight and who is Knave in a simple way? I just want to know the clear ...

-3 votes

0 answers

18 views

I have a Lenovo ThinkPad E14 Gen 2 laptop and every day at midnight, if the laptop is plugged in, it shuts down. If the Computer isn't plugged in it won't shut down but the second I plug it in, it ...

0 votes

0 answers

19 views

I'm doing exercise 6.2 from Type Theory and Formal Proof. Exercise 6.2 Let $Γ ≡S : ∗, P : S →∗, A : ∗$. Prove by means of a flag derivation that the following expression is inhabited in λC with ...

2 votes

0 answers

37 views

does somebody know how to derive a formula for the number of non-isomorphic Moore machines with less than four states and binary input alphabet and binary output alphabet?

0 votes

0 answers

25 views

Chapter 6 of Type Theory and Formal Proof introduces the λ-cube with its 8 systems, differential primarily by how their (form) rules work, summarised in the table below. Question: I am a little ...

0 votes

1 answer

48 views

I was wondering about something. For a finite set $A$ with an equivalence relation $R,ドル I know we can find the cardinality of $R$ using the formula $$ |R| = \sum_{i=1}^{k} |C_i|^2 $$ where $C_1, C_2, \...

0 votes

1 answer

18 views

There's a class of mutices known as the "robust" mutex - when the thread holding the lock dies, the threads acquiring the lock will be notified of this failure. Q: Is there an equivalent of ...

-4 votes

0 answers

26 views

I am a new user to python and i want to use it primarily for data plotting, matlplotlib functions. I was using origin before but i want to shift to python. recently i had to plot some profiles and ...

0 votes

1 answer

27 views

SK combinators and the lambda-calculus are inductively-defined reduction systems. A nice online lambda-calculus interpreter is at https://lambdacalc.dev/ Question: what happens if instead of ...

3 votes

0 answers

59 views

I would like to know if there are any limitations to macro systems, like the ones that many LISP dialects have. Can all meta programming paradigms be implemented through a LISP-ish macro system? Or ...

1 vote

0 answers

29 views

how a computer store information on a hard drive how billion of bits fit into o a hard drive how millions of bit fit into a hard drive do atoms exist where is evidence that atoms exist how binary code ...

1 vote

1 answer

29 views

If you have a tree, there are two common ways to select a random leaf node from the tree: You can "flatten" out the tree, so that each leaf node gets selected with the same probability. ...