22
\$\begingroup\$

The name of this Stack Exchange site is "Programming Puzzles and Code golf" but I was wondering if other types of similar golf (not the sport) would be allowed or welcomed for questions. In particular I was thinking about proof golf. Where a statement in Propositional Calculus or First Order Logic is given and the goal is to create a proof using as few axioms of the system.

These types of puzzles are very much like code golfing in practice but they are certainly not code golf or a programing puzzle. I thought it might make a fun one-off challenge, but on the other hand it might be a bit out of scope for this site.

\$\endgroup\$
  • \$\begingroup\$ For the most part, a challenge needs to involve writing code, since that's what most of us are here for. We have a few different challenge types that vary the method or difficulty of the problem solving required, though. \$\endgroup\$ – mbomb007 Oct 11 '16 at 21:04
  • 2
    \$\begingroup\$ History lesson: This site is (kind of) an off-shoot from Stack Overflow. Certain programming "challenges" were posted on SO, and that gave people the idea to create PPCG as a beta site, which has now graduated. \$\endgroup\$ – mbomb007 Oct 11 '16 at 21:06
  • 2
    \$\begingroup\$ Related: Objective computational challenges without “code” \$\endgroup\$ – Dennis Oct 11 '16 at 21:07
  • \$\begingroup\$ Yes, that's a nice question about it. Though it's allowed, you might want to try the Sandbox first, since many users might think it off-topic if not worded well. \$\endgroup\$ – mbomb007 Oct 11 '16 at 21:09
  • \$\begingroup\$ I saw this shortest logical proof contest on math SE. \$\endgroup\$ – xnor Nov 1 '16 at 2:07
36
\$\begingroup\$

Yes, this is

Or, it's what atomic code golf should be. Take a look at

All of them define a mini-language by listing a limited set of allowed operations, and ask for a task to be done in as few of these operations as possible.

In the same vein, one could have a challenge to construct a regular pentagon in as few ruler-and-compass operations, writing out the operation like "draw a circle with the given point and the current radius", "mark a point at the intersection of two lines", and so on. One could write an interpreter for this language, where each operation is a code instruction, the current picture is the program state, and so on. The result is a challenge like code golf, except that:

  • All submissions must be in the given invented language
  • Rather than minimizing characters, one minimizes operations

Your first reaction might be, "but that's not a programming language, it's geometry!". But why? Perhaps the NAND gate language feels like programming because logic gates happen to be what computers use. It's just association. We already use esoteric languages where a "program" is

And anyone is free to make their own language. Using weird languages is a point of pride in the community. So let's not call something "not programming" for not looking like a typical programming language.

Formal proofs, which OP used as an example, have a particularly close relationship to programming. The Curry-Howard correspondence, aka the proofs as programs interpretation, gives a formal mathematical equivalence between proofs and programs. A challenge to prove a statement in a formal system could be rephrased as writing a program that instantiates a given type.

\$\endgroup\$
  • \$\begingroup\$ The One could write an interpreter for this language part is both essential (we usually require a language to have an interpreter, although I can't find the meta post) and possibly hard (write an interpreter just for a challenge) \$\endgroup\$ – Luis Mendo Oct 25 '16 at 15:59
-1
\$\begingroup\$

No.

We're a programming site. Thus, all submissions (and therefore challenges) must involve the use of code*.

* A programming language which is executable through a digital interpreter.

\$\endgroup\$
  • 1
    \$\begingroup\$ So if the challenge author wrote an online interpreter where the characters 0-9 applied the corresponding axioms to (-a) * (-a), it would be acceptable? Why would going through all that effort to create a digital interpreter instead of writing out the steps change the underlying question? And if it’s still not acceptable, how is it different from creating other programming languages? \$\endgroup\$ – MildlyMilquetoast Oct 5 '17 at 18:33

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .