-
Meat-Free Day Reduces Greenhouse Gas Emissions but Poses Challenges for Customer Retention and Adherence to Dietary Guidelines
Authors:
Giuseppe Russo,
Kristina Gligorić,
Vincent Moreau,
Robert West
Abstract:
Reducing meat consumption is crucial for achieving global environmental and nutritional targets. Meat-Free Day (MFD) is a widely adopted strategy to address this challenge by encouraging plant-based diets through the removal of animal-based meals. We assessed the environmental, behavioral, and nutritional impacts of MFD by implementing 67 MFDs over 18 months (once a week on a randomly chosen day)…
▽ More
Reducing meat consumption is crucial for achieving global environmental and nutritional targets. Meat-Free Day (MFD) is a widely adopted strategy to address this challenge by encouraging plant-based diets through the removal of animal-based meals. We assessed the environmental, behavioral, and nutritional impacts of MFD by implementing 67 MFDs over 18 months (once a week on a randomly chosen day) across 12 cafeterias on a large university campus, analyzing over 400,000 food purchases. MFD reduced on-campus food-related greenhouse gas (GHG) emissions on treated days by 52.9% and contributed to improved fiber (+26.9%) and cholesterol (-4.5%) consumption without altering caloric intake. These nutritional benefits were, however, accompanied by a 27.6% decrease in protein intake and a 34.2% increase in sugar consumption. Moreover, the increase in plant-based meals did not carry over to subsequent days, as evidenced by a 3.5% rebound in animal-based meal consumption on days immediately following treated days. MFD also led to a 16.8% drop in on-campus meal sales on treated days.Monte Carlo simulations suggest that if 8.7% of diners were to eat burgers off-campus on treated days, MFD's GHG savings would be fully negated. As our analysis identifies on-campus customer retention as the main challenge to MFD effectiveness, we recommend combining MFD with customer retention interventions to ensure environmental and nutritional benefits.
△ Less
Submitted 2 April, 2025;
originally announced April 2025.
-
Profinite trees, through monads and the lambda-calculus
Authors:
Vincent Moreau
Abstract:
In its simplest form, the theory of regular languages is the study of sets of finite words recognized by finite monoids. The finiteness condition on monoids gives rise to a topological space whose points, called profinite words, encode the limiting behavior of words with respect to finite monoids. Yet, some aspects of the theory of regular languages are not particular to monoids and can be describ…
▽ More
In its simplest form, the theory of regular languages is the study of sets of finite words recognized by finite monoids. The finiteness condition on monoids gives rise to a topological space whose points, called profinite words, encode the limiting behavior of words with respect to finite monoids. Yet, some aspects of the theory of regular languages are not particular to monoids and can be described in a general setting. On the one hand, Bojańczyk has shown how to use monads to generalize the theory of regular languages and has given an abstract definition of the free profinite structure, defined by codensity, given a fixed monad and a notion of finite structure. On the other hand, Salvati has introduced the notion of language of $λ$-terms, using denotational semantics, which generalizes the case of words and trees through the Church encoding. In recent work, the author and collaborators defined the notion of profinite $λ$-term using semantics in finite sets and functions, which extend the Church encoding to profinite words.
In this article, we prove that these two generalizations, based on monads and denotational semantics, coincide in the case of trees. To do so, we consider the monad of abstract clones which, when applied to a ranked alphabet, gives the associated clone of ranked trees. This induces a notion of free profinite clone, and hence of profinite trees. The main contribution is a categorical proof that the free profinite clone on a ranked alphabet is isomorphic, as a Stone-enriched clone, to the clone of profinite $λ$-terms of Church type. Moreover, we also prove a parametricity theorem on families of semantic elements which provides another equivalent formulation of profinite trees in terms of Reynolds parametricity.
△ Less
Submitted 20 February, 2024;
originally announced February 2024.
-
Syntactically and semantically regular languages of lambda-terms coincide through logical relations
Authors:
Vincent Moreau,
Lê Thành Dũng Nguyên
Abstract:
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed $λ$-terms, defined using denotational semantics in finite sets.
We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal…
▽ More
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed $λ$-terms, defined using denotational semantics in finite sets.
We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic $λ$-definability. Second, we show that any finitary extensional model of the simply typed $λ$-calculus, when used in Salvati's definition, recognizes exactly the same class of languages of $λ$-terms as the category of finite sets does.
The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.
△ Less
Submitted 8 February, 2024; v1 submitted 31 July, 2023;
originally announced August 2023.
-
Profinite lambda-terms and parametricity
Authors:
Sam van Gool,
Paul-André Melliès,
Vincent Moreau
Abstract:
Combining ideas coming from Stone duality and Reynolds parametricity, we formulate in a clean and principled way a notion of profinite lambda-term which, we show, generalizes at every type the traditional notion of profinite word coming from automata theory. We start by defining the Stone space of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo…
▽ More
Combining ideas coming from Stone duality and Reynolds parametricity, we formulate in a clean and principled way a notion of profinite lambda-term which, we show, generalizes at every type the traditional notion of profinite word coming from automata theory. We start by defining the Stone space of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo a notion of equivalence based on the finite standard model. One main contribution of the paper is to establish that, somewhat surprisingly, the resulting notion of profinite lambda-term coming from Stone duality lives in perfect harmony with the principles of Reynolds parametricity. In addition, we show that the notion of profinite lambda-term is compositional by constructing a cartesian closed category of profinite lambda-terms, and we establish that the embedding from lambda-terms modulo beta-eta-conversion to profinite lambda-terms is faithful using Statman's finite completeness theorem. Finally, we prove that the traditional Church encoding of finite words into lambda-terms can be extended to profinite words, and leads to a homeomorphism between the space of profinite words and the space of profinite lambda-terms of the corresponding Church type.
△ Less
Submitted 18 November, 2023; v1 submitted 29 January, 2023;
originally announced January 2023.
