Frühere Suchanfragen

Keine früheren Suchanfragen

Suchoptionen

Nur verfügbar, wenn angemeldet.
mastodontech.de ist einer von vielen unabhängigen Mastodon-Servern, mit dem du dich im Fediverse beteiligen kannst.
Offen für alle (über 16) und bereitgestellt von Markus'Blog

Verwaltet von:

Serverstatistik:

1,5 Tsd.
aktive Profile

mastodontech.de: ÜberStatusProfilverzeichnisDatenschutzerklärung

Mastodon: ÜberApp herunterladenTastenkombinationenQuellcode anzeigenv4.4.1

#cs

7 Beiträge6 Beteiligte0 Beiträge heute
Antwortete im Thread
*
Tariq

@jonmsterling

Thanks

---

I previously struggled to find a T such that

Πα:*.α : T

which appears to ask for a 'type of a type'

with some help, I used the formation rule to say T must be *

---

The reason I'm struggling a little with this kind of expression again is I have a more challenging (to me) exercise where I have to find an inhabitant for α and β given the context

α : ∗
β : ∗
x : α →Πα:*.α
f : (α →α) →α

looking at x is why I'm thinking " what is the type of Πα:*.α ?"

#maths#cs
*
Tariq

I wish there were a way to embed these into blogger as mathjax.

I do use mathjax with blogger, but these "flag format" proofs need the "flagderiv" latex package which isn't part of mathjax.

So I have to latex → PDF → PNG and upload to the blog.

yuk !

#latextex#maths#cs
*
Tariq

I'd welcome advice on lambda calculus.

---

Given context:

Γ ≡ β : ∗, x : Πα : ∗. α

I need to find 3 examples of terms that inhabit β→β

... that aren't β-convertible to each other, and are in β-normal form.

---

my example 1:

λz:β .z

my example 2:

λβ .xβ

for a 3rd example.. I'm playing with ideas like

x(β→β)

since (β→β) is of type * using the formation rule, but not sure..

---

#maths#cs
Laura Sophia

My old introduction was very outdated, so it's time to reintroduce myself:
#introduction

Hi 👋, I’m Laura.

I am a transfeminine person, somewhat in the middle of my transition. 🏳️‍⚧️ #trans #transbubble

A major part of my time I spend as a Postdoc in computer science, working on embedded AI and low-power IoT communication. #cs #TinyML #IoT #academia #science

Outside of work, I am active in the local #queer center (board member, GER: Vorstand), I enjoy playing board games, and I listen to too many #podcasts.

Tariq

advice needed !

I need to find an inhabitant of β given the context

Γ ≡ β : ∗, x : Πα : ∗. α

My brain is telling me that I am free to choose pretty much any type to inhabit β because the context doesn't impose any restriction.

I could have "int" or "bool" or "int → bool", etc and they would all be ok.

Am I right? I'm suffering beginner lack of confidence.

#maths#cs
Paul Houle

⛓️‍💥 Broken Tokens? Your Language Model can Secretly Handle Non-Canonical Tokenizations

arxiv.org/abs/2506.19004

arXiv logo
arXiv.orgBroken Tokens? Your Language Model can Secretly Handle Non-Canonical TokenizationsModern tokenizers employ deterministic algorithms to map text into a single "canonical" token sequence, yet the same string can be encoded as many non-canonical tokenizations using the tokenizer vocabulary. In this work, we investigate the robustness of LMs to text encoded with non-canonical tokenizations entirely unseen during training. Surprisingly, when evaluated across 20 benchmarks, we find that instruction-tuned models retain up to 93.4% of their original performance when given a randomly sampled tokenization, and 90.8% with character-level tokenization. We see that overall stronger models tend to be more robust, and robustness diminishes as the tokenization departs farther from the canonical form. Motivated by these results, we then identify settings where non-canonical tokenization schemes can *improve* performance, finding that character-level segmentation improves string manipulation and code understanding tasks by up to +14%, and right-aligned digit grouping enhances large-number arithmetic by +33%. Finally, we investigate the source of this robustness, finding that it arises in the instruction-tuning phase. We show that while both base and post-trained models grasp the semantics of non-canonical tokenizations (perceiving them as containing misspellings), base models try to mimic the imagined mistakes and degenerate into nonsensical output, while post-trained models are committed to fluent responses. Overall, our findings suggest that models are less tied to their tokenizer than previously believed, and demonstrate the promise of intervening on tokenization at inference time to boost performance.
#ai#llm#cs
Tariq

