The Nineteenth Byte

orlp

5:18 PM

@user56656 by the way

I wasn't trying to answer

at least not myself

I was trying to write a program to answer :)

user56656

Ah nice!

orlp

hence my passionate objection to making it seem as if there was a 'n=1 lookahead' deductive reasoning solution :P

user56656

I've been writing a paper on find short proofs in ŁS myself.

orlp

I'm honestly more interested in automatic systems to generate proofs here than the golf itself

@user56656 a lot of my googling of ŁS led to some 'infinite valued logic', I assume that that is not the same thing?

user56656

Probably not I don't know anything about infinite valued logic

orlp

5:21 PM

some resources were describing what you were in the challenge (the three axiom system + modus ponens), but others were talking about that

and most things I can google regarding automated theorem proving are either first-order logic or using CNF techniques

no axiomatic constructions of propositional logic

user56656

That's probably because propositional logic is decidable, so there is not as much motivation to find proofs when you can just grind it through a SAT solver.

orlp

@user56656 that's what I mean with CNF techniques

they just put everything in conjunctive normal form and go from there

user56656

Yep, I was just agreeing.

orlp

I might ask a question on CS.se

user56656

bredth first search will work.

orlp

5:27 PM

be more specific

because I considered that

user56656

Well take my example in the question ...

orlp

but the branching factor is infinite from what I could see

user56656

@orlp not if you are clever about how you do things.

orlp

I also did an attempt that looks like your example

but I couldn't get the substitution correct

it was very confusing

user56656

substitution?

orlp

5:29 PM

yes

for example

you're substituting ψ → (φ → (A → A)) with (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))

finding appropriate expressions for φ ,ψ, χ

user56656

Oh yes

wait one sec

orlp

and I made a little destructuring algorithm for it

user56656

github.com/criscm2/Logic-Final

orlp

but I wasn't careful enough with the variables, so it was kinda buggy

user56656

^ that is the github repo I'm using for my paper, the tex is a bit of a mess but the haskell file there does the "substitution", we call it "intersection".

orlp

5:32 PM

I called it pattern matching :P

but it became a bit unclear to me because after you've 'destructured' the pattern so to speak

user56656

Hm? I'm not sure what you mean.

orlp

you might have expressions that are now defined and need to be expanded into different goals introduced by modus ponens, etc... I didn't exactly know where contradictions would come up

like

going from this step:

φ
ψ
ψ → (φ → (A → A))
φ → (A → A)        M.P.
A → A              M.P.

to this step:

A → χ
A → (χ → A)
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A)                   M.P.
A → A                               M.P.

there is a LOT going on

first you need to match ψ → (φ → (A → A)) with (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))

(which again, shares variable names which is confusing)

let me change that for a sec

user56656

The program I linked will tell you what global substitutions need to be made, when trying to connect statements.

orlp

first you need to match ψ → (φ → (A → A)) with (α → (β → γ)) → ((α → β) → (α → γ))

but there are many different variables here, and a solution won't assign all of them, yes still be a match

ψ = (α → (β → γ)), φ = (α → β), α = A, γ = A

user56656

I'm not sure what you mean ...

https://tio.run/##tVTNbhMxEL77KUarShsryqE9RhhRUJBAwKWIS1VFs4nTXbHZTXedRIhyRbwO8B7tI4WxHXttVy1cSA7x/HzfzHz2pMT@s6zrw2GJCuFCoZJr2SgQ8GYVmMPpFj7I68g@V@0aXpXY0fkTdhUWtbT2UnbVrmquYXbDWNX0CpuFhIuy3QcE@1J2kkGvvSMqilBw0B8B2SiD8diGUJ8ymDyHwVcYH88cWneGFqzRkwDtUkyz6ArgNPNg3zpFBeRf8ylFv2WMGWVmN9tqh7XUA4jIMpP6cdI5w8xo0jCwKDvolStLFhUGQZOOxya5J9pF2ygkbphOA/FIjsh42bb1kEpS0p0gCEEHAR@7rRyCRutTwDNOQS3GADvVuNvAcQZFADzKXDihw3pBmpF67vIEvMa6D@t7wU2Oi7NObmokUdI5Q8HCsT0gusFI3x12Da6l0Zg5RZxTaHnJ2Sq6nn3VS9vtQDYUcK9Tam67IiMXROvlg6dwnoHgqJzFE4G2TyCh8On4wms4t8@VMSaDuZ58Cu/xSyHhMtDhKkb7cfRhAUuuVRi93fbK9vGu0no9m0AIQsoUsFr…

