#cs

4 posts3 participants0 posts today

Jencel PanicI have long suspected that any language with if's and loops would be Turing complete, turns out there was a proof for that all along...<a href="https://en.wikipedia.org/wiki/Structured_program_theorem" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://en.wikipedia.org/wiki/Structured_program_theorem</a><a href="https://mathstodon.xyz/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://mathstodon.xyz/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

ParisOlga Carmona de plus en plus proche des Féminines du PSG –Afin de concurrencer l’Olympique Lyonnais, les Féminines du PSG souhaitent se renforcer. Elles ser… <a href="https://pubeurope.com/tags/Paris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Paris</a> <a href="https://pubeurope.com/tags/FR" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FR</a> <a href="https://pubeurope.com/tags/France" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#France</a> <a href="https://pubeurope.com/tags/Actu" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Actu</a> <a href="https://pubeurope.com/tags/News" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#News</a> <a href="https://pubeurope.com/tags/Europe" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Europe</a> <a href="https://pubeurope.com/tags/EU" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#EU</a> <a href="https://pubeurope.com/tags/actu" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#actu</a> <a href="https://pubeurope.com/tags/ActuParis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ActuParis</a> <a href="https://pubeurope.com/tags/Actualit%C3%A9s" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Actualités</a> <a href="https://pubeurope.com/tags/Actualit%C3%A9sParis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ActualitésParis</a> <a href="https://pubeurope.com/tags/canalsupporters" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#canalsupporters</a> <a href="https://pubeurope.com/tags/Carmona" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Carmona</a> <a href="https://pubeurope.com/tags/CS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CS</a> <a href="https://pubeurope.com/tags/europe" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#europe</a> <a href="https://pubeurope.com/tags/feminines" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#feminines</a> <a href="https://pubeurope.com/tags/F%C3%A9mininesduPSG" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FémininesduPSG</a> <a href="https://pubeurope.com/tags/f%C3%A9mininespsg" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#fémininespsg</a> <a href="https://pubeurope.com/tags/mercato" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#mercato</a> <a href="https://pubeurope.com/tags/mercatopsg" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#mercatopsg</a> <a href="https://pubeurope.com/tags/NewsParis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#NewsParis</a> <a href="https://pubeurope.com/tags/OlgaCarmona" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#OlgaCarmona</a> <a href="https://pubeurope.com/tags/ParisNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ParisNews</a> <a href="https://pubeurope.com/tags/parissaint" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#parissaint</a>-germain <a href="https://pubeurope.com/tags/parissg" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#parissg</a> <a href="https://pubeurope.com/tags/psg" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#psg</a> <a href="https://pubeurope.com/tags/psgfeminin" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#psgfeminin</a> <a href="https://pubeurope.com/tags/realmadrid" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#realmadrid</a> <a href="https://pubeurope.com/tags/R%C3%A9publiquefran%C3%A7aise" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Républiquefrançaise</a> <a href="https://www.europesays.com/fr/183302/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.europesays.com/fr/183302/</a>

TariqWhy is there no consideration of base cases ?This is the textbook's explanation of "structural induction". The subsequent worked examples don't refer to base cases either.Is it because they are always trivially true? I doubt this, myself.<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

Tariqcurrently learning about "structural induction"my understanding (not 100% sure) * We want to prove a property P for a λ-term E.* E is constructed using a set of construction rules.* So it must have been constructed from a term D by applying a construction rule.* Induction hypothesis (IH) is that P is true for D.* If we can prove that P applies to E by virtue of the IH and a property of the construction rules.... we've proven P is true generally.Is that right?<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqI've been writing up my attempts at the exercises from "Type Theory & Formal Proof".I've done chapter 1, and have almost done chapter 2.I'm sure I've made many errors, but overall it helps me learn the ideas better than just reading, or doing the exercises as if no-one would read the solutions.<a href="https://type-theory-and-formal-proof.blogspot.com/p/contents.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://type-theory-and-formal-proof.blogspot.com/p/contents.html</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqIs dimensional analysis the type theory of physics?<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a> <a href="https://mastodon.social/tags/physics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#physics</a>

TariqIs this correct?Q. Construct a (simply typed) λ-term of type((α →β) →α) →(α →α →β) →αA. My answerλx:((α →β) →α) . λy: (α →α →β) . x(y(z:α)) My reasoning:* the term takes 2 arguments and we don't have a choice of their type* but I can't reach the output type with just those two arguments so I need a 3rd variable which I include as a "pre-typed variable" .. z:αI just feel uncertain about crowbarring a pre-typed z into the expression<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqNeed some advice.The textbook only has example of proofs with the "flags" all at the top of flag notation proofs.But I think for this proof, the flag for `z` needs to be further down.My reasoning .... because if `x` and `y` are instantiated inside the `z` scope, they can't be used outside it.Am I right? Does scope not really matter in flag notation proofs ?Attached image shows both versions for comparison.<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqTo create proof trees like this in LaTexI first tried the popular bussproof but then moved to ebproof as it was slightly nicer for labelling inference steps.I actually tried another one too. Overall they all seemed pretty simple to use which is good - I don't often say that about software!<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a> <a href="https://mastodon.social/tags/latex" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#latex</a> <a href="https://mastodon.social/tags/logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#logic</a>

