Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2018/19 / Oberseminar / Manfred Schmidt-Schauß: Generalizing Nominal Unification


Manfred Schmidt-Schauß: Generalizing Nominal Unification

Oberseminarvortrag von Manfred Schmidt-Schauß über Generalizing Nominal Unification
Wann 14:15 16:00 30.11.2018
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal

Es spricht Manfred Schmidt-Schauß über:
Generalizing Nominal Unification

Nominal unification for syntactically solving equations in
higher-order languages up to alpha-equivalence is known to be solvable
in quadratic time and a single most general solution is sufficient. An
application is the detection of whether two higher-order epressions
are syntactically equal, where the renaming  of arguments in function
definitions is taken into account. More sophisticated applications
like clone detection and computing overlaps of program transformations
with rules of the operational semantics require more expressivity.

The following extensions are discussed: atom-variables, which are
variables and stand for bound names; context variables that  make the
algorithms applicable to rules like dereferencing: let x = K in C[x]
-> let x = K in C[K]; permitting recursive let (as Haskell does).

The results are construction of algorithms for various extensions,
determining their  complexity and  comparing it with the inherent
asymptotic complexity of the problem, and determining upper bounds for
the number of solutions.