orlp

5:41 PM

errors

user56656

did you hit see full text?

orlp

now I did

so the counterintuitive part is that there isn't a clear "needle" and "haystack"

caird coinheringaahing

@Christopher I think your latest edit to the Sandbox seems better fitted to be a comment, so I'm rolling it back and would like to ask you to post it as a comment below the question

orlp

if we see a greek letter as a wildcard

you're essentially matching two words with wildcards

whereas in most pattern matching problems you're dealing with a situation where only one of the two operands has wildcards

user56656

Oh I see.

caird coinheringaahing

5:44 PM

If you disagree, of course, rollback my rollback. Just wanted to make you aware

orlp

@user56656 so that was quite confusing for me

user56656

Yes, I see how that could be confusing. I'm glad the thought never occurred to me that this was a wildcard problem.

orlp

@user56656 the algorithm, did you get it from some literature/reference?

user56656

No, I wrote it myself. I'm supposed to finish the proof of the algo today, would you like me to send that to you when I am done?

orlp

I guess :P

user56656

5:48 PM

If you don't think you are going to read it, I wouldn't be offended if you said no. it just seemed like you were asking for literature.

orlp

I'll skim over it but a proof is less what I need than an explanation ^^

I mean what I wrote is I think correct

now that I think about it in a slightly different way

I think I should think of it as introducing as many new variables as needed, no questions asked

then match as deep as possible

and any variables that got assigned propagate those

if that leads to a contradiction, reject the pattern match

user56656

yep that's it.

orlp

too bad I don't know haskell :P

this sounds made for haskell

from what I know about haskell

user56656

It does fit very well for Haskell. Writing the program was sublime.

orlp

I think I might write it in rust (did it in Python for my prototype) for the speed

because breadth first search isn't particularly... fast

user56656

5:53 PM

The one hiccup I would mention is that you need to screen out things like φ ∩ (φ → φ) where a variable is matched to an expression containing that variable.

orlp

@user56656 can you elaborate? also there is no ∩

user56656

There is no match for φ and (φ → φ) because φ is contained within (φ → φ). My first draft of the program would have no problem "resolving" this match.

orlp

huh?

how would that not match A ∩ (A → A)?

user56656

I was using the ∩ symbol to mean match

orlp

∩ has a pretty clear meaning in logic :P

user56656

5:57 PM

φ ∩ (φ → φ) means φ match (φ → φ)

orlp

also, that is wrong again, that's where I got confused

there is no such thing as sharing variables between the left and right

the variables on the left and right refer to different things

H.PWiz

@user56656 With regards to the recent edit, I had already seen this proof. It is pretty hard to follow and definitely longer than it needs to be

user56656

Oh, in my version the left and right can share variables, we need it so that we can reduce statements that are already in the proof.

orlp

@user56656 ah like that

in that case

how do you prevent this?

New Main Posts

0

Q: Make a Emergency Corridor

In some nations there are recommendations or laws on how to form emergency corridors on streets that have multiple lanes per direction. (In the following we only consider the lanes going in the direction we are travelling.) These are the rules that hold in Germany: If there is only one lane, e...

user56656

6:01 PM

Well I have a base case equivalence (Variable A) B, I check if Variable A appears in B, if it does return Nothing otherwise assign Variable A to B

orlp

I think calling these variables is very dangerous

user56656

@H.PWiz I'm not siked about the metamath proof, but I do think that Metamath might be useful and it could help people who don't have very good ideas about the overall structure of their proof get a foothold.

orlp

that's where I went wrong at first

user56656

They are called free variables, I didn't come up with the name.

There might be a better name but I just went with what I was familiar with.

orlp

@user56656 the wiki page on propositional calculus calls them schemata

user56656

6:05 PM

schemata refers to the rule as a whole, free variable refers to the things that are represented with greek letters.

orlp

Propositional calculus

Propositional calculus (also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic) is the branch of logic concerned with the study of propositions (whether they are true or false) that are formed by other propositions with the use of logical connectives. First-order logic extends propositional logic by allowing a proposition to be expressed as constructs such as "for every", "exists", "equality" and "membership", whereas in proposition logic, propositions are thought of as atoms. == Explanation == Logical connectives are found...

Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Schemata, however, range over all propositions. It is common to represent propositional constants by A, B, and C, propositional variables by P, Q, and R, and schematic letters are often Greek letters, most often φ, ψ, and χ.

user56656

Hm. Ok.

New Sandboxed Posts

6:35 PM

0

A: Sandbox for Proposed Challenges

Is the program 32 or 64 bits? Challenge is simple to explain: write the shortest code you need to determine supplied as a parameter is 32 or 64 bits on your platform. If there is a different kind of bitness, you can also do for it, but is not mandatory. What I really don't want is telling me y...

caird coinheringaahing

6:45 PM

Is anyone here experienced with making quines in esolangs?

maxathousand

6:56 PM

Just wanted to say that I've never posted an answer here, but I enjoy reading the challenges and answers. I like that this community is one of the few on SE that's consistently constructive. +1 to all of you.

flawr

@maxathousand I'd say we are just fast enough to make the not-so-constructive parts disappear before you get to see them :)

J. Sallé

@maxathousand What flawr said. Also, feel free to post an answer to any challenge, we like new people.

caird coinheringaahing

We don't bite... much :P

Erik the Outgolfer

@maxathousand and don't be afraid to "necro-post", we encourage it!

flawr

@J.Sallé Don't worry, every lurker will get addicted at some point:)

maxathousand

7:01 PM

@flawr Hahha, that might be true.. I've looked at some of yall's edits!

flawr

@maxathousand I just posted a rather easy challenge that you could try: codegolf.stackexchange.com/questions/161281/…

maxathousand

@EriktheOutgolfer Maybe I will someday! I'm a software engineer, but I'm encouraged specifically not to write code like you guys usually do, for good reason! I'll have to put the effort into learning all of the usual tricks at some point. Probably start with Javascript, as that's mostly what I work with every day.

J. Sallé

@flawr been there, done that.

maxathousand

@flawr That's actually the one I was just looking at! Maybe after work I'll give it a go!

caird coinheringaahing

@maxathousand If you use JavaScript a lot, but don;t want to start golfing your professional code, you could take a look at Japt, which is a golfing language transpiled into JavaScript

Erik the Outgolfer

7:04 PM

@maxathousand consider that most of us are active here while in job and less while at home :)

J. Sallé

↑ I'm 100% guilty of that.

maxathousand

@cairdcoinheringaahing True! That would be a good one to start with. Thanks

Erik the Outgolfer

note: Japt misses some important features, so don't get disappointed if you can't get it at first :)

flawr

7:21 PM

Can anyone unfreeze prolog? I didn't realize it freezes so quickly.

DJMcMayhem

@flawr holy crap that was fast

Erik the Outgolfer

DJ has an alter ego confirmed

flawr

too bad room owners cannot unfreeze their rooms :/

Erik the Outgolfer

not too bad, otherwise room owners would have been pushing for their room to appear in the normal list

caird coinheringaahing

> 15 hours later…

This room has been automatically frozen for inactivity

That has to be a bug