Charlie McHenryOne of the great heroes in not just Apple history, but computer history, Bill Atkinson, has died at 74 from pancreatic cancer. <a href="https://connectop.us/tags/obit" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#obit</a> <a href="https://connectop.us/tags/RIP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RIP</a> <a href="https://connectop.us/tags/ComputerScience" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ComputerScience</a> <a href="https://connectop.us/tags/CS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CS</a> <a href="https://connectop.us/tags/IT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IT</a> <a href="https://connectop.us/tags/Technology" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Technology</a> <a href="https://connectop.us/tags/ComputerHistory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ComputerHistory</a> <a href="https://connectop.us/tags/Apple" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Apple</a> <a href="https://daringfireball.net/linked/2025/06/07/bill-atkinson-rip" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://daringfireball.net/linked/2025/06/07/bill-atkinson-rip</a>

TariqNeed some help.-----I know that to prove P ⇒ Q, I assume P and derive Q.----Now to prove(A⇒B) ⇒ ((B⇒C) ⇒ (A⇒C))I need to assume (A⇒B) and derive ((B⇒C) ⇒ (A⇒C)).But I can't seem to make progress from (A⇒B) alone, I think I need to assume A is true as well.----Intuitively the statement makes total sense. But drawing the derivation as per image attached using elim and intro rules, I get stuck unless I assume A too.Can anyone help clarify my thinking?<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a> <a href="https://mastodon.social/tags/logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#logic</a>

TariqMy second ever derivation in "flag format"I'm using the flagderiv latex package which is actually very simple to use. It is already installed in Overleaf if you use that.<a href="https://www.ctan.org/pkg/flagderiv" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.ctan.org/pkg/flagderiv</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a> <a href="https://mastodon.social/tags/latex" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#latex</a>

Tariqmy first ever derivation in "flag format" !!<a href="https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-6.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-6.html</a>update - there's a typo on the last line, I'll fix it tomorrow<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqLaTex for LogiciansIt seems to be a collection of how-tos for recreating diagrams / notation used in logic.I may use it for "flag derivation diagrams".<a href="https://www.logicmatters.net/latex-for-logicians/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.logicmatters.net/latex-for-logicians/</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a> <a href="https://mastodon.social/tags/logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#logic</a> <a href="https://mastodon.social/tags/texlatex" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#texlatex</a>

TariqI've posted an exercise I'm not making progress on stack exchange(I think) the core of it is how to handle "free variables" when deriving a type using the 3 rules - (var) (appl) (abst)<a href="https://cs.stackexchange.com/questions/173051/using-premise-conclusion-derivation-rules-with-free-variables-in-simply-typed-λ" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://cs.stackexchange.com/questions/173051/using-premise-conclusion-derivation-rules-with-free-variables-in-simply-typed-λ</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqI'd welcome advice on how to handle "free variables" when working out if a λ-term is legal using the "premise / conclusion" process I'm not sure how to handle the type for the "free variable" y in this exerciseworking out so far <a href="https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-6.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-6.html</a>image attached to illustrate which variable I should have ended up with the empty context justifies...∅ ⊢ ....<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

Tariq<a href="https://mathstodon.xyz/@abuseofnotation" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@abuseofnotation</a> So I typed λxy . x (λz.y) yas((C→B) →B →E) →B→C→Ebut the book says((C→B) →B →E) →B→EI can't pin down the reason one is correct over the other - I can see reasons for both.<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqDo λ-terms of the following form λxy . x (λz.y) yhave a type with 4 parts A → B → C → Dor 3 partsA → B → D----I would have thought 4 parts because there are 3 inputs (x, y, z) and one outputBut a book I'm reading suggests 2 inputs (x, y) and one output---EDIT - my working out<a href="https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-5.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-5.html</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

Tariqhere's my solution to the exercise .. assuming my interpretation of "pre-typed" λ-terms is correct<a href="https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-4.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://type-theory-and-formal-proof.blogspot.com/2025/06/chapter-2-exercise-4.html</a><a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

TariqWhat is a "pre-typed" λ-term?The textbook is unclear.Internet searching doesn't show much which suggests "pre-typed" might be specific to this textbook.<a href="https://mastodon.social/tags/maths" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#maths</a> <a href="https://mastodon.social/tags/cs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cs</a>

Recent searches

Search options

Administered by:

Server stats: