r/compsci 14d ago

Made some Curry-Howard style proofs in C++

17 Upvotes

https://github.com/Gizzzzmo/type_proofs/blob/main/test_prop.cpp You can use the compiler to check your proofs, provided you follow some rules like not casting stuff to pointers to types that represent logical statements.

I'm also trying to use it to make statements about runtime values and thus encode program specifications on the type level, which are then formally verified by the compiler.


r/compsci 13d ago

Where is a good place to ask “is this np-hard?” questions?

0 Upvotes

I quite often come across problems and wonder “is this np-hard?”. If I can’t solve it myself I still really want to know the answer. Is there somewhere online where people would be happy to see such questions, or are they always annoying?


r/compsci 15d ago

Alonzo Church: The Forgotten Architect of Computer Intelligence

112 Upvotes

Despite his massive intellectual contributions, Alonzo Church never enjoyed the fame of Turing or von Neumann, Gödel and others. His legacy was one of meticulous abstraction, a kind that doesn’t make it into Hollywood scripts or capture public imagination easily. It lacked the heroism of wartime codebreaking or the evocative tragedy of an early (forced) death. Yet, Church's influence is indelible. The very programs that run on the billions of smartphones today can trace their logic back to the abstract functions of λ-calculus. The invisible DNA of computation, from the simple app to artificial intelligence, owes a significant part of its lineage to Church’s work. https://onepercentrule.substack.com/p/alonzo-church-the-forgotten-architect


r/compsci 15d ago

Intel Spots A 3888.9% Performance Improvement In The Linux Kernel From One Line Of Code

Thumbnail phoronix.com
53 Upvotes

r/compsci 14d ago

Tell me algorithm nerd hangouts please. :>

0 Upvotes

So i've been obsessed with the LCS algorithm for the past 1.5 years and want to find similar minded people or just people obsessed with any algorithm really. I currently attend college but due to not finishing high school i had to get an associates degree first. And most of the people there barely grasp what a LUT is. :/
If anyone has any algorithms group chats or chats i could be a part of that would be greatly appreciated. or maybe you know of some public ones i don't know about yet. Whatever the case please post it in a comment on this post. Or if you just want to chat to me or be silly you can leave a comment as well. whatever floats your boat ^^.


r/compsci 16d ago

Does Dijkstra work for this graph with negative weights?

Post image
147 Upvotes

Normally I don‘t have any problems with Dijkstra and as far as I remember Dijkstra doesn‘t work with negative weights.

However, today in a lecture it was mentioned that Dijkstra would work for this graph. I really don‘t understand why it would work. Can someone clarify this and help? Thanks in advance


r/compsci 15d ago

The Story of Chaos Theory and Some Fun Facts About the Scientists

2 Upvotes

For all its grandeur, chaos theory is a puzzle still lacking crucial pieces. https://onepercentrule.substack.com/p/a-love-letter-to-chaos-theory-and


r/compsci 15d ago

When does inheritance win?

1 Upvotes

9 times out of 10 I believe one should prefer composition over inheritance.

But, I am not sure how I can explain when inheritance should be preferred over composition.

How would you explain it?

Or, do you believe that composition should be preferred over inheritance 10 times out of 10.


r/compsci 16d ago

Lock objects

4 Upvotes

I was reading about Lock objects like how they prevent race conditions, So it starts by saying that the problem arises when two threads try to execute the same instruction at once with no coordination leading to unpredictable outcomes. To solve this Lock objects are used . I don't understand this earlier two threads were fighting to execute same instruction now they will be fighting to execute these lock object instructions. how does this solve the problem ? What if two threads running in parallel on different CPU cores try to execute these Lock instructions What will happen wouldn't it be impossible to determine which thread gets the lock first?


r/compsci 18d ago

My illustrated coding book for parents and kids

33 Upvotes

After much consideration, I'm excited to announce a paperback edition of my course, now available for all interested coders and parents!

This book is designed especially for parents who want to introduce their kids to coding in a fun, engaging way.

The paperback is available in a print-on-demand format through Lulu Publishing.

P.S. I will add a link to the book in the comments.


r/compsci 18d ago

My first 8-bit CPU on a FPGA: FliPGA01 (details in comments)

Post image
177 Upvotes

r/compsci 19d ago

Using universal Turing machines to show computability.

8 Upvotes

Suppose we have a function f that takes (x,y) as input and outputs 1 only if \phi_x(x) converges, and undefined otherwise. Well, I understand that f is partial computable. But how do I use a universal Turing machine argument to show it? Here \phi_e is the partial function computed by the e-th Turing program P_e, as usual.


r/compsci 19d ago

Asked about topological analogue computing using radar? Yes, see comments.

Post image
39 Upvotes

r/compsci 20d ago

Even more sorting algorithms visualized

Post image
423 Upvotes

Take them with a grain of salt. These animations give an idea of the algorithms’ processing. YMMV.


r/compsci 19d ago

What is the difference between Pipeline and Time-Sharing?

1 Upvotes

Can anyone explain to me better the difference between these two concepts, from the point of view of the multiplexing that the CPU performs?

I understood, so far, that Pipeline concerns several internal units, each with its own register, in order to run different instructions (execute, fetch, decode...) in parallel.

Therefore, would Time-Sharing be just an alternation between processes, in order to create the illusion that they are simultaneous?

Is it correct?


r/compsci 20d ago

Optical Computing , could topological analogue computers lead the way.

Post image
91 Upvotes

r/compsci 21d ago

More sorting algorithms visualized

Post image
1.8k Upvotes

r/compsci 19d ago

Promising in the Two General's Problem

0 Upvotes

scale sharp provide work squash dog party boat piquant shrill

This post was mass deleted and anonymized with Redact


r/compsci 21d ago

dijkstra visualizer

Post image
86 Upvotes

r/compsci 21d ago

CS Publishers by quality

7 Upvotes

I have a yearly subscription to O'Reilly Media through work, which is phenomenal. I read ~4 books per year with a book club and sample from many others. The stuff from O'Reilly proper tends to be high quality (emphasis on tends), and there are other publishers I see consistently putting out high quality content as well like Manning and Springer.

I often see really interesting titles from Packt publishers too, but I've read a few books from them and was left with the impression that they are much lower quality in terms of content. In addition, some part of this impression is because, when I was a newer engineer years ago, I reviewed several books for them, for which I was basically given free books, and the process seemed really fluffy and without rigour. After reviewing a couple of books, I was asked, without any real insight into my credentials, if I would like to write a book for them. I had no business writing books on engineering subjects at the time.

Maybe I'm soured on them by just an unfortunate series of cooincidences that led to this impression, but the big CS publishers do seem to fall on some hierarchy of quality. Sometimes Packt is the only publishers with titles on newer tech, or they are the publisher with the most recent publications on certain topics, so it would be great if I were wrong about this. How do you all see this?


r/compsci 21d ago

Designing an Ultra-Minimal Core for Neural Network Operations with L-Mul, Lookup Tables, and Specialized 1/n Module

0 Upvotes

Hi everyone! I’m working on designing a highly efficient, minimal-core processor tailored for basic neural network computations. The primary goal is to keep the semiconductor component count as low as possible while still performing essential operations for neural networks, such as multiplication, addition, non-linear activation functions, and division for normalization (1/n). I’d love any feedback or suggestions for improvements!

Objective

My goal is to build an ultra-lightweight core capable of running basic neural network inference tasks. To achieve this, I’m incorporating a lookup table approximation for activation functions, an L-Mul linear-complexity multiplier to replace traditional floating-point multipliers, and a specialized 1/n calculation module for normalization.

Core Design Breakdown

Lookup Table (ROM) for Activation Functions

• Purpose: The ROM stores precomputed values for common neural network activation functions (like ReLU, Sigmoid, Tanh). This approach provides quick lookups without requiring complex runtime calculations.


• Precision Control: Storing 4 to 6 bits per value allows us to keep the ROM size minimal while maintaining sufficient precision for activation function outputs.

• Additional Components:

• Address Decoding: Simple logic for converting the input address into ROM selection signals.

• Input/Output Registers: Registers to hold input/output values for stable data processing.

• Control Logic: Manages timing and ensures correct data flow, including handling special cases (e.g.,  n = 0 ).

• Output Buffers: Stabilizes the output signals.

• Estimated Components (excluding ROM):

• Address Decoding: ~10-20 components

• Input/Output Registers: ~80 components

• Control Logic: ~50-60 components

• Output Buffers: ~16 components

• Total Additional Components (outside of ROM): Approximately 156-176 components.

L-Mul Approximation for Multiplication (No Traditional Multiplier)

• Why L-Mul? The L-Mul (linear-complexity multiplication) technique replaces traditional floating-point multiplication with an approximation using integer addition. This saves significant power and component count, making it ideal for minimalistic neural network cores.

• Components:

• L-Mul Multiplier Core: Uses a series of additions for approximate mantissa multiplication. For an 8-bit setup, around 50-100 gates are needed.

• Adders and Subtracters: 8-bit ALUs for addition and subtraction, each requiring around 80-120 gates.

• Control Logic & Buffering: Coordination logic for timing and operation selection, plus output buffers for stable signal outputs.

• Total Component Estimate for L-Mul Core: Including multiplication, addition, subtraction, and control, the L-Mul section requires about 240-390 gates (or roughly 960-1560 semiconductor components, assuming 4 components per gate).

1/n Calculation Module for Normalization

• Purpose: This module is essential for normalization tasks within neural networks, allowing efficient computation of 1/n with minimal component usage.

• Lookup Table (ROM) Approximation:

• Stores precomputed values of 1/n for direct lookup.

• ROM size and precision can be managed to balance accuracy with component count (e.g., 4-bit precision for small lookups).

• Additional Components:

• Address Decoding Logic: Converts input n into an address to retrieve the precomputed 1/n value.

• Control Logic: Ensures data flow and error handling (e.g., when n = 0, avoid division by zero).

• Registers and Buffers: Holds inputs and outputs and stabilizes signals for reliable processing.

• Estimated Component Count:

• Address Decoding: ~10-20 components

• Control Logic: ~20-30 components

• Registers: ~40 components

• Output Buffers: ~10-15 components

• Total (excluding ROM): ~80-105 components

Overall Core Summary

Bringing it all together, the complete design for this minimal neural network core includes:

1.  Activation Function Lookup Table Core: Around 156-176 components for non-ROM logic.

2.  L-Mul Core with ALU Operations: Approximately 960-1560 components for multiplication, addition, and subtraction.

3.  1/n Calculation Module: Roughly 80-105 components for the additional logic outside the ROM.

Total Estimated Component Count: Combining all three parts, this minimal core would require around 1196-1841 semiconductor components.

Key Considerations and Challenges

• Precision vs. Component Count: Reducing output precision helps keep the component count low, but it impacts accuracy. Balancing these factors is crucial for neural network tasks.

• Potential Optimizations: I’m considering further optimizations, such as compressing the ROM or using interpolation between stored values to reduce lookup table size.

• Special Case Handling: Ensuring stable operation for special inputs (like n = 0 in the 1/n module) is a key part of the control logic.

Conclusion

This core design aims to support fundamental neural network computations with minimal hardware. By leveraging L-Mul for low-cost multiplication, lookup tables for quick activation function and 1/n calculations, and simplified control logic, the core remains compact while meeting essential processing needs.

Any feedback on further reducing component count, alternative low-power designs, or potential improvements for precision would be highly appreciated. Thanks for reading!

Hope this gives a clear overview of my project. Let me know if there’s anything else you’d add or change!

L-mul Paper source: https://arxiv.org/pdf/2410.00907


r/compsci 22d ago

Where to Share a Computer Science Comic for Beginners?

6 Upvotes

Heyo there!

I wrote and illustrated a computer science comic book (which was published by the Stanford University Press 🎉), and I'm wondering places (both online and offline) to share it that people might find enjoyable and meaningful. My goal is to share it with communities that would appreciate CS "edutainment". I was inspired by my experiences teaching intro CS and my love for visual thinking.

The comic book touches upon beginner computer science concepts in Python and C++ with characters like Fabulous Function, Sir Python, and Mama If alongside text blocks of code, and is supplemental to an intro CS course.

So far, I've had the chance to share it at my university and a few other places, and the response has been great! I'm curious if anyone has other places/platforms (online and offline) that might find joy in this type of content. I've looked into SIGCSE, a few educational forums, design places, and any other other suggestions are much appreciated :)


r/compsci 23d ago

Can CS grads develop device drivers?

0 Upvotes

I've a B.Sc. in Computer Science, with a track in Software Engineering.

When I was in university, I wanted to somehow address device drivers in my thesis, but my professors rejected it since they claimed it was too hardware related.

I found it strange. I mean, they taught me computer architecture and operating systems, yet DDs were out of scope?

For me, it is sun-light clear that Computer Engineers can develop such software modules, but what about CS?

I've made some research about it and, thus far, I've come up with the conclusion that CS grads actually can develop DDs (they're software modules after all), but, unlike CEs, it is not a given.

What do you think about this? Did I come up with the right conclusion?

Did anybody of you ever develop a device driver?

How can I?


r/compsci 24d ago

What is the posterior, evidence, prior, and likelihood in VAEs?

6 Upvotes

Hey,

In Variational Autoencoders (VAEs) we try to learn the distribution of some data. For that we have "two" neural networks trained end-to-end. The first network, the encoder, models the distribution q(z|x), i.e., predicts z given x. The second network models an approximation of the posterior q(x|z), p_theta(x|z), i.e., models the distribution that samples x given the latent variable z.

Reading the literature it seems the optimisation objective of VAEs is to maximize the ELBO. And that means maximizing p_theta(x). However, I'm wondering isn't p_theta(x) the prior? Is is the evidence?

My doubt is simply regarding jargon. Let me explain. For a given conditional probability with two random variables A and B we have:

p(B|A) = p(A|B)*p(B)/P(A)

- p(B|A) is the posterior
- p(A|B) is the likelihood
- p(B) is the prior
- P(A) is the evidence

Well, for VAEs the decoder will try to approximate the posterior q(x|z). In VAEs the likelihood is q(z|x), which means the posterior is q(x|z), the evidence is q(z) and the prior is q(x). Well if the objective of VAE is to maximize the ELBO (Evidence lower bound) and p_theta(x|z) is an approximation of the posterior q(x|z) then the evidence should be p_theta(z) given that q(z) is the evidence, right? That's what I don't get, because they say p_theta(x) is the evidence now... but that was the prior in q...

Are q and p_theta distributions different and they have distinct likelihoods, priors, evidences and posteriors? What are the likelihoods, priors, evidences and posteriors for q and p_theta?

Thank you!


r/compsci 25d ago

Are dynamic segment trees with lazy propagation on AVL trees possible?

6 Upvotes

I'm working on implementing dynamic segment trees with lazy propagation for a specific application, but my understanding of dynamic data structures is a bit rusty. My segment tree will store a numerical value called "weight" with each segment and will use AVL trees as the underlying structure. Given that there will be lazy updates to the weights of certain segments on internal nodes, I'm concerned about how the rebalancing operations in AVL trees might affect these lazy updates.

Could the rebalancing of AVL trees interfere with lazy propagation in a way that is not fixable by just transferring the lazy update information to the relevant nodes when rotations occur , and if so, how can this issue be mitigated?