New Sandboxed Posts

7:28 PM

0

A: Sandbox for Proposed Challenges

Antigerrymandering code-golf map set-partitions From this question: The United States has a unique love of gerrymandering––the deliberate manipulation of an electoral district to predict certain voting results. Just recently there was a gerrymandering case brought before the Supreme Court. ...

flawr

@EriktheOutgolfer how does that work?

Erik the Outgolfer

constantly unfreezing their room

caird coinheringaahing

@flawr You could request on mother meta, but I'm sure an SE staff member would show up and tell us ~~they can't be bothered~~ why it isn't necessary :/

Erik the Outgolfer

or rather the question will be closed as a dupe way before that

totallyhuman

@cairdcoinheringaahing Maybe not, I think it also checks if there were messages after the unfreeze.

Erik the Outgolfer

7:33 PM

it shouldn't be assumed that anyone is around and not busy when the unfreeze happens

caird coinheringaahing

TFW Windows says that a 3 byte file is "1KB" ಠ_ಠ

J. Sallé

@cairdcoinheringaahing Windows being windows.

New Sandboxed Posts

8:02 PM

0

A: Sandbox for Proposed Challenges

Decompile popularity-contest compiler Pick a language and call it language A. Pick a compiler for that language that translates it to another language, language B. Write a program or function in language A that receives a program in language B and prints/returns a program in language A that pro...

caird coinheringaahing

9:35 PM

> subs/infinite output:
< <FAILED> Entered infinite loop

What a surprise :P

sergiol

Hello

1

A: Sandbox for Proposed Challenges

Is the program 32 or 64 bits? Challenge is simple to explain: write the shortest code you need to determine an executable program supplied as a parameter is 32 or 64 bits. If there is a different kind of bitness, you can also do for it, but is not mandatory. What I really don't want is telling...

does my challenge need more refinement?

Riker

9:59 PM

@Dennis why was the bounty here removed?

"draw attention to get more upvotes"?

49

Q: Is my OS 32-bit or 64-bit?

It's not too important anymore, but occasionally somebody needs to know. Here is a simple golf: Taking no user input, tell me if the computer on which the code is run is on a 64-bit operating system, or a 32-bit operating system! If the code is run on a 32-bit operating system, print "32", if t...

code-golf decision-problem

I'd mark that dupe, despite the OS vs executable difference

sergiol

@Riker, it is not the same thing

very different, indeed

DJMcMayhem

@Riker -35 :O

Holy crap

caird coinheringaahing

@DJMcMayhem Lowest non-deleted score on the site :/

Erik the Outgolfer

@Riker strangely enough, I don't think there was any bounty at all in there

H.PWiz

@Riker That was someone giving away all of there rep on the tree lowest voted questions

New Sandboxed Posts

10:10 PM

0

A: Sandbox for Proposed Challenges

Up goes the number! Given an integer N perform the following steps: (using 9 as an example). Receive input N. (9) Convert N from base10 to base2. (1001) Increase every bit by 1. (2112) Treat the result as base3 and convert it back to base10. (68) Return/Output the result. Input May be rec...

Riker

@H.PWiz ah, was it? ok

@EriktheOutgolfer no there was

tha'ts what it looks like if that happens

the bounty bit is removed from teh history iirc

Erik the Outgolfer

hm, sounds impractical to me

like, since the username is disclosed anyway, why not disclose the amount

Dennis

11:29 PM

@Pavel ppcg.starmaninnovations.com/tnbde/#ZaLUxudpbw

Anonymous

11:41 PM

@Dennis this is a bit more performant

Anonymous

filtering out 0-star users makes it even faster

Anonymous

Ordering by total stars is interesting. Alex is #1, and 4 of the 5 current mods are #2-6 (DJ is #11). All but 2 of the top 10 (Calvin and quartata) are TNB ROs. After typing all of that, I realize now that it's not that interesting and actually totally expected :P

Transcript for