-
Diverse Representation via Computational Participatory Elections -- Lessons from a Case Study
Authors:
Florian Evéquoz,
Johan Rochel,
Vijay Keswani,
L. Elisa Celis
Abstract:
Elections are the central institution of democratic processes, and often the elected body -- in either public or private governance -- is a committee of individuals. To ensure the legitimacy of elected bodies, the electoral processes should guarantee that diverse groups are represented, in particular members of groups that are marginalized due to gender, ethnicity, or other socially salient attrib…
▽ More
Elections are the central institution of democratic processes, and often the elected body -- in either public or private governance -- is a committee of individuals. To ensure the legitimacy of elected bodies, the electoral processes should guarantee that diverse groups are represented, in particular members of groups that are marginalized due to gender, ethnicity, or other socially salient attributes. To address this challenge of representation, we have designed a novel participatory electoral process coined the Representation Pact, implemented with the support of a computational system. That process explicitly enables voters to flexibly decide on representation criteria in a first round, and then lets them vote for candidates in a second round. After the two rounds, a counting method is applied, which selects the committee of candidates that maximizes the number of votes received in the second round, conditioned on satisfying the criteria provided in the first round. With the help of a detailed use case that applied this process in a primary election of 96 representatives in Switzerland, we explain how this method contributes to fairness in political elections by achieving a better "descriptive representation". Further, based on this use case, we identify lessons learnt that are applicable to participatory computational systems used in societal or political contexts. Good practices are identified and presented.
△ Less
Submitted 30 May, 2022;
originally announced May 2022.
-
Unfolding Semantics of the Untyped λ-Calculus with letrec
Authors:
Jan Rochel
Abstract:
We investigate the relationship between finite terms in λ-letrec, the λ-calculus with letrec, and the infinite λ-terms they express. We say that a lambda-letrec term expresses a lambda-term if the latter can be obtained as an infinite unfolding of the former. Unfolding is the process of substituting occurrences of function variables by the right-hand side of their definition.
We consider the fol…
▽ More
We investigate the relationship between finite terms in λ-letrec, the λ-calculus with letrec, and the infinite λ-terms they express. We say that a lambda-letrec term expresses a lambda-term if the latter can be obtained as an infinite unfolding of the former. Unfolding is the process of substituting occurrences of function variables by the right-hand side of their definition.
We consider the following questions: (i) How can we characterise those infinite λ-terms that are λ-letrec-expressible? (ii) Given two λ-letrec terms, how can we determine whether they have the same unfolding? (iii) Given a λ-letrec term, can we find a more compact version of the term with the same unfolding? To tackle these questions we introduce and study the following formalisms: (i) a rewriting system for unfolding λ-letrec terms into λ-terms (ii) a rewriting system for `observing' λ-terms by dissecting their term structure (iii) higher-order and first-order graph formalisms together with translations between them as well as translations from and to λ-letrec.
We identify a first-order term graph formalism on which bisimulation preserves and reflects the unfolding semantics of λ-letrec and which is closed under functional bisimulation. From this we derive efficient methods to determine whether two terms are equivalent under infinite unfolding and to compute the maximally shared form of a given λ-letrec term.
△ Less
Submitted 19 October, 2016;
originally announced October 2016.
-
Maximal Sharing in the Lambda Calculus with letrec
Authors:
Clemens Grabmayer,
Jan Rochel
Abstract:
Increasing sharing in programs is desirable to compactify the code, and to avoid duplication of reduction work at run-time, thereby speeding up execution. We show how a maximal degree of sharing can be obtained for programs expressed as terms in the lambda calculus with letrec. We introduce a notion of `maximal compactness' for lambda-letrec-terms among all terms with the same infinite unfolding.…
▽ More
Increasing sharing in programs is desirable to compactify the code, and to avoid duplication of reduction work at run-time, thereby speeding up execution. We show how a maximal degree of sharing can be obtained for programs expressed as terms in the lambda calculus with letrec. We introduce a notion of `maximal compactness' for lambda-letrec-terms among all terms with the same infinite unfolding. Instead of defined purely syntactically, this notion is based on a graph semantics. lambda-letrec-terms are interpreted as first-order term graphs so that unfolding equivalence between terms is preserved and reflected through bisimilarity of the term graph interpretations. Compactness of the term graphs can then be compared via functional bisimulation.
We describe practical and efficient methods for the following two problems: transforming a lambda-letrec-term into a maximally compact form; and deciding whether two lambda-letrec-terms are unfolding-equivalent. The transformation of a lambda-letrec-term $L$ into maximally compact form $L_0$ proceeds in three steps:
(i) translate L into its term graph $G = [[ L ]]$; (ii) compute the maximally shared form of $G$ as its bisimulation collapse $G_0$; (iii) read back a lambda-letrec-term $L_0$ from the term graph $G_0$ with the property $[[ L_0 ]] = G_0$. This guarantees that $L_0$ and $L$ have the same unfolding, and that $L_0$ exhibits maximal sharing.
The procedure for deciding whether two given lambda-letrec-terms $L_1$ and $L_2$ are unfolding-equivalent computes their term graph interpretations $[[ L_1 ]]$ and $[[ L_2 ]]$, and checks whether these term graphs are bisimilar.
For illustration, we also provide a readily usable implementation.
△ Less
Submitted 23 June, 2014; v1 submitted 7 January, 2014;
originally announced January 2014.
-
Term Graph Representations for Cyclic Lambda-Terms
Authors:
Clemens Grabmayer,
Jan Rochel
Abstract:
We study various representations for cyclic lambda-terms as higher-order or as first-order term graphs. We focus on the relation between `lambda-higher-order term graphs' (lambda-ho-term-graphs), which are first-order term graphs endowed with a well-behaved scope function, and their representations as `lambda-term-graphs', which are plain first-order term graphs with scope-delimiter vertices that…
▽ More
We study various representations for cyclic lambda-terms as higher-order or as first-order term graphs. We focus on the relation between `lambda-higher-order term graphs' (lambda-ho-term-graphs), which are first-order term graphs endowed with a well-behaved scope function, and their representations as `lambda-term-graphs', which are plain first-order term graphs with scope-delimiter vertices that meet certain scoping requirements. Specifically we tackle the question: Which class of first-order term graphs admits a faithful embedding of lambda-ho-term-graphs in the sense that: (i) the homomorphism-based sharing-order on lambda-ho-term-graphs is preserved and reflected, and (ii) the image of the embedding corresponds closely to a natural class (of lambda-term-graphs) that is closed under homomorphism?
We systematically examine whether a number of classes of lambda-term-graphs have this property, and we find a particular class of lambda-term-graphs that satisfies this criterion. Term graphs of this class are built from application, abstraction, variable, and scope-delimiter vertices, and have the characteristic feature that the latter two kinds of vertices have back-links to the corresponding abstraction.
This result puts a handle on the concept of subterm sharing for higher-order term graphs, both theoretically and algorithmically: We obtain an easily implementable method for obtaining the maximally shared form of lambda-ho-term-graphs. Also, we open up the possibility to pull back properties from first-order term graphs to lambda-ho-term-graphs. In fact we prove this for the property of the sharing-order successors of a given term graph to be a complete lattice with respect to the sharing order.
This report extends the paper with the same title (https://arxiv.boxedpaper.com/abs/1302.6338v1) in the proceedings of the workshop TERMGRAPH 2013.
△ Less
Submitted 2 November, 2013; v1 submitted 2 August, 2013;
originally announced August 2013.
-
Expressibility in the Lambda Calculus with mu
Authors:
Clemens Grabmayer,
Jan Rochel
Abstract:
We address a problem connected to the unfolding semantics of functional programming languages: give a useful characterization of those infinite lambda-terms that are lambda_{letrec}-expressible in the sense that they arise as infinite unfoldings of terms in lambda_{letrec}, the lambda-calculus with letrec. We provide two characterizations, using concepts we introduce for infinite lambda-terms: reg…
▽ More
We address a problem connected to the unfolding semantics of functional programming languages: give a useful characterization of those infinite lambda-terms that are lambda_{letrec}-expressible in the sense that they arise as infinite unfoldings of terms in lambda_{letrec}, the lambda-calculus with letrec. We provide two characterizations, using concepts we introduce for infinite lambda-terms: regularity, strong regularity, and binding-capturing chains. It turns out that lambda_{letrec}-expressible infinite lambda-terms form a proper subclass of the regular infinite lambda-terms. In this paper we establish these characterizations only for expressibility in lambda_{mu}, the lambda-calculus with explicit mu-recursion. We show that for all infinite lambda-terms T the following are equivalent: (i): T is lambda_{mu}-expressible; (ii): T is strongly regular; (iii): T is regular, and it only has finite binding-capturing chains.
We define regularity and strong regularity for infinite lambda-terms as two different generalizations of regularity for infinite first-order terms: as the existence of only finitely many subterms that are defined as the reducts of two rewrite relations for decomposing lambda-terms. These rewrite relations act on infinite lambda-terms furnished with a marked prefix of abstractions for collecting decomposed lambda-abstractions and keeping the terms closed under decomposition. They differ in how vacuous abstractions in the prefix are removed.
This report accompanies the article with the same title for the proceedings of the conference RTA 2013, and mainly differs from that by providing the proof of the characterization of lambda_{mu}-expressibility with binding-capturing chains.
△ Less
Submitted 27 May, 2013; v1 submitted 23 April, 2013;
originally announced April 2013.
-
Term Graph Representations for Cyclic Lambda-Terms
Authors:
Clemens Grabmayer,
Jan Rochel
Abstract:
We study various representations for cyclic lambda-terms as higher-order or as first-order term graphs. We focus on the relation between 'lambda-higher-order term graphs' (lambda-ho-term-graphs), which are first-order term graphs endowed with a well-behaved scope function, and their representations as 'lambda-term-graphs', which are plain first-order term graphs with scope-delimiter vertices that…
▽ More
We study various representations for cyclic lambda-terms as higher-order or as first-order term graphs. We focus on the relation between 'lambda-higher-order term graphs' (lambda-ho-term-graphs), which are first-order term graphs endowed with a well-behaved scope function, and their representations as 'lambda-term-graphs', which are plain first-order term graphs with scope-delimiter vertices that meet certain scoping requirements. Specifically we tackle the question: Which class of first-order term graphs admits a faithful embedding of lambda-ho-term-graphs in the sense that (i) the homomorphism-based sharing-order on lambda-ho-term-graphs is preserved and reflected, and (ii) the image of the embedding corresponds closely to a natural class (of lambda-term-graphs) that is closed under homomorphism?
We systematically examine whether a number of classes of lambda-term-graphs have this property, and we find a particular class of lambda-term-graphs that satisfies this criterion. Term graphs of this class are built from application, abstraction, variable, and scope-delimiter vertices, and have the characteristic feature that the latter two kinds of vertices have back-links to the corresponding abstraction.
This result puts a handle on the concept of subterm sharing for higher-order term graphs, both theoretically and algorithmically: We obtain an easily implementable method for obtaining the maximally shared form of lambda-ho-term-graphs. Furthermore, we open up the possibility to pull back properties from first-order term graphs to lambda-ho-term-graphs, properties such as the complete lattice structure of bisimulation equivalence classes with respect to the sharing order.
△ Less
Submitted 26 February, 2013;
originally announced February 2013.
-
Expressibility in the Lambda Calculus with Letrec
Authors:
Clemens Grabmayer,
Jan Rochel
Abstract:
We investigate the relationship between finite terms in lambda-letrec, the lambda calculus with letrec, and the infinite lambda terms they express. As there are easy examples of lambda-terms that, intuitively, are not unfoldings of terms in lambda-letrec, we consider the question: How can those infinite lambda terms be characterised that are lamda-letrec-expressible in the sense that they can be o…
▽ More
We investigate the relationship between finite terms in lambda-letrec, the lambda calculus with letrec, and the infinite lambda terms they express. As there are easy examples of lambda-terms that, intuitively, are not unfoldings of terms in lambda-letrec, we consider the question: How can those infinite lambda terms be characterised that are lamda-letrec-expressible in the sense that they can be obtained as infinite unfoldings of terms in lambda-letrec?
For 'observing' infinite lambda-terms through repeated 'experiments' carried out at the head of the term we introduce two rewrite systems (with rewrite relations) -reg-> and -reg+-> that decompose the term, and produce 'generated subterms' in two notions. Thereby the sort of the step can be observed as well as its target, a generated subterm. In both systems there are four sorts of decomposition steps: -lambda-> steps (decomposing a lambda-abstraction), -@0> and -@1> steps (decomposing an application into its function and argument), and respectively, -del-> steps (delimiting the scope of an abstraction, for -reg->), and -S-> (delimiting of scopes, for -reg+->). These steps take place on infinite lambda-terms furnished with a leading prefix of abstractions for gathering previously encountered lambda-abstractions and keeping the generated subterms closed. We call an infinite lambda-term 'regular'/'strongly regular' if its set of -reg-> -reachable / -reg-> -reachable generated subterms is finite. Furthermore, we analyse the binding structure of lambda-terms with the concept of 'binding-capturing chain'.
Using these concepts, we answer the question above by providing two characterisations of lambda-letrec-expressibility. For all infinite lambda-terms M, the following statements are equivalent: (i) M is lambda-letrec-expressible; (ii) M is strongly regular; (iii) M is regular, and it only has finite binding-capturing chains.
△ Less
Submitted 2 May, 2013; v1 submitted 11 August, 2012;
originally announced August 2012.
-
Repetitive Reduction Patterns in Lambda Calculus with letrec (Work in Progress)
Authors:
Jan Rochel,
Clemens Grabmayer
Abstract:
For the lambda-calculus with letrec we develop an optimisation, which is based on the contraction of a certain class of 'future' (also: virtual) redexes.
In the implementation of functional programming languages it is common practice to perform beta-reductions at compile time whenever possible in order to produce code that requires fewer reductions at run time. This is, however, in principle lim…
▽ More
For the lambda-calculus with letrec we develop an optimisation, which is based on the contraction of a certain class of 'future' (also: virtual) redexes.
In the implementation of functional programming languages it is common practice to perform beta-reductions at compile time whenever possible in order to produce code that requires fewer reductions at run time. This is, however, in principle limited to redexes and created redexes that are 'visible' (in the sense that they can be contracted without the need for unsharing), and cannot generally be extended to redexes that are concealed by sharing constructs such as letrec. In the case of recursion, concealed redexes become visible only after unwindings during evaluation, and then have to be contracted time and again.
We observe that in some cases such redexes exhibit a certain form of repetitive behaviour at run time. We describe an analysis for identifying binders that give rise to such repetitive reduction patterns, and eliminate them by a sort of predictive contraction. Thereby these binders are lifted out of recursive positions or eliminated altogether, as a result alleviating the amount of beta-reductions required for each recursive iteration.
Both our analysis and simplification are suitable to be integrated into existing compilers for functional programming languages as an additional optimisation phase. With this work we hope to contribute to increasing the efficiency of executing programs written in such languages.
△ Less
Submitted 13 February, 2011;
originally announced February 2011.
