004 Datenverarbeitung; Informatik
Refine
Year of publication
Document Type
- Working Paper (122) (remove)
Has Fulltext
- yes (122)
Is part of the Bibliography
- no (122)
Keywords
- Lambda-Kalkül (18)
- Formale Semantik (10)
- Operationale Semantik (8)
- Programmiersprache (7)
- lambda calculus (7)
- Nebenläufigkeit (6)
- functional programming (6)
- concurrency (5)
- pi-calculus (5)
- semantics (5)
- Logik (4)
- Verifikation (4)
- adequate translations (4)
- contextual equivalence (4)
- Funktionale Programmierung (3)
- automated deduction (3)
- context lemma (3)
- functional programming languages (3)
- letrec (3)
- observational semantics (3)
- rewriting (3)
- Funktionale Programmiersprache (2)
- Kontextuelle Gleichheit (2)
- Logics (2)
- Programmtransformation (2)
- Pufferspeicher (2)
- Semantics (2)
- Verification (2)
- call-by-name (2)
- call-by-need (2)
- context unification (2)
- infinitary lambda calculus (2)
- lambda-calculus (2)
- lazy evaluation (2)
- logics in artificial intelligence (2)
- non-determinism (2)
- nondeterminism (2)
- program transformation (2)
- programming languages (2)
- second order unification (2)
- unification (2)
- verification (2)
- Abstrakte Reduktion (1)
- Abstrakter Automat (1)
- Algorithmus (1)
- Alice ML (1)
- Alpha equivalence (1)
- Baumgrammatiken (1)
- Beschreibungskomplexität (1)
- Big data (1)
- Bildverarbeitung (1)
- Call-by-Need (1)
- Causal Machine Learning (1)
- Clean (1)
- Computerlinguistik (1)
- Contextual Equivalence (1)
- Customer data sharing (1)
- Data access (1)
- Data portability (1)
- Digital footprints (1)
- Enriched Digital Footprint (1)
- FinTech (1)
- Flash Memories (1)
- Futures (1)
- Green Nudging (1)
- Haskell (1)
- Hauptkomponentenanalyse (1)
- Independent Component Analysis ICA (1)
- Iteratives Array (1)
- Kontextuelle Gleicheit (1)
- Lambda Calculus (1)
- Letrec-Kalkül (1)
- ML <Programmiersprache> (1)
- Marketplace lending (1)
- Nichtdeterminismus (1)
- Online Algorithms (1)
- Open banking (1)
- Operational Semantics (1)
- P2P lending (1)
- Paging Algorithms (1)
- Polynomielles Wortproblem (1)
- Principal Component Analysis PCA (1)
- Principal Independent Component Analysis PICA (1)
- Product returns (1)
- Programmiersprachen (1)
- Programmkalküle (1)
- Programmkorrektheit (1)
- Rate Distortion Theory (1)
- Reduktionssystem (1)
- Roboter (1)
- Rènyi mutual information (1)
- Seitenersetzungsstrategie (1)
- Selbstorganisierende Karte (1)
- Semantik (1)
- Sharing (1)
- Software (1)
- Speicherbedarf (1)
- Striktheitsanalyse (1)
- Takens-Grassberger correlation integral (1)
- Terrmersetzungssystem (1)
- Transkription (1)
- Umbenennung (1)
- Unabhängige Komponentenanalyse (1)
- Wortproblem (1)
- Zellularer Automat (1)
- abstract reduction (1)
- adequate translation (1)
- alpha renaming (1)
- attention-based object recognition (1)
- call-by-need lambda calculus (1)
- cellular automata (1)
- classification (1)
- clustering (1)
- correctness (1)
- decidability questions (1)
- deduction (1)
- feature selection (1)
- formal languages (1)
- formal semantics (1)
- grammar-based compression (1)
- image databases (1)
- iterative arrays (1)
- matching (1)
- meta languages (1)
- nominal unification (1)
- observational equivalence (1)
- polynomial word problem (1)
- precongruence (1)
- process approximation (1)
- program correctness (1)
- programming calculi (1)
- randomized algorithms (1)
- scale-invariant object model (1)
- sharing (1)
- similarity (1)
- simulation (1)
- space bounded computations (1)
- straight line programs (1)
- strictness analysis (1)
- theory of computation (1)
- translation (1)
- tree grammars (1)
- verzögerte Auswertung (1)
Institute
We consider unification of terms under the equational theory of two-sided distributivity D with the axioms x*(y+z) = x*y + x*z and (x+y)*z = x*z + y*z. The main result of this paper is that Dunification is decidable by giving a non-deterministic transformation algorithm. The generated unification are: an AC1-problem with linear constant restrictions and a second-order unification problem that can be transformed into a word-unification problem that can be decided using Makanin's algorithm. This solves an open problem in the field of unification. Furthermore it is shown that the word-problem can be decided in polynomial time, hence D-matching is NP-complete.
We consider the problem of unifying a set of equations between second-order terms. Terms are constructed from function symbols, constant symbols and variables, and furthermore using monadic second-order variables that may stand for a term with one hole, and parametric terms. We consider stratified systems, where for every first-order and second-order variable, the string of second-order variables on the path from the root of a term to every occurrence of this variable is always the same. It is shown that unification of stratified second-order terms is decidable by describing a nondeterministic decision algorithm that eventually uses Makanin's algorithm for deciding the unifiability of word equations. As a generalization, we show that the method can be used as a unification procedure for non-stratified second-order systems, and describe conditions for termination in the general case.