Help needed !

Show there is a t such that ⊥: t where

⊥ ≡ Πα:*.α

I've only ever seen the type binder Π used in λ2 types of terms, not terms themselves.

It would be like saying ... show there is a t such that (α → α):t

What am I missing?

#maths#cs
*
:flag_enby_wartime: 𝕛𝕦𝕝𝕖𝕤 :antifa:

I wonder whether "fusion trees with multiple roots" exist

what I know after a quick search

  • there is a bonsai technique concerning roots of fusion trees
  • there is a minecraft modpack called fusion forest
  • there is a company called b-forest
  • there is a famous counter strike player named forest
  • there is a subfield named forest informatics
  • there is a greek thing named b dag
#tcs#theoreticalComputerScience#cs
amen zwa, esq.

Common types of #programming books:

• THEORETICAL—#CS pure theory books on "programming as a mathematical activity": "The Lambda Calculus, Its Syntax and Semantics" (barendregt), "Category Theory for Programmers" (Milewski), etc.

• PRACTICAL—#IT pure coding books on "programming as a vocational activity": "The C Programming Language" (Kernighan), typical API call-fest pulps, etc.

• BALANCED—introductory programming books with ample theoretical background, for CS undergraduates: "Introduction to Functional Programming" (Bird), "The Implementation of Functional Programming Languages" (Jones), etc.

Rxiv mechanobio

📰 "Multicontinuum Homogenization for Poroelasticity Model"
arxiv.org/abs/2506.20890 #Physics.Comp-Ph #Mechanics #Math.Na #Cs.Na #Cs.Ce #Cell

arXiv logo
arXiv.orgMulticontinuum Homogenization for Poroelasticity ModelIn this paper, we derive multicontinuum poroelasticity models using the multicontinuum homogenization method. Poroelasticity models are widely used in many areas of science and engineering to describe coupled flow and mechanics processes in porous media. However, in many applications, the properties of poroelastic media possess high contrast, presenting serious computational challenges. It is well known that standard homogenization approaches often fail to give an accurate solution due to the lack of macroscopic parameters. Multicontinuum approaches allow us to consider such cases by defining several average states known as continua. In the field of poroelasticity, multiple-network models arising from the multiple porous media theory are representatives of these approaches. In this work, we extend previous findings by deriving the generalized multicontinuum poroelasticity model. We apply the recently developed multicontinuum homogenization method and provide a rigorous derivation of multicontinuum equations. For this purpose, we formulate coupled constraint cell problems in oversampled regions to consider different homogenized effects. Then, we obtain a multicontinuum expansion of the fine-scale fields and derive the multicontinuum model supposing the smoothness of macroscopic variables. We present the most general version of equations and the simplified ones based on our numerical experiments. Numerical results are presented for different heterogeneous media cases and demonstrate the high accuracy of our proposed multicontinuum models.
Tariq

Did I get this right?

Given these four declarations:

α : ∗
β : ∗
f : α →β
x : α

The following are the only valid λ2-contexts:

α : *
α : *, x : α
β : *
α: *, β : *
α: *, β : *, f: α→β

(here λ2 is second order lambda calculus, and α, β are type variables, not object variables)

#maths#cs
Rxiv mechanobio

📰 "Contactless Precision Steering of Particles in a Fluid inside a Cube with Rotating Walls"
arxiv.org/abs/2506.15958 #Physics.Flu-Dyn #Dynamics #Cs.Ro #Cs.Lg #Cell

arXiv logo
arXiv.orgContactless Precision Steering of Particles in a Fluid inside a Cube with Rotating WallsContactless manipulation of small objects is essential for biomedical and chemical applications, such as cell analysis, assisted fertilisation, and precision chemistry. Established methods, including optical, acoustic, and magnetic tweezers, are now complemented by flow control techniques that use flow-induced motion to enable precise and versatile manipulation. However, trapping multiple particles in fluid remains a challenge. This study introduces a novel control algorithm capable of steering multiple particles in flow. The system uses rotating disks to generate flow fields that transport particles to precise locations. Disk rotations are governed by a feedback control policy based on the Optimising a Discrete Loss (ODIL) framework, which combines fluid dynamics equations with path objectives into a single loss function. Our experiments, conducted in both simulations and with the physical device, demonstrate the capability of the approach to transport two beads simultaneously to predefined locations, advancing robust contactless particle manipulation for biomedical applications.
AngesagtLive-Feeds
Über