this post was submitted on 28 Mar 2024
33 points (100.0% liked)

Programming

17443 readers
151 users here now

Welcome to the main community in programming.dev! Feel free to post anything relating to programming here!

Cross posting is strongly encouraged in the instance. If you feel your post or another person's post makes sense in another community cross post into it.

Hope you enjoy the instance!

Rules

Rules

  • Follow the programming.dev instance rules
  • Keep content related to programming in some way
  • If you're posting long videos try to add in some form of tldr for those who don't want to watch videos

Wormhole

Follow the wormhole through a path of communities !webdev@programming.dev

founded 1 year ago
MODERATORS
snowe@programming.dev
Ategon@programming.dev
MaungaHikoi@lemmy.nz
33
Why focus on formal language in theory of computation? Most programs do more than merely accept or reject an input (lemy.lol)
submitted 7 months ago by matcha_addict@lemy.lol to c/programming@programming.dev
9 comments fedilink hide all child comments
 

While reading Sipser's book on theory of computation, it relies heavily on the concept of formal language, and machines that merely accept or reject an input.

But most useful programs we deal with do more than merely verify an input. They compute something. We may compute a solution for an equation instead of merely verify it. We may sum a list of numbers, or calculate some function on it.

Maybe "most" is an exaggeration since I can't prove it. But still, it begs the question. Why not deal with machines than do more than merely verify?

all 10 comments
sorted by: hot top controversial new old
[–] Corbin@programming.dev 23 points 7 months ago

It's because most of the hard questions and theorems can be phrased over the Booleans. Lawvere's fixed-point theorem, which has Turing's theorem and Rice's theorem as special cases (see also Yanofsky 2003), applies to Boolean values just as well as to natural numbers.

That said, you're right to feel like there should be more explanation. Far too many parser papers are written with only recognition in mind, and the actual execution of parsing rules can be a serious engineering challenge. It would be nice if parser formalisms were described in terms of AST constructors and not mere verifiers.

[–] Azzu@lemm.ee 8 points 7 months ago (1 children)

I'm not an expert in formal languages at all... But when I read your question, I was like "really?"

I mean yeah, when we talk about a program's purpose we don't often say "it verifies an input". But what is verifying an input really? Deciding if a statement is true or false. And if you really want to, you can deconstruct almost anything any program does into components of that.

Should this UI element be displayed? Input: page visit, user, users preferences. Output: reject/confirm. Should the UI element be red? Should it be green?

And so on and so on for literally everything. Yeah, formal language theory is not strictly required for doing that, but it still is the foundation that is abstracted away. Same as you don't need to know about the theory behind mathematical operations and classes and sets to do 1+1.

[–] matcha_addict@lemy.lol 6 points 7 months ago (2 children)

How would you represent something like "sum a list of numbers" as components of verifiers?

[–] KindaABigDyl@programming.dev 6 points 7 months ago* (last edited 7 months ago)

Here's how I think it works

In formal language, what it means to accept a verification means does the result fall into the list of acceptable values.

Consider adding two 2-bit numbers:

  • Alphabet: { 0, 1}
  • Language: { x | x consists of four binary digits representing two 2-bit binary numbers where the result of adding these two numbers is a valid 2-bit binary number (i.e. falls between 00 and 11) }
  • Then you have an automata that will:
    • Start from the rightmost bit
    • Add the corresponding bits (+ carry from any previous iterations)
    • Carry over to the left if needed
    • Repeat for both bits
    • Check for acceptance
  • Machine as a whole simply checks did the inputs produce a valid 2-bit number, so it just accepts or rejects

The machine itself simply holds this automata and language, so all it does is take input and reject/accept end state. I think you're just getting caught up in definitions

A sum of a list of numbers I think would be something like

  • Alphabet: digits 0-9 and ','
  • Language: a single string of digits or a single string of digits followed by a comma and another valid string
  • Automata:
    • Are we a single string of digits? If yes, accept
    • Sum the last number into the first and remove the comma
    • Repeat
  • Machine: Does the some operation result in a valid string?

Machines accept a valid state or hit an error state (accept/reject). The computation happens between the input and accept/reject.

But maybe I don't understand it either. It's been a while since I poked around at this stuff.

[–] Phoenix3875@lemmy.world 3 points 7 months ago (1 children)

For all possible input, only recognize the one input that's (under certain encoding scheme) equal to the sum of the given list. That's for a given list.

Another more general approach is that, only recognize the input if (under certain encoding), it's a pair of a list and a number, where the number is the sum of the list.

[–] Phoenix3875@lemmy.world 3 points 7 months ago* (last edited 7 months ago)

In general, given a Turing machine which outputs the result of a procedure to its memory tape, you can equivalently construct a recognizer of valid input/output pairs. Say P is the procedure, then the recognizer R is let (i, o) = input in P(i) = o

The reverse is also possible. Give a recognizer R, you can construct a procedure P that given part of the input (can be empty), computes the rest of the input that makes R accept the whole. It can be defined as for o in all-strings, if R(i, o) then output o and halt, else continue.

It might feel contrived at first, but both views can be useful depending on the situation. You'll get used to it soon with some exercises.

[–] abhibeckert@lemmy.world 8 points 7 months ago* (last edited 7 months ago) (1 children)

But most useful programs we deal with do more than merely verify an input [...] We may sum a list of numbers [...]

Computers are binary. 1 or 0. Pass through the electrical gate; or do not pass through the gate. That's the only tool we've got to work with and therefore, "sum a list of numbers" is literally implemented as a series of "accept or reject" steps.

Everything above that is a convenient layer of abstraction. Abstraction is there to reduce your mental load while working but it doesn't always achieve that goal — especially if you don't know what's going on underneath.

[–] matcha_addict@lemy.lol 4 points 7 months ago

I suppose you're right. But I thought the reason we are using conceptual models of computation is to not concern ourselves with the implementation details of the physical world and real computers. It's why we have an infinite tape, for example.

Representing a "sum a list of numbers" problem in terms of binary logic gates would be the opposite of that. We're complicating the problem. Turing machines as I've seen them are not that low level. Would binary addition be the sensible way to sum a list of numbers in a turing machine?

Your answer is still convincing though... I suppose we can represent functions as series of verifiers. But my only remaining point of confusion is... Is that really the better way?

[–] solrize@lemmy.world 2 points 7 months ago

Language recognition is a useful framework for complexity theory. There are also "counting problems" and complexity classes for them, like #P:

https://en.m.wikipedia.org/wiki/%E2%99%AFP

If you're looking at numerical calculations from a theoretical standpoint, there is a variant of Turing machines for that, with a lot of really nice results:

https://en.m.wikipedia.org/wiki/Blum%E2%80%93Shub%E2%80%93Smale_machine